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