形式的検証による自動的な予想解決

要旨: 大規模言語モデルにおける近年の進歩は、初歩的な問題解決から研究レベルの問題に対するますます高い能力へと、数学的推論を行う能力を大きく向上させてきました。しかし、そのような問題を確実に解き、検証することは、自然言語による推論に固有の曖昧さのため、依然として困難です。本論文では、自然言語による推論と形式的検証を統合することで、人手を最小限に抑えたエンドツーエンドの問題解決を可能にする、研究レベルの数学問題に取り組むための自動化フレームワークを提案します。本フレームワークは2つのコンポーネントから成ります。非形式的な推論エージェント Rethlas と、形式的検証エージェント Archon です。Rethlas は、推論プリミティブを定理探索エンジン Matlas と組み合わせることで、人間の数学者のワークフローを模倣し、解法戦略を探索して候補となる証明を構築します。Lean 4 のプロジェクトへと、構造化されたタスク分解、反復的な洗練、そして自動化された証明合成を通じて、非形式的な議論を翻訳するために、形式的定理探索エンジン LeanSearch を備えた Archon は、機械検査可能な正しさを保証します。このフレームワークを用いて、可換代数における未解決問題を自動的に解決し、得られた証明を人間の関与を実質的にほとんど伴わずに Lean 4 で形式的に検証します。実験の結果、強力な定理検索ツールが、異なる分野にまたがる数学的手法の発見と適用を可能にすること、また形式的エージェントが非自明な推論ギャップを自律的に埋められることを示します。より広く言えば、本研究は、定理検索ツールを備えた非形式的および形式的推論システムが連携して検証可能な結果を生み出し、人間の労力を大幅に削減し、人間—AI 協働による数学的研究の具体的な実装を提供する、数学研究における有望なパラダイムを示すものです。