Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques

TL;DR

This paper demonstrates that integrating ChatGPT with basic search techniques significantly improves formal proof generation efficiency, achieving a 31.15% success rate on the miniF2F dataset and outperforming existing benchmarks.

Contribution

It introduces a novel approach combining large language models and simple search methods to enhance formal proof generation in proof assistants like Lean.

Findings

Best model surpasses all known benchmarks with 31.15% pass rate

Models perform well across multiple datasets and language models

Insights suggest promising future directions for AI-assisted formal proofs

Abstract

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.