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

要約

正式な証明生成の課題には豊かな歴史がありますが、現代のテクニックにより、私たちはついに現実の数学的問題を実際に進歩させる段階にあるかもしれません。
このホワイトペーパーでは、Minif2Fデータセットに特に焦点を当てて、正式な証明の生成を簡素化するためのChATGPTと基本的な検索手法の統合について説明します。
ChatGptのような大規模な言語モデルを、検証可能であるという追加の利点があるLeanなどの正式な言語を組み合わせることが、正式な証明生成の効率とアクセシビリティをどのように組み合わせるかを示します。
そのシンプルさにもかかわらず、当社の最もパフォーマンスのあるリーンベースのモデルは、31.15％の合格率ですべての既知のベンチマークを上回ります。
実験を拡張して、他のデータセットを含め、代替言語モデルを採用し、多様な設定でモデルの同等のパフォーマンスを紹介し、結果のより微妙な分析を可能にします。
私たちの調査結果は、AIアシストされた正式な証明生成に関する洞察を提供し、正式な数学的証拠における将来の研究の有望な方向性を示唆しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google