MetaとNYUのh1システム、精巧な定理証明ワークフローを低コストで上回る
重要ポイント
- •Meta FAIRとNYUが構築したh1は、精巧な証明スキャフォールドを、永続的なファイル編集、即時のLean 4コンパイラフィードバック、モデル主導のリフレクションからなるシンプルなループに置き換えた。
- •このシステムはGPT-5.5を使用してPutnamBenchで672問中670問、FATE-Xで100点中90点を記録し、エルデシュ問題の変種を含むFormalConjecturesコレクションの未解決問題8件を解決した。
- •DeepMindのAlphaProof Nexusと比較して、h1はエルデシュ問題の解決で76%に対して82.5%の成功率を達成し、成功した証明1件あたりのコストは317ドルに対して121ドルだった。
- •この研究は2022年のMetaの先行研究であるHTPS定理証明器に基づいており、スケーラブルな汎用手法が手作りの手法を上回り得るという「苦い教訓」を反映している。
- •システムの性能は基盤となるフロンティアモデルに大きく依存しており、PutnamBenchがほぼ飽和状態にある中、今後のより意味のある指標は未解決問題コレクションでの成果となる。
Metaとニューヨーク大学の研究者らは、数学の定理証明のために最小限に切り詰めた人工知能システムを構築し、入念に設計されたLean証明ワークフローに匹敵、あるいはそれを上回る成果を、より低いコストで達成した。
h1と呼ばれるこのシステムが提起する主張はシンプルだ。自動定理証明においては、モデルが良好なフィードバックを受けられれば、複雑さよりもシンプルさが勝つということである。
最小限のエージェントループ
この研究はMetaのFAIR研究チームとNYUによるもの。2026年10月25日に公開された論文「h1: A Taste of the Bitter Lesson in Automated Theorem Proving」で、研究者らはh1を、フロンティア大規模言語モデルをLean 4に接続し、検証結果をリアルタイムでモデルにフィードバックする最小限のエージェントループとして説明している。
Lean 4は数学的な議論をコードとして記述するオープンソースの証明アシスタントであり、各ステップは人間のレビュアーではなくコンパイラが検証する。この仕組みでは検証器が最終判断を下し、証明はコンパイルが通って初めて成立する。
ほとんどの自動証明器は、問題を分割し、サブタスクを振り分け、多数の構成要素を統括する事前定義されたワークフローなど、精巧なスキャフォールドで言語モデルを包み込んでいる。h1のフレームワークはそうした機構を省き、代わりにいくつかのシンプルな仕組みに依拠している:
- 永続的なファイル編集により、モデルはステップ間で状態を保持する証明ファイル上で作業する
- 編集のたびの即時コンパイラフィードバックにより、エラーがすぐに表面化する
- リフレクションにより、言語モデル自身の、何が誤っていたかを推論する能力を活用する
論文によれば、h1の性能は主としてLeanとの効率的なインターフェースに由来し、洗練されたオーケストレーションによるものではないという。
ベンチマーク結果
研究によると、h1は複数の形式定理証明ベンチマークで最先端の性能を達成した。北米の学部生を対象とした年次数学コンテスト、ウィリアム・ローウェル・パトナム競技大会の問題から構築されたPutnamBenchでは、GPT-5.5を使用して672問中670問を解答。FATE-Xの評価では100点中90点を記録した。
また、このシステムはFormalConjecturesコレクションの未解決問題8件を解決した。これには、多産な数学者ポール・エルデシュにちなんで名付けられた一連の問いであるエルデシュ問題の変種が含まれる。こうした問題はLeanの形式言語で記述されるため、解決とは文章による議論ではなく、機械検証済みの証明を生成することを意味する。
最も直接的な比較対象はDeepMindのAlphaProof Nexusである。エルデシュ問題の解決において、h1は82.5%の成功率を記録し、AlphaProof Nexusは76%だった。精度の差よりもコストの差は大きく、成功した証明1件あたりh1は121ドルを費やしたのに対し、AlphaProof Nexusは317ドルだった。
数学に適用された「苦い教訓」
論文のタイトルは「苦い教訓(bitter lesson)」を指している。これは、AI研究者リッチ・サットンが2019年のエッセイで提唱した概念で、大規模な計算資源によって駆動されるスケーラブルな汎用手法は、時間の経過とともに特殊化された手作りの手法を上回る傾向があるという考えである。
Metaがこの問題に取り組むのは今回が初めてではない。この研究は、2022年に発表されたHTPSニューラル定理証明器を含むMetaの先行研究に基づいており、アプローチの転換を反映している。従来のシステムはモデルの周囲により賢い探索を構築することに焦点を当てていたが、h1はモデルが検証器と直接やり取りすることに焦点を当てている。
タイミングも重要である。h1の成果はGPT-5.5などのフロンティアモデルに依存しており、優れたPutnamBenchのスコアは同モデルによって達成された。
これが意味するもの
コスト数値はこの研究の最も実用的な部分である。成功した証明1件あたりのコストが317ドルから121ドルに下がれば、そもそもどの問題に取り組む価値があるかという判断が変わる。1回の試行にかかるコストが下がれば、チームはより難しい、あるいはより思案的な予想に対して、より多くの試行を実行できる。結果が機械検証されているという点も魅力の一つである。形式証明の進展は、証明アシスタントがソフトウェアやハードウェア設計の検証にも使われていることから、数学の枠を大きく超えて注目を集めている。
ただしいくつかの留意点がある。ベンチマークのスコアは特定のテストセットにおける性能を示すものであり、PutnamBenchは672問中670問とほぼ飽和状態にあるため、今後最も注目に値する指標は、FormalConjecturesのような未解決問題コレクションでの成果である。また、h1のアプローチは基盤となるフロンティアモデルに大きく依存している。
論文のより広いメッセージは、強力なベースモデルとクリーンな検証器フィードバックの組み合わせが、精巧なスキャフォールドよりも重要かもしれない、というものである。この賭けは、これらのベンチマークにおいて裏付けられた。
出典: CryptoBriefing
