Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs
Large Language Models have demonstrated remarkable capabilities in natural language processing tasks, including mathematical problem-solving that requires multi-step logical reasoning. However, challenges persist in automating the identification of key mathematical concepts, understanding their interrelations, and formalizing proofs within a rigorous framework. We present a novel framework that leverages knowledge graphs to augment LLMs to construct and formalize mathematical proofs. Our results demonstrate significant performance improvements across multiple datasets, with using knowledge graphs, achieving up to a 34% success rate on the MUSTARDSAUCE dataset on o1-mini and consistently outperforming baseline approaches by 2-11% across different models. We show how this approach bridges the gap between natural language understanding and formal logic proof systems and achieve elevated results for foundation models over baseline.
Code (0)
등록된 구현이 없습니다.
Tasks
Formal LogicKnowledge GraphsLanguage ModelingLanguage ModellingLarge Language ModelLogical ReasoningMathematical Problem-SolvingMathematical ProofsNatural Language UnderstandingSimilar Papers 제목 키워드 기반
NaturalProver: Grounded Mathematical Proof Generation with Language Models
Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core t…
Automated Theorem ProvingLanguage ModelingLanguage ModellingLemmaHead: RAG Assisted Proof Generation Using Large Language Models
Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consi…
Automated Theorem ProvingMathematical ProofsMathematical ReasoningRAG+1NaturalProofs: Mathematical Theorem Proving in Natural Language
Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. …
Automated Theorem ProvingDomain GeneralizationInformation RetrievalRetrieval+1Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be …
Towards a Mathematics Formalisation Assistant using Large Language Models
Mathematics formalisation is the task of writing mathematics (i.e., definitions, theorem statements, proofs) in natural language, as found in books and papers, into a formal language that can then be checked for correctn…
Language ModelingLanguage ModellingLarge Language Model