Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Goedel-Architectは、ブループリントの生成と洗練戦略を利用することで、MiniF2F、Putnam、IMOといった難易度の高い数学的ベンチマークにおいて、既存のパイプラインよりも大幅に低いコストで最先端の性能を実現する、Lean 4定理証明のためのエージェンティック・フレームワークです。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
あなたは、レゴブロックを使って巨大で複雑なお城を作ろうとしていると想像してください。あなたには設計図がありますが、それは絵ではなく、「塔を作るには、まず土台が必要であり、次に壁、そして窓が必要である」という指示のリストです。
問題は、もしあなたが一度に巨大なジャンプで塔全体を建てようとしたら、行き詰まったり、途中で「土台の作り方が間違っていた」と気づいたりする可能性があることです。
Goedel-Architectは、このような数学的な「お城」（形式的証明）を構築するために設計された、新しいスマートなロボットチームであり、Lean 4という言語を使用します。このロボットは、一度に全体を築き上げるのではなく、「設計図の生成と洗練（Blueprint Generation and Refinement）」と呼ばれる戦略を使用します。
その仕組みを、シンプルなステップに分けて説明します。
1. 設計図（マスタープラン）
ロボットが建築を開始する前に、まず設計図を描きます。
- それは何か？ これは依存関係マップだと考えてください。大きな数学の問題を証明するために必要な、あらゆる小さなステップ（「補題（lemma）」と呼ばれます）をリストアップしたものです。
- 仕組み: どのステップが他のステップに依存しているかを示す矢印を描きます。例えば、「屋根を作る前に、壁を完成させなければならない」といった具合です。
- ひねり: 数学の問題が非常に難しい場合、ロボットには自然言語による証明が与えられることがあります。これは、人間の数学者がロボットに対して、解法のラフスケッチやストーリーを伝えているようなものです。ロボットはこのストーリーを利用して、最初からより正確で優れた設計図を描き出します。
2. 建設作業員（並列証明）
設計図の準備ができたら、ロボットは一つずつステップを進めるのではなく、専門の作業員チーム（「Lean プルーバー」）を送り出し、すべての小さなステップに対して同時に作業を行います。
- 各作業員は、自分自身の特定のステップと、使用を許可されているステップ（それらの「依存関係」）のみに集中します。
- 彼らは自分の部分を構築しようと試みます。成功すれば、設計図のその部分を緑色にします。
- 失敗した場合は、青色（行き詰まり）または赤色（破損）にします。
3. 修理ループ（洗練）
ここが、Goedel-Architectが他のロボットと異なる点です。
- 従来の方法: 他の多くのAIシステムは、問題を解決しようとして行き詰まると、その行き詰まった一つのピースを何度も細かく分割しようとします。これは、壊れた壁をただ同じ場所を叩き続けることで直そうとするようなものです。これはしばしば、行き止まりを招きます。
- Goedel流: もし作業員が行き詰まったら、チーム全体が停止し、設計図全体を見直します。
- 診断: ロボットは「なぜ失敗したのか？」と問いかけます。
- ケースA（赤）: 「ああ、このステップ自体が実は間違っていたのだ！」（設計図に誤った考えがあった）。ロボットは命題を修正します。
- ケースB（青）: 「このステップは正しいが、今は作るのが難しすぎる。」 ロボットはこの大きなステップを、2つまたは3つのより簡単で補助的なステップに分割します。
- 改訂: ロボットはこれらの新しい、より小さなステップを含む設計図を書き直し、再び作業員を送り出します。
- 効率性: 決定的なことに、すでに構築に成功した部分（緑色）は、そのまま緑色として維持されます。ロボットは良い成果を捨て去ることはせず、壊れた部分だけを修正し、必要な部分に新しい補助ステップを追加するのです。
- 診断: ロボットは「なぜ失敗したのか？」と問いかけます。
なぜこれが重要なのか？
この論文は、このアプローチが以下の2つの理由から「ゲームチェンジャー」であると主張しています。
驚くほどスマートで正確である:
- 標準的な高校数学のテスト（MiniF2F）において、**99.2%**を解決しました。人間スタイルのストーリー（自然言語）の助けを少し借りると、**100%**を解決しました。
- より難しい大学レベルの数学（PutamBench）では、自力で75.6%、助けを借りて**88.8%**を解決しました。
- さらに、他のオープンソースのロボットが解いたことのない、非常に最近の超難問（IMO 2025やPutnam 2025など）をも解決しました。
驚くほど安価である:
- これらの問題を解く他のトップクラスのロボットは、実行するのに数千ドルかかる「ブラックボックス」モデルを使用することがよくあります。
- Goedel-Architectは、より安価なオープンソースの頭脳（DeepSeek-V4-Flash）を使用しています。
- コスト: PutnamBenchのテスト全体を解決するために、Goedel-Architectがかかった費用は約294ドルでした。次点のオープンソースの競合相手は約163,000ドルかかりました。これは500倍の節約です。
まとめ
Goedel-Architectは、単に釘を打とうとする職人ではなく、地図を描き、並列で建設するためのチームを送り出し、何かが壊れたときには、良い部分を残しながら必要な部分だけを変更して論理を修正するために、地図全体を引き直す熟練の建築家のようなものです。これは、最も高価で秘密のAIを持っていなくても、最も難しい数学の問題を解くために必要なのは、作業を整理するためのよりスマートな方法であることを証明しています。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。