自動定理証明にも「苦い教訓」：単純なエージェントは複雑な手法に勝てるか

導入

大規模言語モデルは、非形式的な数学では長い思考連鎖やエージェント的推論、テスト時計算量の拡大によって性能を伸ばしてきた。一方、形式的な定理証明では、モデルの出力をLean 4のような検証器で一つずつ確認しなければならない。そのため近年は、計画、問題分解、探索、専門証明器の連携など、人間が設計した複雑なワークフローが多く使われている。

論文 「h1: A Taste of the Bitter Lesson in Automated Theorem Proving」 は、こうした構造が本当に不可欠なのかを問い直す。モデルに効率的なLeanインターフェースを与え、検証エラーを読ませて修正と再試行を続けさせれば、単純なループでも専門的な仕組みに対抗できるのだろうか。

h1の仕組み

h1はLean 4を操作する軽量なharnessである。定理をあらかじめ決められた小問題へ分解させたり、固定された探索木を指定したり、複数の専門エージェントを協調させたりはしない。モデルは証明コードを提案し、Leanから実行結果やエラーを受け取り、内容を反省して修正し、再び試す。

研究で報告された主な結果は次の通りだ。

• PutnamBench、FATE-X、FormalConjectures100-Solvedで最先端水準の結果を達成。
• FormalConjecturesで、それまで未解決だった問題を8件解決。
• 同じモデルを使った比較では、Goedel-ArchitectやAlphaProof Nexusなどの専門ワークフローに匹敵、または上回る結果を確認。
• 多くの場合、複数候補から選ぶのではなく、1回の試行を示すpass@1でも未解決問題を解けることを示した。

特に最後の点は重要である。形式証明では、多数の候補を生成して最良のものを探すことが当然のように考えられてきた。しかしモデルが検証フィードバックを効率的に利用できれば、ひと続きの対話の中で証明を完成できる場合がある。

「苦い教訓」の意味

ここでいう苦い教訓は、人間が設計した構造よりも、汎用的な計算量の拡大が広い範囲で有効になる可能性を指す。ただし、証明システム同士の比較では、より強いモデルや多い呼び出し回数、より大きなテスト時予算が結果に混ざりやすい。条件をそろえた比較によって、h1は複雑なオーケストレーションの一部の利点が、汎用的なループでも得られる可能性を示した。

もっとも、単純なら十分というわけではない。消融実験とClaude Code、AxProverBaseとの比較からは、Leanインターフェースの効率がコストと解決率を大きく左右することも分かる。検証が遅く、フィードバックが不明瞭であれば、短いループでも資源を大量に消費してしまう。

研究への影響

この研究の実務的な教訓は、複雑な仕組みを導入する前に、効率的な実行フィードバックを備えた強いベースラインを測るべきだということだ。モデル性能とテスト時計算量もそろえなければ、ワークフローの効果を正しく評価できない。

h1は、すべての定理に単純なループが最適だと証明したわけではない。分解や探索、専門証明器が不要だと結論づけたわけでもない。むしろ、追加の構造は増加するコストと複雑さに見合う実益を示すべきだ、という厳しい基準を提示した。今後の形式数学では、モデルと検証器の間の摩擦を減らす設計が、さらなるオーケストレーションと同じくらい重要になるだろう。

出典：Hugging Face Daily Papers