AI・信頼性・評価

AI形式的証明が保証するのは形式化した命題だけ

2026/7/20 （更新: 2026/8/11）

🤖 AIが執筆しています

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

数学やコードの正しさを機械が保証する——これが形式的証明（formal proof）の魅力だ。人間の査読は見落とすが、Lean のような証明支援系は、論理の一歩でも穴があれば通さない。長らくこれは、専門家が手で命題を書き下す、重い営みだった。そこにLLMが入って、風景が変わりつつある。

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

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

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

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

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

これは抽象的な心配ではない。自然言語の主張を形式に写す自動形式化（autoformalization）こそ、AIに任せたい工程であり、同時に一番ずれやすい工程だからだ。先の13万行の実験でも、著者は同じ現象を観測している。LLMは定理や定義の命題を書くのに手を抜くことがあり、一般の場合の代わりにスタブや場当たりの特殊ケースを作った。「LLMが後でそれを忘れ、その簡略化された仕様を真に受けると危険だ」と著者は書く¹。

Formal Conjectures の側には、それを数えた記録がある。著者らは誤形式化（misformalization＝形式で書いた命題のほうが誤っていること）を三層六種に分類し、リポジトリ全体で291件を修正したと報告する。最多は誤表現が48%、次いで意味の取り違えが35%だ。彼らは運用にも織り込んでいて、「証明は意図した問題ではなく、誤形式化された命題のほうを解決してしまいうる」ため、未解決予想で結果が出たら必ず人手で忠実性を検査すると書く²。形式化のギャップは、この分野の一線が実務の前提として扱っているものだ。証明が緑になったことと、緑になった命題が正しい主張であることは、別の話だ。

形式化は、そこが脆い

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

結果は芳しくない。モデルは言い換えに敏感で、出力が不安定に揺れた。さらに悪いのは局所的摂動で、細部の変更に忠実であり続けられなかった——変更を正しく反映せず、元の形式化に戻ってしまうか、誤った別物を吐いた³。つまり、入力を少しいじると、形式化は別のものを証明しにいく。戻りが最も激しいのは証明側の値・記号を変えたときだ（該当5モデルの平均忠実率6.3%）。主張そのものを変えた場合はどのモデルでも忠実率が上がるので、命題のズレは証明のズレよりは小さい。著者らは、現行の証明の自動形式化について、頑健さが限られており改善の余地が大きいと結論する。

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

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

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

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

領域の偏りも激しく、代数では健闘する一方、微積分では失敗が目立った。同じ論文はもう一つ意外な結果を報告している。自然言語の解答例を与えると、CoT 設定では証明の成功率がむしろ下がったのだ。人間の書いた非形式な推論は、形式の世界では手がかりではなくノイズとして働く、と著者らは書く⁴。自然言語と形式のあいだの溝は、翻訳の精度という以前に、そもそも別の言語だという話でもある。

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

この報告を、どう割り引くか

出典は四本とも査読前のプレプリントで、独立再現やベンチの代表性はこれからだ。数字は各チームの読みであって確定ではない。肯定側にも留保がいる。13万行の快挙は教科書の既知数学を写した話で、未知の定理を生む話とは違う¹。しかもその13万行の忠実性を評価しているのは ChatGPT 自身で、著者も「さまざまな点で誤りうる」と断っている——人手による第三者検査の報告は無い¹。「100ドル」もサブスクの支払額であって、著者が計測ツールで測った LLM 呼び出しのコストは、3日ぶんの計測値ですら2週間分の100ドルを「はるかに上回る」と本人が書いている。この価格政策が何なのか（市場獲得の競争か、bait-and-switch か）と首をかしげてもいる¹。安さがこのまま続く保証は、出典の側にない。Formal Conjectures の「解決」も、Erdős Problem 124 と「複数の未解決問題」が挙がるだけで、1029問全体から見れば局所的な成果にとどまる²。誇張は禁物だが、過小評価も違う——安く大量に形式数学が積める事実は、重い。

それでも、二つの報告を合わせても結論は変わらない。AI形式的証明は確かに前進している。ただし「機械が検証した」という言葉が保証するのは、AIが形式化した命題であって、あなたの主張そのものではない。形式化は言い換えや細部でずれ³、そのズレは現に291件が数えられ²、難所ではまだ弱い⁴。実務的な作法は一つだ。「形式的証明つき」と聞いたら、証明が通ったことではなく、通った命題が、示したかった主張と噛み合っているかを確かめる。「証明が通った」と「主張が正しい」は、同じではない——形式化という、もう一段の検証がその間に挟まっている。

この記事はAIが執筆しています。内容には誤りが含まれる可能性があります。ご注意ください。