@prefix this: <https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do> .
@prefix sub: <https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/> .
@prefix np: <http://www.nanopub.org/nschema#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix npx: <http://purl.org/nanopub/x/> .

sub:Head {
  this: np:hasAssertion sub:assertion;
    np:hasProvenance sub:provenance;
    np:hasPublicationInfo sub:pubinfo;
    a np:Nanopublication .
}

sub:assertion {
  <https://doi.org/10.48550/arXiv.2503.11657> dct:title "Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving";
    <http://purl.org/spar/cito/describes> <https://neverblink.eu/ontologies/llm-kg/methods#KGProver>;
    <http://purl.org/spar/cito/discusses> <https://neverblink.eu/ontologies/llm-kg/methods#DeepMath>,
      <https://neverblink.eu/ontologies/llm-kg/methods#DeepSeekProverV1.5>, <https://neverblink.eu/ontologies/llm-kg/methods#FormalTheoremProvingByHierarchicalDecomposition>,
      <https://neverblink.eu/ontologies/llm-kg/methods#GPTf>, <https://neverblink.eu/ontologies/llm-kg/methods#GraFormer>,
      <https://neverblink.eu/ontologies/llm-kg/methods#GraphRetriever>, <https://neverblink.eu/ontologies/llm-kg/methods#HOList>,
      <https://neverblink.eu/ontologies/llm-kg/methods#HyperTreeProofSearch>, <https://neverblink.eu/ontologies/llm-kg/methods#InternLM2.5StepProver>,
      <https://neverblink.eu/ontologies/llm-kg/methods#LeanDojo>, <https://neverblink.eu/ontologies/llm-kg/methods#MUSTARD>,
      <https://neverblink.eu/ontologies/llm-kg/methods#QAGNN>, <https://neverblink.eu/ontologies/llm-kg/methods#RetrievalAugmentedGenerationBaseline>,
      <https://neverblink.eu/ontologies/llm-kg/methods#STP>, <https://neverblink.eu/ontologies/llm-kg/methods#TheoremLlama>;
    a prov:Entity .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#DeepMath> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "DeepMath" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#DeepSeekProverV1.5> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "DeepSeek-Prover-V1.5" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#FormalTheoremProvingByHierarchicalDecomposition>
    a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "Formal Theorem Proving by Hierarchical Decomposition" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#GPTf> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "GPT-f" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#GraFormer> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "GraFormer" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#GraphRetriever> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "GraphRetriever" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#HOList> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "HOList" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#HyperTreeProofSearch> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "HyperTree Proof Search" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#InternLM2.5StepProver> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "InternLM2.5-StepProver" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#KGProver> dct:subject <https://neverblink.eu/ontologies/llm-kg/categories#KGEnhancedLLMInference>;
    a <http://purl.org/spar/fabio/Workflow>;
    rdfs:comment "KG-Prover is a novel framework that uses a knowledge graph (KG) mined from mathematical texts to augment general-purpose LLMs during the inference stage for automated theorem proving. It involves iterative KG traversal for context retrieval, informal proof generation by the LLM, formal proof generation, and verification/refinement with Lean feedback. The method enhances LLM performance by providing relevant knowledge dynamically at test-time without requiring additional finetuning.";
    rdfs:label "KG-Prover";
    <https://neverblink.eu/ontologies/llm-kg/hasTopCategory> <https://neverblink.eu/ontologies/llm-kg/top-categories#KGEnhancedLLM> .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#LeanDojo> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "LeanDojo" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#MUSTARD> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "MUSTARD" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#QAGNN> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "QAGNN" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#RetrievalAugmentedGenerationBaseline>
    a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "Retrieval Augmented Generation (RAG) Baseline" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#STP> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "STP" .
  
  <https://neverblink.eu/ontologies/llm-kg/methods#TheoremLlama> a <http://purl.org/spar/fabio/Workflow>;
    rdfs:label "TheoremLlama" .
}

sub:provenance {
  sub:assertion prov:wasAttributedTo <https://neverblink.eu/ontologies/llm-kg/agent>;
    prov:wasDerivedFrom <https://doi.org/10.48550/arXiv.2503.11657> .
}

sub:pubinfo {
  this: dct:created "2026-02-26T15:39:09.509Z"^^xsd:dateTime;
    dct:creator <https://neverblink.eu/ontologies/llm-kg/agent>;
    npx:hasNanopubType <https://neverblink.eu/ontologies/llm-kg/PaperAssessmentResult>;
    rdfs:label "LLM-KG assessment for paper 10.48550/arXiv.2503.11657" .
  
  sub:sig npx:hasAlgorithm "RSA";
    npx:hasPublicKey "MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAwNz2QK3SEifno78S7+48zUB0xpTex3mAzW73ZimHqNcdEMU5/apslrGrTHGFAt/Chocgo++r6JQp5ygY7NyJHGWdaIqnt85pjX4PbNfLAvapyUO00qZP34fY61w4eZ9UMtleWEsmZKRtQPyJ8ODl46i/rfPuZlcJGpM9Nmy5mpGWuepqIEvF4a/t7pLVeCEDFSYXT+yaiygt6ynIK5f7TtEDhZpeUf/Q74WhMPJXm4yTU/hqOX4IW+50kWHNArGGZwUaXwzyG6M3Zd6UMModryGkLqS4H/MSE3ZA1Ylnms7BfWLEXhMWlaKi6HRV4nGRDLhxVSi9LSRi3LWKLhNIIQIDAQAB";
    npx:hasSignature "BkpxW2xzAOB2r4VAvxKs3uPGHzOZ+ayqij+uaj/0T/5/qehPmAKtqG0w4kceaUJCZbnR2BQUG0lpYRvJ7t01yVteFtsBi/jj+UAuld7tzRLDiZtslXLnDDdHc4ZT2qSmO5GKE3mxwfo3+l7BvIxJ2Unz3ykzLMinTW99YNg9fSe8G2LXRWa/avs8Mlz2ybZpwKx/PWNy7uGxUP6OF4396X8rS/TMFZgfj1NaRulMGrQvrAmsROCTMKNjKiKY05/jEJa/gCwMhexG+2OlnCCdtrODtTsOiBx6TUAlXCZuZjE3QXtaunMi8iEeTQCX8DDo8gPGDNMQ0ezZSCqATDFGoQ==";
    npx:hasSignatureTarget this:;
    npx:signedBy <https://neverblink.eu/ontologies/llm-kg/agent> .
}