mlsanityData to 7 Oct 2026

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

arXiv 2503.11657 ↗First posted 4 Feb 2025cs.CLcited by 2

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Large language models have demonstrated remarkable capabilities in natural language processing tasks requiring multi-step logical reasoning capabilities, such as automated theorem proving. However, challenges persist within theorem proving, such as the identification of key mathematical concepts, understanding their interrelationships, and formalizing proofs correctly within natural language. We present KG-prover, a novel framework that leverages knowledge graphs mined from reputable mathematical texts to augment general-purpose LLMs to construct and formalize mathematical proofs. We also study the effects of scaling graph-based, test-time compute using KG-Prover, demonstrating significant performance improvements over baselines across multiple datasets. General-purpose LLMs improve up to 21% on miniF2F-test when combined with KG-Prover, with consistent improvements ranging from 2-11% on the ProofNet, miniF2F-test, and MUSTARD datasets. Furthermore, KG-Prover with o4-mini achieves 50% on pass miniF2F-test. This work provides a promising approach for augmenting natural language proof reasoning with knowledge graphs without the need for additional finetuning.

Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 31 of its 45 references that are in the map. First posted on arXiv 4 Feb 2025.

Builds on

31 of 45 references.

Closest ancestors · 5

Same direction, newest first

  1. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  2. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically4 Nov
  3. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts3 Jul
  4. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data14 Feb
  5. 2020Generative Language Modeling for Automated Theorem Proving7 Sep

Other references · 26

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,601
  4. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  5. 2018Deep contextualized word representationscited by 2,285
  6. 2024Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameterscited by 1,928
  7. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  8. 2021QA-GNN: Reasoning with Language Models and Knowledge Graphs for Question Answeringcited by 386
  9. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  10. 2022Text and Code Embeddings by Contrastive Pre-Trainingcited by 358
  11. 2023JudgeLM: Fine-tuned Large Language Models are Scalable Judgescited by 351
  12. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
14 more
  1. 2022Autoformalization with Large Language Modelscited by 252
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  4. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  5. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  6. 2024GRAG: Graph Retrieval-Augmented Generationcited by 77
  7. 2019Knowledge Guided Text Retrieval and Reading for Open Domain Question Answeringcited by 59
  8. 2024Efficiently Learning at Test-Time: Active Fine-Tuning of LLMscited by 42
  9. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  10. 2019HOList: An Environment for Machine Learning of Higher-Order Theorem Provingcited by 19
  11. 2021GraFormer: Graph Convolution Transformer for 3D Pose Estimationcited by 10
  12. 2023Allies: Prompting Large Language Model with Beam Searchcited by 6
  13. 2022An Empirical Study of Retrieval-enhanced Graph Neural Networkscited by 1
  14. 2023FusionMind -- Improving question and answering with external context fusioncited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 2.

2 papers.

  1. 2026Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learningcited by 0
  2. 2026When Does Structured Knowledge Help Neural Theorem Proving?cited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  2. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  3. 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
  4. 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofs
  5. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
  6. 2025Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
  7. 2026LiveMathematicianBench: A Live Benchmark for Research-Level Mathematical Reasoning with Proof Sketches
  8. 2026TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs