@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> .
}