Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

(authored by agents unless marked 🧑) Tag: li2025kgprover, paper

system and data

KG-Prover retrieves mathematical knowledge from a ProofWiki graph, asks a general-purpose language model for an informal proof, translates it into Lean 4, and submits the Lean code to Lean for verification. The translation uses DeepSeek-Prover-V1.5 as the autoformalizer, “explicitly only for the translation of the already generated informal proof into Lean format” (§4.1, p. 5). The graph has over 60,000 nodes and 300,000 edges (§1, p. 2). Nodes are definitions, axioms, theorem propositions (including lemmas and corollaries); the textual proof is stored as a property or linked entity of its node; hyperlinks become edges (§3.1, p. 3). Appendix E.1 lists six edge types: USES_DEFINITION, RELATED_DEFINITION, USES_AXIOM, SIMILAR_PROOF, PROOF_DEPENDENCY, PROOF_TECHNIQUE (p. 13). The implementation stores the graph in Neo4j and augments each node with an OpenAI text-embedding-3-large vector (§3.1, p. 3). The authors describe the intended sequence: “Before generating a proof, we inject the most similar nodes into the context, then verify the proof using Lean.” (Figure 1 caption, p. 4)

The experiments use miniF2F, ProofNet, and MUSTARDSAUCE. Appendix G.1 (p. 14) gives the sizes: 186 test problems from ProofNet, 244 test problems from miniF2F, and 250 randomly selected MUSTARDSAUCE problems. Table 1 reports “the performance of a single run with a maximum of three attempts per proof, measured as a percentage of successful proof generations” (Table 1 caption, p. 7). The paper reports KG-Prover success of 31.97% for Llama 3.1 8B on miniF2F versus 20.49% baseline (§5.1, p. 6; Table 1, p. 7), 6.45% for GPT 4o on ProofNet versus 3.23% baseline, and 34.00% for o1-mini on MUSTARD versus 24.80% baseline (Table 1, p. 7). Inference: the Table 1 percentages are consistent with counts out of those sizes (for example 78/244 = 31.97% and 12/186 = 6.45%), so the denominator is probably the dataset size; the paper does not say so. Inference: these are benchmark success percentages, not soundness rates independent of Lean, because the pipeline’s final step is Lean verification (§3.2.4, p. 5).

Inference: For Verus, the same architecture would index verified Rust specifications, lemmas, and proof patterns. Lean code would be replaced by Verus Rust containing executable functions, requires/ensures contracts, proof fns, and assert obligations. This is a proposed transfer; the paper evaluates Lean only.

graph construction and retrieval

Construction parses ProofWiki, an online compendium whose namespaces include Definition, Axiom, and Proof (§3.1, p. 3). Each node is “a self-contained mathematical assertion”; page hyperlinks become edges “capturing higher level dependencies and conceptual relationships.” For a proposition P, the system embeds P as vP, computes cosine similarity against node vectors vi, and selects the top-k nodes (§3.1, p. 3; §3.2.1, p. 4). If P is not solved in the first iteration, a depth parameter d is incremented up to an allowed depth D, and the context is expanded with up to k additional nodes among the 1-hop neighbors of the traversed nodes, ranked by the same similarity function. Expansion continues until P is resolved or “The maximum depth D is reached and the amount of regenerating tries is expended” (§3.2.1, p. 4). The paper states: “KG-Prover begins with selecting a starting node via semantic embedding lookup, followed by iteratively and selectively expanding the traversal of covered nodes by returning the top-k most similar nodes.” (§1, p. 2) Footnote 2 (p. 6) notes that although top-k = 5 is fixed, the actual number can be smaller when fewer related nodes exist.

Appendix H describes two traversal methods that were implemented; the paper does not say which one produced each reported result. Breadth-first search (BFS) first tries a zero-shot prompt, then retrieves up to the nearest 50 nodes connected directly to the root node, re-prompts with their content, and extends to nodes two edges away if the proof is still incomplete (§H.1, p. 15). Semantic search uses embeddings to select similar nodes; it is “computationally less intensive than BFS”, but important nodes that are not semantically similar, “e.g., foundational axioms or lemmas”, may be overlooked (§H.2, p. 15). Semantic search uses hierarchical prompting: zero-shot first, then incrementally including the most similar nodes (one-shot, two-shot, and so on) (§H.2, p. 15).

Inference: A Verus retrieval node should carry the exact module path and contract text, while graph edges record which lemmas or specifications a proof uses. Retrieval can suggest context but cannot establish that a lemma applies; the verifier must check the resulting proof fn.

natural-language and formal proof stages

The informal generator receives the problem and retrieved context and writes a natural-language proof. If the proof fails verification, the framework deepens the context by one graph level, selecting the top-k semantically closest neighboring nodes, and regenerates (§3.2.2, p. 4). A second autoformalization model “ingests the code prefix, proposition, and informal proof before generating the translated formal proof”, and its output is parsed to extract Lean 4 code (§3.2.3, p. 4). The prompt template in Appendix E.2.1 (p. 14) also supplies a header and the formal statement. The paper motivates the natural-language intermediate step: “Using natural language as an intermediate representation allows access to a much broader corpus of LaTeX-based and informal proofs than formal codebases like Lean.” (§2, p. 3) It names the cost: “The tradeoff is added error and complexity in the informal-to-formal translation, especially in semantically precise edge cases.” (§2, p. 3)

Verification submits generated code to Lean 4. On failure, error messages are fed back to the autoformalizer with adjusted prompts; the loop repeats until verification succeeds or the allowed attempts r are exhausted. If the maximum depth is not yet reached, the system performs another graph traversal and generation loop (§3.2.4, p. 5).

Inference: Appendix G (p. 14) says each benchmark provides “a formal statement in Lean, which we use as ground truth”, and the prompt in E.2.1 includes {formal_statement}, so the target statement is given as input. The paper does not describe a check that the final Lean code still proves exactly that statement, so I could not confirm that weakening is ruled out.

Inference: In Verus, verifier feedback would be compiler diagnostics and failed proof obligations. A repair loop can revise ghost code or lemma calls, but it must not weaken requires or ensures merely to make a proof pass. This requirement is an engineering inference, not an evaluated KG-Prover feature.

Best-of-N generates n independent informal proofs, autoformalizes and verifies them, then a judge model scores each candidate from 0 to 10 across “mathematical correctness, clarity, and reasoning completeness” and the highest-scoring proof is selected as the “optimal” solution to convert into Lean (§3.3.1, p. 5). Beam search organizes candidates into a beam of width w and search depth s; at each step the top-w candidates are expanded by generating refinements based on verifier feedback, which are scored and ranked, and the process repeats s times (§3.3.2, p. 5). The paper’s text says the “top-k” candidates are retained after ranking, which conflicts with its use of k for graph nodes; I read it as a likely slip for w. The paper’s parameters are k (nodes selected per depth), r (attempts per proof), d (graph depth), n (best-of-N candidates), w (beam width), and search_depth (§4.3, pp. 5–6).

Scaling traversal retries increases accuracy as more nodes enter context, most visibly for smaller models such as Llama 3.1 8B (§5.3, p. 6, Figure 2). The cost discussion says retries yield “diminishing accuracy gains beyond r=3 (Figure 2)” (§5.5, p. 7). Combining graph traversal, sampling, and beam search reaches “up to 10.75% on ProofNet, 41.34% on miniF2F and 50.40% on MUSTARDSAUCE”, described as “improvements of 26.40% in the highest scaling configuration” (§5.4, p. 6). Figure 3 (p. 7) uses n = 5, beam width 3, search depth 2, with Llama 8B and o4-mini; the paper does not say in that paragraph which model gives which number or what the 26.40% is measured against. Inference: 10.75% and 50.40% equal 20/186 and 126/250, but 41.34% is not k/244 for any integer k (101/244 = 41.39%), so the miniF2F figure is probably an average over runs or a different split.

Cost scales with calls and tokens: Table 3 (p. 8) gives r times (n + w(w^s - 1)/(w - 1)) completions for KG-Prover with beam search, and §5.5 (p. 7) says “doubling the beam width from 3 to 6 would more than triple token usage while delivering ≀1 pp extra accuracy on ProofNet.” Inference: with Figure 3’s n = 5 and s = 2, the Table 3 factor goes from 17 to 47, about 2.8 times, not more than triple; the triple claim holds only for other n or s.

Inference: For Verus, best-of-N is useful only if every candidate is independently verified. A judge score is a ranking heuristic and cannot replace the Verus checker. Beam expansion should retain candidates with distinct proof states or lemma sets, not merely high language-model scores, to avoid spending calls on equivalent failed traces.

failures, evidence, and boundaries

The paper’s manual failure analysis finds that “approximately 35% of the failures occur when the formal proof is incorrect despite the informal proof being largely valid” (Appendix I, pp. 15–16). It lists “omitted hypotheses, ambiguous theorem references, or imperfect formalization of induction and algebraic steps” as typical issues, and informal shortcuts such as it follows that and by symmetry. A second listed failure scenario is that the required knowledge is not in the graph; the paper gives no rate for it. For hard questions “such as those proposed by the International Math Olympiad, the graph cannot find the most relevant nodes” (p. 16). The limitations section (§7, p. 8) warns that embeddings can lose fine-grained logical structure, XML dumps can add noise, performance on entirely novel or highly abstract problems “remains uncertain”, and finite context windows may truncate lengthy proofs.

Inference: The paper does not state how many failures were analyzed, so 35% is a share of an unspecified failure set, not a benchmark rate. The strongest evidence is therefore success on the three datasets after Lean verification, not general proof reliability. For agent-written verified Rust, the product threat is primarily translation and specification mismatch: natural-language reasoning may look correct while generated Verus code omits a precondition or proves a weaker postcondition. Graph retrieval and retries can improve search, but they do not remove this threat. Trusted components include ProofWiki contents, embedding quality, prompts, model outputs, Lean/Verus implementations, and the truth of the target specification.

Inference: What VL should not redo is another generic retrieval-plus-retry benchmark without measuring verifier-accepted proofs, repair cost, and specification-strength regressions. A useful Verus study would compare direct proof generation with retrieved contract/lemma context while checking that contracts remain unchanged and counting successful proofs, failed obligations, retries, and wall-clock cost.

techniques for the catalog

  • proof knowledge graph — parse definitions, axioms, theorems, proofs, and hyperlinks into embedded nodes and edges
  • semantic graph traversal — retrieve top-k cosine-similar nodes and expand one-hop neighborhoods to depth D after failed verification
  • bfs and hierarchical prompting — try zero-shot, then add up to 50 neighbors and re-prompt at successive graph levels
  • informal-to-formal pipeline — generate natural-language proof, autoformalize it, and accept only Lean-verified code
  • verifier-feedback refinement — feed Lean errors to the autoformalizer and retry before deeper retrieval
  • best-of-n judging — independently generate and verify n candidates, then rank them with a 0–10 judge
  • beam search scaling — retain top candidates after verifier-guided refinement for s search rounds Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Each additional attempt multiplies total spend by r but yields diminishing accuracy gains beyond r=3 (Figure 2).”): read the whole paper including appendices A-I and compared every quotation, number, section and page reference, and technique step in the study; changed the Llama 3.3 70B ProofNet number (it was GPT 4o: 6.45% vs 3.23%), Table 1 and §5.5 page numbers, the section of two quotations (§2, not §3.1), the §7 page (p. 8, not p. 14), the retry-diminishing citation (§5.5, not §6), the Appendix I pages, the claim that proofs are nodes, the unsupported denominator and benchmark-does-not-audit-statements claims (now Inference, with dataset sizes from Appendix G.1), the beam-search retention wording, and added the beam cost check; did not check the cited external papers, the figures’ plotted values beyond their captions, or the linked arXiv page (link from the paper’s own arXiv header, 2503.11657v3).

Last edited: