https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/Head https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://www.nanopub.org/nschema#hasAssertion https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/assertion https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://www.nanopub.org/nschema#hasProvenance https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/provenance https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://www.nanopub.org/nschema#hasPublicationInfo https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/pubinfo https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.nanopub.org/nschema#Nanopublication https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/assertion https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/dc/terms/title Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/describes https://neverblink.eu/ontologies/llm-kg/methods#KGProver https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#DeepMath https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#DeepSeekProverV1.5 https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#FormalTheoremProvingByHierarchicalDecomposition https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#GPTf https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#GraFormer https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#GraphRetriever https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#HOList https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#HyperTreeProofSearch https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#InternLM2.5StepProver https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#LeanDojo https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#MUSTARD https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#QAGNN https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#RetrievalAugmentedGenerationBaseline https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#STP https://doi.org/10.48550/arXiv.2503.11657 http://purl.org/spar/cito/discusses https://neverblink.eu/ontologies/llm-kg/methods#TheoremLlama https://doi.org/10.48550/arXiv.2503.11657 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://www.w3.org/ns/prov#Entity https://neverblink.eu/ontologies/llm-kg/methods#DeepMath http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#DeepMath http://www.w3.org/2000/01/rdf-schema#label DeepMath https://neverblink.eu/ontologies/llm-kg/methods#DeepSeekProverV1.5 http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#DeepSeekProverV1.5 http://www.w3.org/2000/01/rdf-schema#label DeepSeek-Prover-V1.5 https://neverblink.eu/ontologies/llm-kg/methods#FormalTheoremProvingByHierarchicalDecomposition http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#FormalTheoremProvingByHierarchicalDecomposition http://www.w3.org/2000/01/rdf-schema#label Formal Theorem Proving by Hierarchical Decomposition https://neverblink.eu/ontologies/llm-kg/methods#GPTf http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#GPTf http://www.w3.org/2000/01/rdf-schema#label GPT-f https://neverblink.eu/ontologies/llm-kg/methods#GraFormer http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#GraFormer http://www.w3.org/2000/01/rdf-schema#label GraFormer https://neverblink.eu/ontologies/llm-kg/methods#GraphRetriever http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#GraphRetriever http://www.w3.org/2000/01/rdf-schema#label GraphRetriever https://neverblink.eu/ontologies/llm-kg/methods#HOList http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#HOList http://www.w3.org/2000/01/rdf-schema#label HOList https://neverblink.eu/ontologies/llm-kg/methods#HyperTreeProofSearch http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#HyperTreeProofSearch http://www.w3.org/2000/01/rdf-schema#label HyperTree Proof Search https://neverblink.eu/ontologies/llm-kg/methods#InternLM2.5StepProver http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#InternLM2.5StepProver http://www.w3.org/2000/01/rdf-schema#label InternLM2.5-StepProver https://neverblink.eu/ontologies/llm-kg/methods#KGProver http://purl.org/dc/terms/subject https://neverblink.eu/ontologies/llm-kg/categories#KGEnhancedLLMInference https://neverblink.eu/ontologies/llm-kg/methods#KGProver http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#KGProver http://www.w3.org/2000/01/rdf-schema#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. https://neverblink.eu/ontologies/llm-kg/methods#KGProver http://www.w3.org/2000/01/rdf-schema#label KG-Prover https://neverblink.eu/ontologies/llm-kg/methods#KGProver https://neverblink.eu/ontologies/llm-kg/hasTopCategory https://neverblink.eu/ontologies/llm-kg/top-categories#KGEnhancedLLM https://neverblink.eu/ontologies/llm-kg/methods#LeanDojo http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#LeanDojo http://www.w3.org/2000/01/rdf-schema#label LeanDojo https://neverblink.eu/ontologies/llm-kg/methods#MUSTARD http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#MUSTARD http://www.w3.org/2000/01/rdf-schema#label MUSTARD https://neverblink.eu/ontologies/llm-kg/methods#QAGNN http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#QAGNN http://www.w3.org/2000/01/rdf-schema#label QAGNN https://neverblink.eu/ontologies/llm-kg/methods#RetrievalAugmentedGenerationBaseline http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#RetrievalAugmentedGenerationBaseline http://www.w3.org/2000/01/rdf-schema#label Retrieval Augmented Generation (RAG) Baseline https://neverblink.eu/ontologies/llm-kg/methods#STP http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#STP http://www.w3.org/2000/01/rdf-schema#label STP https://neverblink.eu/ontologies/llm-kg/methods#TheoremLlama http://www.w3.org/1999/02/22-rdf-syntax-ns#type http://purl.org/spar/fabio/Workflow https://neverblink.eu/ontologies/llm-kg/methods#TheoremLlama http://www.w3.org/2000/01/rdf-schema#label TheoremLlama https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/provenance https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/assertion http://www.w3.org/ns/prov#wasAttributedTo https://neverblink.eu/ontologies/llm-kg/agent https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/assertion http://www.w3.org/ns/prov#wasDerivedFrom https://doi.org/10.48550/arXiv.2503.11657 https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/pubinfo https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://purl.org/dc/terms/created 2026-02-26T15:39:09.509Z https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://purl.org/dc/terms/creator https://neverblink.eu/ontologies/llm-kg/agent https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://purl.org/nanopub/x/hasNanopubType https://neverblink.eu/ontologies/llm-kg/PaperAssessmentResult https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do http://www.w3.org/2000/01/rdf-schema#label LLM-KG assessment for paper 10.48550/arXiv.2503.11657 https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/sig http://purl.org/nanopub/x/hasAlgorithm RSA https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/sig http://purl.org/nanopub/x/hasPublicKey MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAwNz2QK3SEifno78S7+48zUB0xpTex3mAzW73ZimHqNcdEMU5/apslrGrTHGFAt/Chocgo++r6JQp5ygY7NyJHGWdaIqnt85pjX4PbNfLAvapyUO00qZP34fY61w4eZ9UMtleWEsmZKRtQPyJ8ODl46i/rfPuZlcJGpM9Nmy5mpGWuepqIEvF4a/t7pLVeCEDFSYXT+yaiygt6ynIK5f7TtEDhZpeUf/Q74WhMPJXm4yTU/hqOX4IW+50kWHNArGGZwUaXwzyG6M3Zd6UMModryGkLqS4H/MSE3ZA1Ylnms7BfWLEXhMWlaKi6HRV4nGRDLhxVSi9LSRi3LWKLhNIIQIDAQAB https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/sig http://purl.org/nanopub/x/hasSignature BkpxW2xzAOB2r4VAvxKs3uPGHzOZ+ayqij+uaj/0T/5/qehPmAKtqG0w4kceaUJCZbnR2BQUG0lpYRvJ7t01yVteFtsBi/jj+UAuld7tzRLDiZtslXLnDDdHc4ZT2qSmO5GKE3mxwfo3+l7BvIxJ2Unz3ykzLMinTW99YNg9fSe8G2LXRWa/avs8Mlz2ybZpwKx/PWNy7uGxUP6OF4396X8rS/TMFZgfj1NaRulMGrQvrAmsROCTMKNjKiKY05/jEJa/gCwMhexG+2OlnCCdtrODtTsOiBx6TUAlXCZuZjE3QXtaunMi8iEeTQCX8DDo8gPGDNMQ0ezZSCqATDFGoQ== https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/sig http://purl.org/nanopub/x/hasSignatureTarget https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do https://w3id.org/np/RAi_53mSPRrWhLngRPhQ1YKoR_fxmjeCUqmYB-doqX6Do/sig http://purl.org/nanopub/x/signedBy https://neverblink.eu/ontologies/llm-kg/agent