Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
This work addresses the problem of making formal proof generation more efficient and accessible for mathematicians and AI researchers, though it appears incremental as it builds on existing methods like ChatGPT and Lean.
The paper tackled the challenge of formal proof generation by integrating ChatGPT with basic searching techniques, achieving a 31.15% pass rate on the miniF2F dataset, which surpasses all known benchmarks.
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 ChatGPT and basic searching techniques to simplify generating formal proofs, with a particular focus on the miniF2F dataset. We demonstrate how combining a large language model like ChatGPT with a formal language such as Lean, which has the added advantage of being verifiable, enhances the efficiency and accessibility of formal proof generation. Despite its simplicity, our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate. We extend our experiments to include other datasets and employ alternative language models, showcasing our models' comparable performance in diverse settings and allowing for a more nuanced analysis of our results. Our findings offer insights into AI-assisted formal proof generation, suggesting a promising direction for future research in formal mathematical proof.