Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
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.
Cite
@article{arxiv.2502.03321,
title = {Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques},
author = {Sangjun Han and Taeil Hur and Youngmi Hur and Kathy Sangkyung Lee and Myungyoon Lee and Hyojae Lim},
journal= {arXiv preprint arXiv:2502.03321},
year = {2025}
}
Comments
This manuscript was accepted for publication in the proceedings of the Computing Conference 2025 (Springer LNNS). The Version of Record (VoR) has not yet been published. This Accepted Manuscript does not reflect any post-acceptance improvements or corrections. Use of this version is subject to Springer Nature's Accepted Manuscript terms of use