Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs
This work addresses the problem of automating mathematical proof generation for researchers and AI systems, offering an incremental improvement by integrating knowledge graphs without fine-tuning.
The authors tackled the challenge of automated theorem proving by developing KG-prover, a framework that combines large language models with knowledge graphs from mathematical texts to generate and formalize proofs. The approach improved general-purpose LLMs by up to 21% on the miniF2F-test dataset, achieving over 50% accuracy with specific models.
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 without additional scaling. Furthermore, KG-Prover with o4-mini achieves over 50% miniF2F-test. This work provides a promising approach for augmenting natural language proof reasoning with knowledge graphs without the need for additional finetuning.