LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
本論文は、非形式的な推論とLeanコンパイラのフィードバックを橋渡しすることで、汎用的な大規模言語モデルが形式的な定理証明において最先端の性能を達成することを可能にするエージェント型フレームワークであるLEAPを紹介しており、2025年パトナム数学競技会の全12問を解破し、新たに提案されたLean-IMO-Benchにおいて特化型システムを大幅に上回る成果を収めている。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
想像してみてください。あなたの前には、複雑な概念を平易な英語で説明でき、素晴らしい物語を語ることができ、困難なパズルを解き明かすことができる、天才的な世界レベルの数学者がいます。しかし、この数学者はプログラミングが非常に苦手です。もしあなたが数学の問題を解くためのプログラムを書くよう頼んだら、一見正しそうに見えるものの、実行しようとした瞬間にクラッシュしてしまうようなコードを書いてしまうかもしれません。
これが、現在の大規模言語モデル（LLM）における数学の現状です。彼らは「非形式的」な数学（それについて話すこと）には驚異的な能力を発揮しますが、「形式的」な数学（Leanのような、たった一つのタイポで証明が壊れてしまう、コンピュータでチェック可能な厳格な言語を書くこと）には苦戦します。
この論文は、この天才的な数学者がようやく完璧なコードを書けるように、**「超有能なプロジェクトマネージャー」**として機能する新しいシステム、LEAP（LLM-in-Lean Environment Agentic Prover）を紹介しています。
LEAPの仕組みを、簡単な比喩を使って説明します。
1. 問題点：「ワンショット」の罠
以前は、AIに定理の証明を依頼すると、まるで一度の呼吸ですべてをやり遂げようとする学生のように、一気に解決策を書き出そうとしていました。もし3ページ目でミスをしたら、全体が失敗に終わります。論文ではこれを「ワンショット形式化（one-shot formalization）」と呼んでおり、難しい問題に対してはほとんど機能しません。
2. 解決策：「設計図」アプローチ
LEAPは、高層ビルを建てるプロセスのように、工程を細分化することでゲームのルールを変えました。
- ステップ1：建築家のスケッチ（設計図）： ビル全体を一度に建てようとするのではなく、LEAPはまずAIに「設計図」を描かせます。これは平易な英語で書かれたハイレベルな計画です。「これを解決するには、まず補題Aを証明し、次に補成立Bを証明し、最後にそれらを組み合わせる必要がある」といった内容です。
- ステップ2：建設作業員（形式的証明）： 設計図が承認されると、AIは計画のほんの一部に対して、実際のLeanコードを書こうと試みます。
- ステップ3：検査官（コンパイラ）： Leanコンパイラは、厳格な建築検査官として機能します。コードをチェックし、もし完璧であれば成功です。もしエラーがあれば、「基礎に亀裂が入っています」といった具体的なメッセージを返します。
- ステップ4：修理屋（自己洗練）： AIは検査官のメモを読み、特定のエラーを修正して、再度試行します。最初からやり直すのではなく、単に穴を塞ぐのです。
3. 秘訣：「メモリマップ」（DAG）
LEAPの最も巧妙な部分は、自分が何をしたかを記憶する方法です。巨大な迷路を解いている場面を想像してください。
- 従来の方法： 行き止まりに突き当たったとき、自分がどこから来たのかを忘れ、時間を無駄にして同じ場所をぐるぐる回ってしまうかもしれません。
- LEAPの方法： LEAPは迷路全体の地図（有向非巡回グラフ、またはDAGと呼ばれます）を描きます。
- もし迷路の一つの枝で小さなパズル（補題）を解いたなら、それを地図に書き留めます。
訳して、もし後で別の枝で同じパズルに遭遇したとしても、二度解き直すことはありません。地図を見て、すでに解決策があることを確認し、それを使用します。 - これにより、AIがエネルギーを浪費して車輪の再発明をすることを防ぎ、そうでなければ永遠に時間がかかるような、極めて大規模で複雑な問題への対処を可能にします。
- もし迷路の一つの枝で小さなパズル（補題）を解いたなら、それを地図に書き留めます。
4. 結果：ゼロからヒーローへ
このシステムは、世界で最も難しい数学の問題を用いてテストされました。
- パットナム数学コンペティション： これは北米の大学生向けの過酷な数学競技会です。2025年、平均的な学生のスコアは120点中わずか2点でした。LEAPは、**100%**の全問題（12問すべて）を解きました。
- IMO-Bench： 著者らは、国際数学オリンピック（IMO）に基づいた新しいテストを作成しました。数学に特化した従来のAIシステムは約48%を解きましたが、汎用AIを使用しているLEAPは**70%**を解きました。
5. 大きな教訓
この論文は、数学のためだけに作られた小さな特化型ロボットを作る必要はないと主張しています。代わりに、汎用AI（あらゆることを少しずつ知っているAI）を取り上げ、そこに優れたワークフロー（設計図、検査官、そしてメモリマップ）を与えることが重要なのです。
このように考えてみてください。完璧なケーキを焼くために、ケーキ作り「だけ」が得意なロボットは必要ありません。ただ、優れたレシピ、厳格な味見役、そして何がうまくいったかを記録するためのノートを与えられた、汎用的なシェフがいればよいのです。LEAPは、そのレシピ、味見役、そしてノートを提供することで、「話し上手」を「完璧な証明者」へと変貌させるのです。
要約すると： LEAPはAIをより賢くしているわけではありません。単に、AIに思考を整理し、自身の作業をチェックし、成功したことを記憶するための「より良い方法」を与えているのです。これにより、これまでの汎用AIでは不可能だった数学の問題を解くことが可能になります。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。