Goedel-Prover - 数学問題の形式的証明の自動生成とオープンソースの推論モデル

ゲーデル証明器とは何ですか？

Goedel-Proverは、プリンストン大学、清華大学、その他の機関によって開発されたオープンソースの大規模言語モデル（LLM）であり、数学の問題に対する形式的証明の生成を自動化することを目的としています。自然言語で記述された数学の問題を形式言語（Lean 4など）に変換することで、形式的な数学的記述や証明の不足という課題に取り組んでいます。Goedel-Proverは、専門家による反復的な手法を用いて学習され、形式的証明データセットを継続的に拡張することで、証明能力を段階的に向上させています。複数のベンチマークにおいて優れた性能を発揮しており、miniF2Fベンチマークでは57.6%の成功率を達成し、従来のオープンソースモデルを大きく上回っています。Goedel-Proverは、PutnamBenchの7つの問題を正常に解決し、Lean Workbookに対して約3万件の形式的証明を生成しました。これは、自動定理証明の分野における大きなブレークスルーと言えるでしょう。

Goedel-Prover の主な機能

• 正式な翻訳目標は、自然言語で表現された数学の問題を形式言語に変換し、翻訳の正確性と完全性を確保することである。
• 証明生成完全な証明を自動的に生成し、複雑な数学的推論をサポートします。
• パフォーマンス最適化証明機能は、専門家による反復手法に基づいて継続的に最適化され、それによって証明の成功率が向上します。
• 大規模データ処理大規模な形式的記述や証明データセットを処理・生成することで、モデルの汎化能力を向上させる。

ゲーデル・プルーバーの技術原理

• 正式な翻訳：
  • 自然言語で記述された数学の問題は、2つの形式化ツール（形式化ツールAと形式化ツールB）を用いてLean 4の形式言語に変換されます。形式化スタイルの多様性を高めるため、2つの形式化ツールは異なるデータセットで学習されます。
  • 形式的な記述の品質は、コンパイルの正確性（CC）テストと忠実度および完全性（FC）テストに基づいて評価され、リーン構文に準拠し、元の問題の意味を正確に捉えていることを確認します。
• エキスパートイテレーション初期段階では、既存の証明器（DeepSeek-Prover-V1.5-RLなど）を用いて各形式的命題に対して複数の証明候補が生成され、Leanコンパイラを用いて証明の正当性が検証されます。検証された証明は収集され、トレーニングデータとして使用され、ベースモデル（DeepSeek-Prover-V1.5-Baseなど）の教師あり微調整が実行され、新しい証明器が生成されます。このプロセスが繰り返され、各反復で新しい証明器を用いてより多くの証明が生成され、トレーニングデータに追加されることで、モデルの証明能力が徐々に向上します。
• データセットの拡張Goedel-Proverは、公開されているNuminaデータセットに加え、多数の個人収集された数学問題を形式化し、それらをLean Workbookの既存の記述と統合することで、形式化された記述の大規模なデータセットを構築します。トレーニング中は、Mathlib4などの外部データセットが段階的に追加され、モデルの様々な数学領域への適応性が向上します。

ゲーデル＝プローバー・プロジェクトの住所

• GitHubリポジトリ：https://github.com/Goedel-LM/Goedel-Prover
• ハギングフェイスモデルライブラリ：https://huggingface.co/Goedel-LM/Goedel-Prover
• arXiv技術論文：https://arxiv.org/pdf/2502.07640v1

Goedel-Prover の応用シナリオ

• 数学研究これは数学者が複雑な定理の証明を迅速に検証するのに役立ち、研究プロセスを加速させる。
• 数学教育これは、教師が詳細な証明を提供することで、生徒が数学の概念と論理を理解するのに役立つ。
• ソフトウェア検証ソフトウェアアルゴリズムの論理的な正しさを検証し、ソフトウェアの信頼性とセキュリティを向上させる。
• AIアルゴリズムの検証AIアルゴリズムの理論的根拠を検証し、その論理的な正しさと性能を保証する。
• 学際的研究異なる学問分野間の理論的な関連性を検証し、学際的研究のための理論的根拠を提供する。