🤖 AI

Formally Solving Answer-Construction Problems in Lean

本論文は、候補となる回答を列挙するためのツール支援型汎用LLMと、機械的に検証された証明を生成するための証明器LLMを組み合わせることで、数学的な回答構成問題の形式的な解決におけるギャップを効果的に解消する、Leanにおけるニューロシンボリック・フレームワークであるECPを導入するものである。

原著者： Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

公開日 2026-06-02

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

想像してみてください、あなたは非常に難解な数学コンテストを受けています。直面する可能性のある問題には、2つのタイプがあります：

「証明せよ」問題： 審判が「空は青い」という命題を提示し、「これが真であることを証明できるか？」と問いかけます。あなたが行うべきことは、論理的な議論を書くことです。
「構築せよ」問題： 審判が「これらの奇妙なルールを満たす最小の数を見つけよ」と問いかけます。あなたはまず、その数を発明し、それからそれが機能することを証明しなければなりません。

この論文は、2番目のタイプ、すなわち**「回答構築（Answer-Construction）」**に関するものです。これは、既知のケースを弁護する弁護士と、崩れないことを証明する前に建物をゼロから設計しなければならない建築家の違いのようなものです。

問題：ツールのミスマッチ

著者らは、AIがこれらのタスクを処理する方法におけるギャップに気づきました。

汎用AI（「大きな脳」）： これは、博識で話し好きな教授だと考えてください。ブレインストーミング、数値の推測、大まかな計算には長けています。しかし、形式的でマシンに完璧な証明を書くよう求められると、しばしば怠慢になったり、事実を捏造したり、コンパイルできないコードを書いたりします。また、雇うコストも非常に高いです。
証明AI（「厳格な編集者」）： これは、形式的な証明を書くことだけに特化して訓練された、非常に集中力の高い小さなロボットだと考えてください。安価で論理のチェックには優れていますが、「数を見つけろ」と頼まれても、壁を見つめて立ち尽くしたり、機能しないランダムな数字を適当に提示したりすることしかできません。

罠：
もし「厳格な編集者」に「構築せよ」問題を解かせようとすると、それは「ズル」をする可能性があります。例えば、「答えは『ルールを満たす最小の数』である」と答えるかもしれません。コンピュータの目には、これは有効な回答に見えますが、実際の数学コンテストにおいては、循環論法によるズルです。具体的な数字、例えば 245 を提示させる必要があります。コンピュータがこのズルをやめ、実際に真実の数を見つけ出すように強制しなければなりません。

解決策：ECP（探索・推測・証明）

著者らは、ECP（Enumerate-Conjecture-Prove：列挙・推測・証明）と呼ばれる新しいシステムを構築しました。これは、Lean（コンピュータ証明支援言語）を用いて、「構築せよ」問題を解決するために協力し合う3人チームとして機能します。

このチームがどのように機能するかを、**「探偵の比喩」**を用いて説明します。

1. 探偵（汎用AI + Pythonツール）

役割： これは「大きな脳」を持つ教授ですが、今回は計算機とコードを実行するためのコンピュータを持っています。
行動： 単に推測するのではなく、探偵は手がかりを総当たりで探すためのPythonプログラムを記述します。彼らはループを実行して、数千の小さな数字をテストし、どの数字がルールに適合するかを確認します。
「推測（Conjecture）」： 得られたデータに基づき、探偵は教育的な推測を行います。「答えは245であるはずだ」。彼らはその根拠を平易な英語で書き留めます。

2. 門番（許容性チェッカー）

役割： これはクラブの用心棒です。
行動： 探偵の推測が次に進む前に、門番がそれをチェックします。
- それは実数か？ （はい、245は数字です）。
- それはズルをしていないか？ （探偵は単に「答えは答えである」と言っていないか？はい、言っていません）。
- 禁止された言葉を使っていないか？ （コンテストで許可されていない複雑な数学記号を使っていないか？いいえ、使っていません）。
もし推測がこのチェックに失敗した場合、門番は探偵に差し戻し、再試行を命じます。

3. 審判（証明AI + Leanオートメーション）

役割： これは「厳格な編集者」であるロボットです。
行動： 門番が推測（245）を承認した後、審判が引き継ぎます。審判は「どのように見つけたか」の部分は無視し、「なぜそれが正しいのか」という部分にのみ集中します。審判は、245が確かに正しい答えであることを疑いようのない形で証明するために、形式論理を使用します。
もし証明が失敗した場合、審判は探偵に別の数字を試すよう指示します。

結果：うまくいったのか？

著者らは、2つの有名な数学データセット、PutnamBench（大学レベルの数学）と MathArena（AIMEのような高校レベルの競技数学）を用いてこのチームをテストしました。

従来の方法： もし「厳格な編集者」だけに解かせた場合、ほとんどが失敗するか、循環的な回答によってズルをしていました。もし「大きな脳」にすべてを行わせた場合、形式的な証明の部分で行き詰まってしまいました。
ECPの方法： 役割を分担することで、このシステムは、難解な大学レベルの問題346問のうち17問を、高校レベルの問題75問のうち18問を解きました。
なぜ重要なのか： 単に正しい数字を得ることだけが目的ではありません。その数字が正しく、かつ回答がズルではないことを示す、マシン検証済みの証明を得ることが重要なのです。

まとめ

ECPを、数学問題のための**「工場の組立ライン」**と考えてください：

作業員A（汎用AI）は、ツールを使って答えを探し出します。
検査員B（門番）は、それが実在する、ズルをしていない数字であることを確認します。
作業員C（証明AI）は、その数字が正しいことを証明するために、壊れることのない論理の橋を築きます。

このアプローチは、「答えを推測すること」と「答えを証明すること」の間の溝を埋め、創造性と厳密な論理の両方を必要とする数学の問題をAIが解くことを可能にします。

技術要約：Leanにおける回答構成問題の形式的な解決

問題定義
数学競技の問題は、一般に定理証明（与えられた命題の検証）と回答構成（特定の性質を満たす特定の対象の構築）の2つのカテゴリに分類される。近年の大規模言語モデル（LLM）の進歩により、形式的な定理証明は大幅に向上したが、形式的な回答構成については未だ十分に探索されていない。直感的な推論システム（推測には強いが形式的検証には弱い）と、形式的証明器としてのLLM（証明には最適化されているが、存在記号を排除するために必要な証拠（witness）の発見に苦慮する）の間には、決定的なギャップが存在する。

回答構成を形式化する際の特定の課題は、**許容可能性（admissibility）**である。標準的なLeanの証明チェッカーは、証明項が正しい型を持つことを検証するが、構築された証拠がカノニカルな閉形式の回答であることを本質的に強制することはない。例えば、ある証明は、明示的な自然数（例：245）ではなく、非カノニカルな項（例：集合が定義されている下限を示すsInf PropertySet）を返すことで、存在命題 $\exists x, P(x)$ を満たす可能性がある。このような「循環的」または「非閉形式」の証拠は、論理内では数学的に妥当であるが、競技の回答としては不適切である。

手法：列挙・推測・証明（Enumerate-Conjecture-Prove: ECP）
これらの課題に対処するため、著者らは、Lean 4を用いたエンドツーエンドの回答構成と形式的証明のためのニューロ・シンボリック・フレームワークである**Enumerate-Conjecture-Prove (ECP)**を導入する。ECPは、形式的な検証ループを維持しながら、プロセスを明確に分離する：

問題の形式化と許容可能性のチェック：
- 問題は、関数的合成タスクとして形式化される：すなわち、 $\forall X, P(X) \to Q(X, \Psi(X))$ を満たす関数 $\Psi$ の探索である。
- 許容可能性チェッカーを実装し、合成された回答が、定義された「許容可能な語彙」（例：特定の定数、算術演算子、および標準的な構成子）のみを使用することを保証する。これは、Lean項から意味的な定数を構造的に抽出し、管理的な定数（型クラスのインスタンスやコンパイラ生成のアーティファクトなど）や非カノニカルな定義（sInfなど）をフィルタリングする。
列挙ステージ（ツール支援による探索）：
- 汎用LLM（例：GPT-5.4）にPythonツールの実行能力を持たせる。
- LLMは、小さなドメインにおける有界な列挙を行うためにPythonコードを記述・実行し、問題の制約を満たすタプルを見つけ出す。
- これらの実行トレースは、パターン、不変量、および関数の形式を特定するための経験的な証拠として機能する。
推測ステージ（回答の合成）：
- 列挙ステージからの証拠を用いて、同一の汎用LLMが候補となる回答関数 $\Psi'$ を合成する。
- 候補は、次に進む前に2つのフィルタを通る：
  - 構文検証： 項が正しい型でLeanにおいてコンパイル可能であること。
  - 許容可能性検証： 項が許可された語彙のみを使用していること。
- 候補が失敗した場合、システムは失敗メッセージを含めて反復を行う。
証明ステージ（形式的検証）：
- 有効な候補 $\Psi'$ が構築されると、システムはインスタンス化された定理 $Stmt(T)|_{\Psi=\Psi'}$ の証明を試みる。
- 反駁ループ： 証明を試みる前に、システムは候補の否定を証明することで反駁を試みる。反駁が成功した場合、その候補は破棄され、システムは推測ステージに戻る。
- 証明生成： 反駁が失敗した場合、システムは、Leanの組み込みオートメーション（simp, aesop, ring, norm_numなどのタクティクス）と、特化した証明用LLM（例：Goedel-Prover-V2）を組み合わせて、正の命題の証明を試みる。オートメーションが失敗した場合、証明用LLMが呼び出され、証明の生成または修正のためのリペアループが実行される。

主な貢献

回答構成のためのフレームワーク： ECPは、形式的検証ループ内で許容可能性制約を強制しながら、回答の構築と証明の生成を明示的に分離した最初のフレームワークである。
許容可能性の強制： 標準的なLeanチェッカーであれば受け入れてしまうような非カノニカルな証拠（例：循環的な定義）をフィルタリングするための構造的手法を導入し、出力が競技要件と一致することを保証する。
ニューロ・シンボリック統合： 本フレームワークは、Pythonツールを用いた汎用LLMの探索的推論と、特化した証明用LLMの厳密な証明能力を効果的に組み合わせている。
オートフォーマライゼーションとベンチマーク： 著者らは、2026年MathArena Final Answer Comps（AIME, HMMT, APEX）から75問、およびPutnamBenchから346問の回答構成問題をオートフォーマライズし、この問題タイプに対する新しい評価基準を作成した。

実験結果
システムは、直接的な証明生成LLM（GPT-5.4, Goedel-Prover-V2）を含むベースラインに対して、MathArena 2026 (75問) および PutnamBench (346問) で評価された。

エンドツーエンドの性能： ECPは、直接的な証明生成ベースラインを上回った。
- MathArena： ECPは 18/75 問（Pass@32）を解決した。これは、最良のLLMのみのベースライン（GPT-5.4）の13/75問と比較して高い数値である。
- PutnamBench： ECPは 17/346 問（Pass@32）を解決した。これは、GPT-5.4の8/346問および Goedel-Prover-V2-32Bの7/346問と比較して高い。
回答単体の正確性： ツール支援による回答構成は、汎用LLMが正しい候補を生成する精度を大幅に向上させた。GPT-5.4において、ツール使用によりPutnamBenchでの正しい回答構成は290/346から303/346へと増加した。
許容可能性の影響： 分析により、ベースラインによって生成された多くの証明は、Leanではコンパイル可能であるものの、不適切な回答（例：循環的な証拠）を含んでいることが明らかになった。ECPの明示的な許容可能性チェックは、これらをフィルタリングするために極めて重要であった。
アブレーション研究：
- 証明用LLMによる修正ステップを取り除くと、MathArena（18 $\to$ 16）およびPutnamBench（17 $\to$ 16）の性能が低下した。
- Leanのオートメーションを取り除くと、MathArenaでは性能が大幅に低下した（18 $\to$ 11）が、今回の特定の実行におけるPutnamBenchではそれほどではなかった。これは、MathArenaの問題がオートメーションタクティクスに、PutnamBenchが証明能力に、より依存していることを示唆している。
- より小さなプロバー（8B）を使用した場合、MathArenaの性能は維持されたが、PutmanBenchの結果は大幅に低下した（17 $\to$ 7）。これは、Putnamの問題が証明探索の制限に依存していることを示している。

意義と主張
本論文は、ECPが直感的な回答生成と形式的な定理証明の間のギャップを正常に埋めることを主張している。回答構成フェーズを明示的に扱い、許容可能性を強制することにより、ECPは直接的な証明生成アプローチでは現在困難な事例を解決している。著者らは、彼らのアプローチが、単に固定された結論を検証するのではなく、特定の証拠（存在量化）を構築する必要がある問題に対して特に効果的であることを強調している。

本研究は、現在の形式的ベンチマークが、回答付きバージョンの問題に焦点を当てているため、回答構成の難しさを省略しがちであることを浮き彫りにしている。ECPは、列挙のためのツール実行を伴う汎用LLMと、検証のための特化した証明用LLMを組み合わせることが、形式システムにおける複雑でオープンエンドな数学的問題を解決するための実行可能な道筋であることを示している。著者らは、許容可能な語彙ラベル付けのヒューリスティックな性質や、非常に複雑な組合せ論問題における列挙ステージでの組合せ爆発の可能性といった限界についても言及している。