定理証明AI「h1」、単純な反復処理で専門ワークフローに匹敵する結果を報告
日本語参考要約訳
MetaとNYUによる新しい論文は、優れたLeanツールとより多くの計算量を備えた単純なループが、人手で設計した定理証明ワークフローに匹敵するか、上回ることを示しています。 コンピューターで検証できる言語Leanで数学の証明を書くシステムでは、計画を立て、問題を分割する人手設計のワークフローが増えています。性能向上には、より強いモデルや計算量の増加も伴うことが多く、ワークフロー自体の貢献が分かりにくくなります。 研究チームはh1を作りました。モデルに高速なLeanのフィードバックと検索ツールを提供し、検証に失敗するたびに作業を続けさせるループです。計画は押し付けず、各ラウンドの前に進捗の要約だけを引き継ぎます。 投稿者によると、同じモデルを使う比較でh1はPutnamBenchで598問を解き、人手設計のGoedel-Architectの597問を上回りました。問題当たりの費用は1.08ドル対1.47ドルです。インターフェースも依然重要で、Opus 4.8ではh1が難しい代数問題100問中83問を解いたのに対し、Claude Codeは63問でした。
※長文投稿のため、参考訳は概要を最大600字まで表示しています。 元投稿をご参照ください
AINNでは投稿本文・投稿者本人の追記・第三者コメントの全文転載を避け、X公式埋め込みと元投稿への導線を中心に表示します。
AIによる見どころ整理
何について
Meta・NYUなどの研究チームが、Lean 4による検証と振り返りを繰り返す定理証明用の仕組み「h1」を発表しました。証明の分割手順を固定せず、失敗後も進捗を引き継いで作業を続けます。 論文ではPutnamBenchの672問中598問を解き、比較対象のGoedel-Architectは597問でした。問題当たりの費用はh1が推計1.08ドル、比較対象が1.47ドル。h1はDeepSeek V4 Flash、比較側の597問はFlash／Proを使った非形式的証明付きの4試行という条件です。またOpus 4.8を使うFATE-Xの100問では、h1が83問、標準のClaude Codeが63問を解きました。
なぜ注目
専門的な工程を増やす前に、検証と継続の仕組みを比較する重要性を示します。費用はトークンと料金表によるAPI相当の推計で、キャッシュ再利用の仮定も含みます。実支出やあらゆる数学課題での優位性を示すものではありません。
🔰 初学者向け要約
AIに複雑な役割分担をさせる代わりに、証明が正しいか機械で確認し、失敗したら考え直す流れを繰り返す研究です。モデルの能力だけでなく、作業を続けさせる仕組みも結果を左右します。
用語を調べる
公開記事とWeb上の出典をもとに、Geminiが短く説明します。1日5回まで利用できます。