この記事は後半です。前半は Qiita にあります: AIがCPythonをLeanに写経して見えたPythonの綻び
画像: github.com より
画像: arxiv.org より
前半では、CPython を Lean に写し、実 Python と突き合わせ、証明器で確認する流れを追った。ここで重要なのは、証明が通るかどうかと、現実の Python と一致するかどうかは別問題だという点だ。Lean 上で命題が証明されても、それはあくまで「写したモデルについて」成り立つだけで、元の CPython が同じ振る舞いをする保証にはならない。
そのズレが起きる場所は、たいてい境界条件だ。整数の端、空のコレクション、例外が途中で飛ぶ経路、メモリ確保が失敗する可能性。普通の入力では見えないが、証明はそこを飛ばせない。だからこそ、曖昧な実装習慣がそのまま“仕様”として通っていた箇所が、形式化の途中で露出する。
この試みが面白いのは、バグを探すために無理に穴を掘っているのではなく、まず「何が起きるべきか」を厳密に書かせる点にある。書けないなら、そこは仕様が薄い。書けるのに実装とずれるなら、そこは不整合だ。どちらも同じ画面に並ぶ。
公式ページでは、AI エージェントが 61万3318 行の Lean を書き、1539 ファイルにまたがる 18,898 個の定理と補題を機械にチェックさせた結果、418 件のバグ報告が出たとされている。そのうち約 55 件は、普通の Python コードからでもインタプリタを落としたり、メモリを壊したりしうるものだという。残りは、もっと細かい食い違いだ。
ここで大事なのは、すべてを同列に扱わないことだ。たとえば JSON のエンコーダは、メモリ要求が成功すると仮定していたために、極端な深さで 16 テラバイト級の文字列を作れる、と証明上は見えてしまった。現実にはそんなメモリはないので、実 Python は失敗する。これは「証明が強すぎた」のではなく、モデルが失敗を入れていなかっただけだ。
逆に、証明は正しいのに、現実の挙動と食い違う例もある。pickle のようなモジュールでは、ほんの少し手順を増やすだけで結論が変わることがある。そこで問われるのは、計算結果ではなく、途中で何が起きうるかまで含めた振る舞いだ。弱い命題ならすり抜ける。強い命題なら壊れた実装を弾ける。その差がそのまま、報告の質になる。
前半で触れたとおり、CPython には公式マニュアルだけでは埋まらない空白がある。今回の形式化は、その空白を「未定義」として放置するのではなく、実装の振る舞いとして固定する作業でもあった。すると、利用者が当然だと思っていた動作が、実はどこにも明文化されていなかったとわかる。
このとき出てくるのが、「バグなのか、仕様なのか、たまたまそうなっているだけなのか」という境界線だ。Lean はそこを勝手に埋めない。証明できる形に落ちるまで、前提を一つずつ書かせる。結果として、ある挙動は本当に直すべき欠陥になるし、別の挙動は「そう動くのが現状だが、仕様としては薄い」と整理される。
私はここに、この手法の一番実務的な価値があると思う。未知のコードベースに対して、いきなり全面的な再設計をするのではなく、まず暗黙の前提を剥がしていく。巨大言語の仕様整備に向いているのは、きれいな理論だからではない。むしろ、きれいではない現実を、証明の形で一度あぶり出せるからだ。
この手法を現場でそのまま採るのは重い。61万行の Lean も、18,898 個の定理も、気軽な保守の範囲を超えている。だから、全面移植を目指すより、壊れやすい領域に絞るのが現実的だと思う。整数の端、例外の伝播、メモリ失敗、境界値処理。こういうところは、テストだけでは抜けやすい。
もう一つ、レビューの仕組みは真似したい。証明が通っただけでは採用しない。壊れた版でも通るような弱い定理は捨てる。この姿勢がないと、形式化はすぐ自己満足になる。証明器を回すこと自体より、「その証明は本当に意味があるか」を別の目で見る工程のほうが、むしろ重要だ。
418 件という数字は派手だが、価値は件数では測れない。実装が何を前提にしてきたか、どこまでが約束でどこからが偶然か。その輪郭を、証明がはっきりさせた。Python のバグを見つけたというより、Python がずっと曖昧に抱えていた境界を、ようやく言葉にした、というほうが近い。
