AIが書いたコード、数学的に証明できるか：Leanとともに行う形式検証の実践
AIコーディングツールが生成したコードの正確性を保証するために、Leanのような証明支援系を活用する半自動形式検証パイプラインとその限界を考察します。
AIコーディングエージェントが作り出したコードを「とりあえず動くから先へ進もう」という姿勢で信頼するのは難しくなっています。コードは実行できても境界条件で失敗したり、セキュリティ不変条件を破る事例が繰り返される中で、テストを超えて数学的証明によって核となる性質を保証しようとする流れが注目されています。結論から言えば、AIが生成したコード全体を自動で証明するレベルにはまだ達していませんが、人間が仕様と不変条件を定義し、AIがLeanのような証明支援系の証明スケッチを生成して検証する半自動パイプラインは現実的な代替案です。ただし、検証ツール自体の信頼性と仕様の誤り可能性まで考慮する必要があるため、形式検証はバイブコーディングの信頼問題を大きく軽減するものの、完全に解消するわけではありません。
AIコーディングがもたらした「証明」への新たな需要
AIコーディングツールは自然言語の要件をもっともらしいコードに変換する能力に優れていますが、出力が常に要件を正確に反映している保証はありません。単体テストと統合テストは入力空間の一部しか確認できず、回帰テストも人間が想定したシナリオを超えることは難しいです。特に決済、認証、データ完全性のように失敗コストが大きい領域では、「テストに合格した」というだけでは不十分で、「すべての可能な入力に対してこの性質が保たれる」という数学的保証が必要です。
こうした背景から、最近注目すべき事例は2026年10月に公開されたOpenAIの内部モデル研究結果です。数学の未解決問題を扱った成果物722編、372まとまりがGitHubに公開され、その多くは証明をLeanで形式化して同時に公開されました。1つの結果にChatGPT Proで約3時間相当の計算が必要だったとされていますが、これはAIが数学証明の形式化を大規模に実行できるというシグナルでもあります。ただし「AIが作った証明はもっともらしく見えても信じにくい」という懸念から、結果の発表だけでなくLean検証の合格が重要な信頼装置として提示された点が目を引きます。
Leanで「証明付きコード」を作るパイプライン
Leanはもともと数学者が定理を形式化して証明するために使っていた証明支援系です。小さなカーネルがすべての証明ステップを再確認する構造のため、カーネルが通過させた証明はその仕様に限って非常に高い信頼性を持ちます。この特性をソフトウェア検証に応用すると、コードとともに「この関数はソートされた結果を返す」「このデータ構造はすべての挿入後も平衡条件を保つ」といった定理を証明できます。
実践で有望なパイプラインは次のように構成できます。
- 開発者が検証対象の関数の仕様と不変条件を先に定義します。
- AIコーディングエージェントが実装コードとともにLeanの定理宣言と証明スケッチを生成します。
- 開発者は定理宣言が元の要件を本当に含んでいるか、前提条件が抜けていないかを確認します。
- Leanカーネルが証明を検査して合格すれば、その性質は以後のリファクタリングでも機械的に保証されます。
例えばソート関数を検証するなら、「結果が非減少順である」と「結果は入力の順列である」という2つの不変条件を同時に証明する必要があります。AIはこの2条件を満たす証明をかなりうまく生成する傾向がありますが、開発者は「本当にこの定理が自分が求めるソートを意味しているか」を検討しなければなりません。仕様が弱ければ些細な性質だけを証明しても検証に合格したように見える可能性があるからです。
実務導入の参入障壁とAIが下げられる部分
形式検証の最大の障壁は仕様の記述と証明に必要な学習曲線です。Leanは依存型理論に基づいているため、一般の開発者には文法と証明戦略が馴染みにくく、小さな関数1つを証明するにもかなりの時間がかかることがあります。また、仕様自体を形式言語に移す作業はビジネス要件を曖昧さなく定義しなければならないため、非常に難しい作業です。
AIはこの点で参入障壁を下げる役割を果たします。証明支援系のエラーメッセージを見て次の証明戦略を提案したり、補題を自動的に見つけ出すことで証明時間を短縮できます。自然言語で書かれた不変条件の説明をLeanの定理の形に変換する下書き作成も、AIが得意とする領域です。ただしここには2つの注意が必要です。第一に、AIが生成した証明スケッチがLeanカーネルを通過したとしても、仕様が元の意図と異なれば意味がありません。第二に、今年の夏にLean検査器自体で「偽」を証明できるバグが複数発見された事例のように、検証ツールの信頼基盤も完璧ではありません。したがって形式検証は「数学的に絶対に正しい」ではなく「ツールと仕様が信頼できるという前提の下で非常に強い保証を与える」と理解すべきです。
開発者がレビューすべき不変条件と仕様の役割
AIが生成した証明とコードをレビューする際に開発者が集中すべき点は、証明そのものよりも仕様と不変条件です。Leanカーネルが通過させた証明は形式的に正しいですが、その定理がビジネス要件を正確に含んでいるか、すべての入力範囲を網羅しているか、隠れた前提条件がないかを人間が確認しなければなりません。例えば「配列インデックスが範囲外にならない」という不変条件を検証するとき、AIが空の配列だけを考慮する前提条件を追加してしまうと、実際の運用環境では意味がなくなります。
実務では不変条件を階層別に分けるのが良いです。データ構造の内部一貫性、関数の事前事後条件、モジュール間の契約、セキュリティ境界条件をそれぞれ別の定理として管理すれば、検証範囲が明確になります。AIはこうした定理のリストをすばやく生成し証明の試行を繰り返せますが、最終的に「この仕様が正しいか」を判断する責任は人間にあります。この過程で仕様変更履歴とレビュー根拠を残しておくと、後でなぜその不変条件を選んだのか追跡しやすくなります。その際、md-logのようなヒューマンインザループレビューアーカイブが実務的に有用です。
形式検証が解決できることと限界
形式検証はすべてのソフトウェア問題を解決するわけではありません。UIの応答性、外部APIとの統合、性能のボトルネックのような非機能要件は定理として表現しにくく、アプリケーション全体の完全な正確性を証明するのは費用対効果が低いです。実用的な適用範囲は、決済ロジック、認証・認可、合意アルゴリズム、データベーストランザクションのようにエラーが致命的なコアモジュールと、アルゴリズムの核となる不変条件が明確な部分です。
AIがこの限界をすぐに変えることはできませんが、適用コストを下げるという点で意味があります。反復的な証明の試行と補題の探索をAIが代行することで、人間は仕様設計とアーキテクチャ決定に集中できます。ただしAIが生成した証明とコードを無批判に受け入れてはいけません。Lean検査器のバグ、仕様の誤り、モデルの自信過剰などが重なると、「検証合格」というラベルがかえって誤った確信を与える可能性があります。したがって形式検証はバイブコーディングの信頼性問題をコアモジュールでは大きく緩和しますが、コードベース全体の完全な正確性保証へ拡張するにはまだ現実的な限界があります。
AIが生成したコードを数学的に証明できるかという問いには、「指定した仕様と不変条件に限っては、できる」と答えられます。LeanとAIを組み合わせれば証明作成コストが下がり、コアロジックの信頼性を既存のテストよりはるかに強く保証できます。しかしその信頼は仕様の正確性とツールの信頼性の上に成り立っているため、人間が不変条件と前提条件を最後までレビューするヒューマンインザループが不可欠です。
参考資料
- 形式化検証とLean：AIはコードセキュリティをアサーションから数学的証明へどう変えるか
- AIが書いた証明はもっともらしく見えても信じにくいという話 ...
- AIが数学証明をLeanに移し「検証合格」と表示されたら、 ...
- 数学モデルの主張を検証するLean証明資料が公開 OpenAIが内部 ...
- 722件のAI生成証明：誰が検証するのか？OpenAI ...
- AIが自ら賢くなる方法 3-3（Stanford CS329A わかりやすく ...）
- AlphaProof Nexus: 数学的証明に取り組む新しいAIツール
- Prakash: 「2年後にはコードを書くことは死んだ技術になる」 — 形式検証が数十年のLinuxレビューで見逃されたバグを発見 — BigGo Finance
- 安価なコード、貴重な信頼：大規模なコードモダナイゼーション - Command Line
- &Truth、コード向けユニバーサル検証マシン構築に7000万ドルのシード資金を調達 – Unite.AI
- LLMは形式ソフトウェア検証をはるかに大規模に実現可能にしている / Anthropic
- 数学を作り直した後、A.I.はコンピュータのバグを根絶できるか？ - The New York Times
よくある質問
- AIが書いたコードをLeanで完全に証明できますか？
- いいえ。Leanは人間が定義した仕様と不変条件に対してのみ証明を検査します。AIが生成したコード全体のすべての性質を自動で証明することは現時点では不可能であり、仕様の正確性は人間がレビューする必要があります。
- Leanとは何ですか？
- Leanは数学の定理やプログラムの性質を形式的に表現し、証明を機械的に検査する証明支援系です。小さなカーネルが証明を検査するため、合格した証明はその仕様に限り非常に強い信頼を提供します。
- 実務で形式検証を導入する際の最大の障壁は何ですか？
- 仕様を形式言語に移し、証明を作成するために必要な学習曲線と時間的コストが最も大きいです。AIが証明スケッチを生成して参入障壁を下げることはできますが、仕様設計の責任は依然として人間にあります。
- AIが生成した証明がLeanに合格したら無条件に信じてよいですか？
- Leanカーネルが合格させたなら、その証明は形式的に検証されたものです。ただし、検査器自体のバグの可能性と仕様が元の意図と異なる可能性があるため、完全な絶対的信頼というより強い保証として理解すべきです。
- バイブコーディングでは形式検証をどこに優先的に適用すべきですか？
- 決済、認証、認可、合意アルゴリズム、データ完全性のようにエラーコストが大きいコアモジュールにまず適用するのが実用的です。UIや外部統合のように不変条件が曖昧な部分は効果が低いです。