AI・信頼性・評価

AIの数学証明はLeanで確かめれば正しい？保証される範囲

2026/7/20 （更新: 2026/10/12）

🤖 AIを使用して執筆

「形式的証明つき」が、本物になってきた

形式的証明（formal proof）を実際に扱うツールが、Lean のような証明支援系である。命題も証明もその体系の記法で書き下す必要があり、書き下しの重さが適用範囲を長く狭めてきた。LLM（大規模言語モデル）にその書き下しを任せる試みが、目に見える量を積み上げ始めている。

象徴的なのが、Josef Urban の実験だ。Urban は、LLMと高速な証明チェッカーの間に単純なフィードバックループを組み、Munkres の一般トポロジーの大部分を自動形式化した。この証明チェッカーは Chad Brown の高階集合論システム Megalodon で、Lean ではない。結果は、2週間で約13万行（累計16万行）、費用はLLMのサブスクリプション料金で約100ドル。Urysohn の補題（3千行）、Urysohn の距離化定理（2千行）、Tietze の拡張定理（1万行超）を含み、定理・補題は1500本を超えた¹。使ったのは市販の ChatGPT や Claude を CLI 経由で回しただけだ。

ただし忠実性の評価は、ChatGPT 自身が選んだ主要30件を ChatGPT 自身が採点したものにとどまり、著者も「さまざまな点で誤りうる」と断っている。人手による第三者の検査は報告されていない¹。100ドルもサブスクの支払額であって、著者が計測ツールで測った LLM 呼び出しのコストは、3日ぶんの計測値ですら2週間分の100ドルを「はるかに上回る」と本人が書いている¹。この価格がどんな事業方針によるのか（市場の奪い合いか、おとり商法か、など）と著者は疑問符つきで書き添えており、安さが続く保証は出典の側に無い¹。そして積み上がったのは教科書に載る既知の数学の形式化であって、新しい定理を生んだ話ではない¹。それでも、形式数学を短期間に大量に積み上げることは、既に個人の規模でできている。

前進は分量だけではない。DeepMind らの Formal Conjectures は、Lean 4 で書かれた2615問の評価基盤で、うち1029問は未解決の研究予想（学習データに答えが無い＝汚染ゼロ）だ³。狙いは「解けるかを測る」だけでなく「解かせる」ことにあり、著者らはこの基盤が既に新しい数学的発見に活用され、未解決の研究予想の解決も含まれると報告する。論文はその中身を名指ししている。Boris Alexeev がこの基盤の形式化を使い、AI証明器 Aristotle で Erdős Problem 124 を証明した。DeepMind の証明エージェントもリポジトリ全体を系統的に評価し、複数の未解決問題を解いたという。ほかに Alexeev と Mixon の仕事を、「その後の数多くの成功」の一例として挙げている。ただし、1029問のうち何問が解かれたかを論文は数えていない。しかも論文の但し書きによれば、Erdős 124 は当初の形式化が誤っていて、意図しない仮定が余分に入っていた。証明はその仮定に依らずに通ったという。採点の道具から発見の道具へ踏み出しつつあるのは確かだが、その幅を測る数は論文には無い。

だが、保証するのは「形式化した命題」だけ

ただし、注意点がある。形式的証明の保証には但し書きがついて回る。この但し書きは証明支援系のコミュニティが古くから明示してきたもので、目新しい暴露ではない。機械が検証するのは、形式言語で書かれた命題 P が証明できる、という事実だけだ。あなたが本当に示したかった主張 Q と、その形式化 P が一致している保証は、機械の側には無い。P が Q より弱ければ、証明は通るのに、Q については何も言えない。P が弱くなるのは、形式化が仮定を余分に足す、範囲を狭める、自明な場合に置き換える、といった場合である。「機械検証済み」という言葉は、この形式化のギャップまで保証したかのように聞こえる。

この区別は、評価指標の設計にそのまま現れている。ある研究は、Lean のコンパイルが通ることを「与えられた形式命題に対して形式証明が正しいことを形式的に保証する」ものと定義し、その形式命題が自然言語の主張と噛み合うかを別の指標として切り出した²。機械が答えられるのは前者だけだ、という設計上の割り切りである。

これは抽象的な心配ではない。自然言語の主張を形式に写す自動形式化（autoformalization）は、AIに任せたい工程であり、同時に最もずれやすい工程だからだ。先の13万行の実験でも、著者は同じ現象を観測している。初期には、LLMが定理や定義の命題を一般の場合で書かず、スタブや場当たりの特殊ケースで済ませることが時折あった。「LLMが後でそれを忘れ、その簡略化された仕様を真に受けると危険だ」と著者は書き、注意を促すプロンプトで対処し、一、二度は不正確さを洗い出す専用のプロンプトも使ったという¹。

形式化のずれを数えた記録は、Formal Conjectures の側にある。著者らは誤形式化（misformalization＝形式で書いた命題のほうが誤っていること）を三層六種に分類し、リポジトリ全体で291件が修正されたと報告する。最多は量化子の誤りや仮定の落としといった主張の写し損ねで48%、次いで Lean の型や演算子の約束事の見落とし（自然数が0を含む、など）が35%だ。ただしこの291件は、AI に任せた形式化だけの数ではない。初期の寄稿は全て手書きで、最近の寄稿の大半が AI のツールを使っており、表は両者を分けていない。うち16件は、形式化の手違いではなく元の文献の側の誤りに由来する³。

彼らは運用にも織り込んでいて、「証明は意図した問題ではなく、誤形式化された命題のほうを解決してしまいうる」ため、未解決予想で結果が出たら必ず人手で忠実性を検査すると書く。AlphaProof などが証明や反証を試みた結果を人が調べると、見つかるのは主に誤形式化のほうだという。易しい特殊ケースが反証されれば、定義の書き違いを疑う手がかりになる³。機械はズレが無いことを保証しないが、ズレを探す手がかりは出す。

形式化は、そこが脆い

その脆さを正面から測った研究がある。Gui らは、証明の自動形式化が不完全な入力にどれだけ頑健かを初めて体系的に評価した²。miniF2F と MATH-500 を土台に、7つのLLMベースのモデルを、二種類の摂動にかけた。大域的摂動（同じ証明を別の言い回しに書き換える）と、局所的摂動（値や証明の一手を変える）だ。

結果は芳しくない。モデルは言い換えに敏感で、出力が不安定に揺れた。さらに悪いのは局所的摂動で、細部の変更に忠実であり続けられなかった。モデルは変更を正しく反映せず、元の形式化に戻るか、誤った別物を出力した²。つまり、入力を少し変えると、形式化は別のものを証明しにいく。戻りが最も激しいのは証明側の値・記号を変えたときだ（形式化専用の2モデルを除く5モデルの平均忠実率6.3%）。主張そのものを変えた場合はどのモデルでも忠実率が上がり、命題のズレは証明のズレよりは小さい。それでも、素の入力で命題の一致率が最も高い Gemini-3.1-Pro は、主張の数値や記号を変えても、見分けのついた出力の7〜8割台で元の主張の命題を書いた（変更を反映したのは14〜27%）²。著者らは、現行の証明の自動形式化について、頑健さが限られており改善の余地が大きいと結論する。

もっともこの論文は、命題の側のズレも直接測っている。形式化した命題が自然言語の主張と意味的に一致する率（StmtSC）は、摂動をかけない素の入力でも最良の Gemini-3.1-Pro で82.0%（miniF2F）・81.4%（MATH-500）にとどまる。残る6モデルは miniF2F で38〜74%、MATH-500 で29〜58%だった。うち4つは証明を作る専用モデルを形式化に転用したもので、形式化のために作られた2モデルは MATH-500 で5割前後だった²。「命題のズレは証明のズレより小さい」は、「命題なら大丈夫」という意味ではない。形式化のギャップは、理屈だけでなく実測でも開いている。

ただしその実測でも、Lean が機械検証しているのは型検査だけで、意味が元の主張と合うかの判定は LLM（Gemini-2.5-Flash）が下している。もっとも、著者らはこの LLM ジャッジを人手のアノテーション100件と照合し、命題側で94/100・Cohen の κ=0.88 だったと報告している。残る留保は、各モデルの出力が1入力1サンプル（Pass@1）であることだ²。

人の目で測った記録もある。証明探しのベンチマーク FormalMATH を作った著者らは、Lean のコンパイルを通った自動形式化の命題のうち、複数の LLM が全員で意味の一致を認めたものだけを残し、否定が証明できてしまう命題も除いた。それでも、国際数学オリンピックのメダリスト級の専門家12人が意味の一致を照合すると、残ったのはその72.1%だった（集めた問題全体に対する割合で30.1%から21.7%へ）⁴。

そして、難所ではまだ弱い

証明を作る力そのものにも天井がある。FormalMATH は、高校オリンピアドから学部レベルまでの5,560問を、代数・応用数学・微積分・数論・離散数学など多領域で測るベンチマークだ⁴。研究レベルの未解決問題を測るものではない。論文公開時（2025年5月）の最良は、実用的なサンプリング予算（pass@32）で成功率16.46%だった。その後、DeepSeek-Prover-V2-671B が同じ予算32で28.31%を記録している。ただしその記録は2025年5月22日付で、論文公開のわずか17日後のものだ。公式リーダーボードには、それ以降の登録が無い（2026年9月確認）⁴。しかも16.46%は7Bモデル、28.31%は671Bモデルの値で、同じ7B同士なら22.41%にとどまる。

とはいえ、全体集合の表だけでは、その後の伸びは読めない。後続の研究には、全体集合の他の問題が学習に使われたとして、評価専用に取り分けた425問の部分集合（FormalMATH-Lite）で測るのを標準の慣行とするものがある。この部分集合は、既存の証明器 DeepSeek-Prover-V1.5-RL で解ける問題と解けない問題を半数ずつ選んで作られている⁴。pass@32 での最良は FormalMATH の公開時点で既に48.94%（7Bの Kimina-Prover）で、2025年10月には7Bの証明器が53.8%を報告した⁴⁵。部分集合の値は、全体集合の値と直接は比べられない。

全体集合では、領域の偏りも激しく、代数では健闘する一方、微積分では失敗が目立った。同じ論文はもう一つ、直感に反する結果を報告している。二つの証明器で比べると、自然言語の解答例を添えた CoT は、添えない CoT よりわずかに成功率が低かった（部分集合 FormalMATH-Lite、K=3200 で0.5〜1.4ポイント）。ただし CoT を使わない生成よりは高かった⁴。著者らは要旨で、人間の書いた非形式な推論が形式の設定では手がかりよりノイズになると述べる。本文では、その原因を、非形式の推論と Lean の戦術の空間のずれに求める仮説を立てている⁴。この仮説どおりなら、自然言語と形式のあいだの溝は、翻訳の精度だけの問題ではない。

研究レベルの未解決問題では、成功率の天井をまだ読めない。Formal Conjectures の凍結サブセット FC100OpenSet1（未解決の研究予想100問）では、AlphaProof も DeepMind の証明エージェントも0%のままだ³。ただ、この0%には定義上の要素がある。タグ付けの時点で形式証明が存在しない問題を集めたサブセットなので、出発点がそもそも0%なのだ。同じ論文は、その証明エージェントがリポジトリ全体では複数の未解決問題を解いたとも書いている。既解決の100問（FC100SolvedSet1）でなら、AlphaProof が45〜50%、証明エージェントが66%に届く。難所の手前と難所とで、景色がはっきり違う。

この記事はAIを使用して執筆されました。内容には誤りが含まれる可能性があります。事実や数字の出典は脚注から確かめられます。