LemmaHead: 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 consists of fine-tuning the model on written mathematical content such as academic publications and textbooks, so that the model can learn to emulate the style of mathematical writing. In this project, we explore the effectiveness of using retrieval augmented generation (RAG) to address gaps in the mathematical reasoning of LLMs. We develop LemmaHead, a RAG knowledge base that supplements queries to the model with relevant mathematical context, with particular focus on context from published textbooks. To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving via generating proofs to a given mathematical claim in the Lean formal language.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingMathematical ProofsMathematical ReasoningRAGRetrieval-augmented GenerationMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of…
Language ModelingLanguage ModellingLarge Language ModelTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories …
PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in P…
Baldur: Whole-Proof Generation and Repair with Large Language Models
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by trai…
Inference acceleration for large language models using "stairs" assisted greedy generation
Large Language Models (LLMs) with billions of parameters are known for their impressive predicting capabilities but require lots of resources to run. With their massive rise in popularity, even a small reduction in requi…
PredictionText Generation