用ChatGPT和基础搜索，让形式化证明更简单高效
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
- 结合ChatGPT与Lean语言，提升形式化证明生成效率
- 在miniF2F数据集上达31.15%通过率，超越现有基准
- 方法简洁可复现，适合数学推理与AI辅助证明研究者
形式化证明生成面临长期挑战，但借助现代技术，我们正有望在真实数学问题上取得实质性进展。本文探索将ChatGPT与基础搜索技术结合，用于简化形式化证明生成，重点基于miniF2F数据集。结果表明，将大型语言模型如ChatGPT与可验证的形式语言Lean结合，显著提升了证明生成的效率与可及性。尽管方法简单，其最优的Lean模型在miniF2F上达到31.15%的通过率，超过所有已知基准。我们在其他数据集上扩展实验，采用不同语言模型，验证了模型在多种场景下的可比性能，实现更细致的结果分析。研究为人工智能辅助形式化数学证明提供了新方向。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。