Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2502.03321 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929719899848704 |
|---|---|
| author | Han, Sangjun Hur, Taeil Hur, Youngmi Lee, Kathy Sangkyung Lee, Myungyoon Lim, Hyojae |
| author_facet | Han, Sangjun Hur, Taeil Hur, Youngmi Lee, Kathy Sangkyung Lee, Myungyoon Lim, Hyojae |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_03321 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Han, Sangjun Hur, Taeil Hur, Youngmi Lee, Kathy Sangkyung Lee, Myungyoon Lim, Hyojae Logic in Computer Science Artificial Intelligence 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. |
| title | Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2502.03321 |