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

Problem Statement

While Large Language Models (LLMs) have demonstrated capabilities in multi-step logical reasoning, automated theorem proving remains challenging. Specific hurdles include the accurate identification of key mathematical concepts, understanding their interrelationships, and correctly formalizing proofs within natural language or formal systems. Existing approaches often rely on intensive fine-tuning, expert iteration, or training on large volumes of formal data (e.g., Lean), which can be resource-heavy and limit the model's ability to leverage broader, informal mathematical knowledge. Furthermore, purely formal approaches may struggle with the flexibility of natural reasoning, while purely natural language approaches face ambiguity when translating to formal verification systems.

Methodology: KG-Prover

The authors introduce KG-Prover, a novel framework that augments general-purpose LLMs with a knowledge graph (KG) mined from reputable mathematical texts (specifically ProofWiki) to construct and formalize proofs. The system operates without additional fine-tuning of the base LLM, relying instead on test-time compute scaling and retrieval-augmented generation.

Core Components

1. Knowledge Graph Construction:

   • Source: The graph is built by parsing ProofWiki, extracting nodes from namespaces such as "Definition," "Axiom," and "Proof."
   • Structure: Each node represents a self-contained mathematical assertion (e.g., a theorem proposition or definition). Edges represent hyperlinks found within the text, capturing dependencies and conceptual relationships.
   • Scale: The resulting graph contains over 60,000 nodes and 300,000 edges.
   • Embeddings: Nodes are augmented with pre-computed embedding vectors (using text-embedding-3-large) to facilitate semantic retrieval.

2. Inference Pipeline:

   • Retrieval & Traversal: Given a proposition $P$, the system computes its embedding and retrieves the top-$k$ most similar nodes. If the initial proof attempt fails, the system iteratively expands the context by traversing the graph to depth $d$, selecting top-$k$ neighbors of previously visited nodes.
   • Informal Proof Generation: The LLM generates an informal, natural language proof using the retrieved context. This leverages the model's emergent reasoning abilities and the broad corpus of informal proofs available in the KG.
   • Autoformalization: A separate model (DeepSeek-Prover-V1.5) translates the informal proof into Lean 4 code.
   • Verification & Refinement: The generated Lean code is verified using the Lean 4 theorem prover. If verification fails, error messages are fed back to the autoformalizer for refinement. If the proof still fails, the system may increase the graph traversal depth or employ search strategies.

3. Scaling Strategies (Test-Time Compute):

   • Best-of-N: The system generates $n$ independent informal proofs, autoformalizes them, and uses a dedicated "judge" model to score them based on correctness and clarity, selecting the highest-scoring candidate.
   • Beam Search: Proof candidates are organized into a beam of width $w$. At each step, candidates are expanded based on verifier feedback, scored, and the top-$k$ are retained for the next iteration. This balances exploration of diverse proof paths with verification-driven refinement.

Key Contributions

• KG-Prover Framework: A system that integrates natural language informal proof generation with iterative, knowledge-graph-based traversal and an LLM-as-a-judge mechanism, eliminating the need for specialized training or expert iteration.
• Large-Scale Mathematical KG: The construction of a knowledge graph from ProofWiki with 60,000+ nodes and 300,000+ edges, modeling complex relationships between mathematical concepts.
• Iterative Refinement System: A heuristic evaluation and beam search mechanism that improves performance by up to 26.4% over baselines and 21.8% over non-scaling KG-Prover configurations.
• Demonstration of Test-Time Scaling: Evidence that modulating graph traversal depth and employing search strategies (Best-of-N, Beam Search) significantly boosts performance without retraining the underlying models.

Experimental Results

The framework was evaluated on three benchmarks: miniF2F-test, ProofNet, and MUSTARDSAUCE.

• Performance Gains:

  • KG-Prover consistently outperformed baseline systems and standard Retrieval-Augmented Generation (RAG) across all datasets.
  • Improvements ranged from 2% to 11% over baselines across multiple models (Llama 3.1 8B, GPT-4o, o1-mini, etc.).
  • On miniF2F-test, general-purpose LLMs improved by up to 21% when combined with KG-Prover.
  • The configuration of KG-Prover with o4-mini achieved a 50% pass rate on miniF2F-test.
  • In the highest scaling configuration, improvements reached 26.4% over baselines.

• Scaling Effects:

  • Traversal Depth: Accuracy increased with greater traversal depth ($r$), particularly for smaller parameter models like Llama 3.1 8B. The first few depth increases yielded the most significant gains.
  • Search Strategies: Combining the KG with Beam Search and Best-of-N sampling further enhanced accuracy, achieving up to 10.75% on ProofNet and 50.40% on MUSTARDSAUCE.
  • Finetuned Models: Even when applied to models already fine-tuned for Lean (e.g., TheoremLlama, DeepSeek-Prover-V1.5), KG-Prover provided additional performance gains (e.g., +1.85% over a finetuned baseline on miniF2F).

Significance and Claims

The paper posits that KG-Prover offers a promising, scalable approach to automated theorem proving that does not require additional fine-tuning or intensive expert iteration. By leveraging the built-in natural language reasoning capabilities of general-purpose LLMs and augmenting them with structured, graph-retrieved information, the framework effectively bridges the gap between informal reasoning and formal verification.

The authors emphasize that this method allows existing foundation models to achieve performance comparable to or exceeding that of specialized, fine-tuned systems simply by injecting related concepts during inference. The work highlights the potential of test-time compute scaling—modulating graph traversal depth and employing search strategies—as a viable alternative to scaling model parameters for complex reasoning tasks. While the approach introduces challenges in the informal-to-formal translation step, the two-agent system (generation + autoformalization) supported by graph retrieval successfully mitigates these issues, providing interpretable reasoning traces and novel strategies for proof generation.