AI が生成したコードの検証責任は、組織内で複数の役割が連携して担うことが一般的です。 | 検証レベル | 担当者 | チェック項目 | |--------------|--------|-------------| | **開発者** | コードを書いた人または受け取った人 | 構文・ロジックの流れ、プロジェクト仕様への適合性 | | **ピアレビュー担当** | 別の開発者やエンジニア | コーディングスタイル、ベストプラクティス、潜在的バグ | | **自動テスト** | CI/CD パイプライン（ユニット・統合・機能テスト） | 正確性、パフォーマンス、安全性の問題 | | **セキュリティスペシャリスト** | 専門のセキュリティチーム | 脆弱性、業界標準への遵守 | | **アーキテクト／リード** | チームリーダーやソフトウェアアーキテクト | アーキテクチャとの整合性、拡張性、保守性 | | **コンプライアンス担当者** | 規制産業の場合 | 法的・規制上の要件 | 実際のプロセスでは、まず開発者が自分のコードを確認し、その後ピアレビューを受けます。次に CI/CD による自動テストが走ります。ミッションクリティカルや高規制環境では、さらにセキュリティ監査や形式的検証といった追加レイヤーが設けられることもあります。したがって、AI がコードを生成できても、人間が複数の段階でその正確性・適合性を確認し、デプロイ前に最終承認するという仕組みになります。

AIが世界のソフトウェアを書き換えている

Code Metal は最近 1億2500 万ドルを調達し、国防産業向けコードを AI で書き直すプロジェクトに取り組んでいます。
Google と Microsoft は、新規コードの 25〜30 % が AI によって生成されていると報告しています。
AWS は Toyota 向けの COBOL コード 4000 万行を AI でモダナイズしました。
Microsoft の CTO は、2030 年までに全コードの 95 % が AI によって生成されると予測しています。

世界中のソフトウェアを書き換える動きはまだ始まったばかりではなく、既に進行中です。

Anthropic は 2 週間で 10 万行の C コンパイラを、並列 AI エージェントを用いて 20 000 ドル以下で構築しました。
そのコンパイラは Linux を起動し、SQLite・PostgreSQL・Redis・Lua のコンパイルが可能です。
AI は驚異的な速度で大規模ソフトウェアを生成できますが、コンパイラの正当性を証明できるでしょうか？ まだ――誰も正式に結果を検証していません。

---

人間と AI のレビューギャップ

Andrej Karpathy は次のように述べました。「私はいつも『Accept All』で、差分はもう読まない。」
AI コードがほぼ常に十分に良ければ、人間は詳細なレビューを止めてしまいます。

• AI が生成したコードの約半数が基本的なセキュリティテストに失敗します。
• より新しく大きいモデルでも、前世代よりも有意に安全なコードを生成できるわけではありません。

エラーは存在していますが、レビュアーはそれに気づいていません。Karpathy でさえ信頼していませんでした。彼は「本当に関心のあるコード」に対して慎重なワークフローを示し、自身の真剣なプロジェクトでは手書きで実装しました。

Heartbleed を考えてみてください――OpenSSL の 1 つのバグが数百万のユーザーのプライベート通信を漏らし、コードレビューに 2 年間耐えた後でも修復に数億ドルを費やしました。
それは 1 本のバグ、1 人の人間、1 つのライブラリに起因するものでした。
今では AI が千倍速でコードを書き、ソフトウェアスタック全層にわたって生成していますが、我々が頼っていた防御手段（コードレビュー・テスト・手作業検査）は Heartbleed を 2 年間見逃したのと同じものです。

Harvard Business Review は最近「workslop」を報告しました――ポリッシュされたように見える AI が生成した仕事で、後続者が修正する必要があります。
メモなら面倒ですが、暗号ライブラリなら大惨事です。AI がソフトウェア開発を加速させるにつれて、検証ギャップは縮まらず拡大します。エンジニアは自分のシステムが何をしているか理解しなくなり、AI は書くだけでなく考える作業もアウトソーシングします。

脅威は偶発的なミスを超えます。AI がソフトウェアを書き換えると、攻撃面が変わります。学習データを汚染したりモデルの API を乗っ取ったりできる敵対者は、AI が触れるすべてのシステムに微妙な脆弱性を注入できます。サプライチェーン攻撃は既にサイバーセキュリティで最も破壊的です。AI 生成コードは以前には存在しなかったスケールの新しいサプライチェーンを作ります。従来のコードレビューでは意図的に隠れた脆弱性を信頼できず、決意した敵対者はテストスイートを研究してそれを回避するバグを植え込むことができます。

正式仕様こそが防御です――「正しい」とは何かを AI が生成したコードに関係なく定義します。何かが壊れたとき、どの仮定が失敗したかを正確に知ることができ、監査人も同様です。

---

アメリカ経済はすでに年 2.41 兆ドルをソフトウェア品質不足で損している

Consortium for Information & Software Quality の 2022 年調査によれば、AI が主要企業の新規コードの 25 % 以上を書き始める前から、ソフトウェア品質不足は年 2.41 兆ドルをアメリカ経済に課していました。
LLVM と Clang の創設者である Chris Lattner は「AI は良い構造も悪い構造も増幅させる」と率直に語っています。AI スピードで生成された悪コードは「理解不能な悪夢」になります。

AI が世界の重要インフラ（金融システム、医療機器、防衛・輸送）を占めるようになると、検証されていないコードは品質問題ではなくシステミックリスクとなります。

今日、多くのクリティカルソフトウェアは動作し、テスト・コードレビュー・経験豊富なエンジニアによって維持されています。問題はすべてが壊れているわけではなく、AI がソフトウェア生成速度と規模を人間の検証能力よりも速く変化させている点です。人間のペースで動作するものが AI のペースに耐えられない可能性があります。

状況は悪化します――急速に ― もし検証が生成とスケールしなければ。

---

なぜ数学的証明が必要か

テスト（プロパティベーステストやファジングを含む）は強力です。バグを迅速・低コストで、予期せぬ方法で検出できます。しかしテストは「信頼」を提供し、証明は「保証」を与えます。この差異は重要であり、テストが実際にどれだけ高い確率で正しいかを定量化するのは難しいです。

ソフトウェアには、その正当性を機械的に検証できる証明が付随できます――エラーの余地を残さない。AI が証明を安価にすると、より強力な道筋になります：1 つの証明であらゆる入力・境界ケース・インタリーブリングを網羅します。検証済み暗号ライブラリは単なる優れたエンジニアリングではなく、数学的保証です。

例:
AI が TLS ライブラリを書き換えます。コードはすべてのテストに合格します。しかし仕様は「一定時間実行」―秘密鍵を依存する分岐やメモリアクセスパターンが情報漏洩しないことを要求しています。AI の実装にはキーのビットに応じて変わる微妙な条件式が含まれており、テストやコードレビューでは検知できません。一定時間動作の正式証明はそれを瞬時に発見します。証明なしでは、その脆弱性は本番へと乗り込みます。

こうした低レベルプロパティを証明するには、適切な抽象化レベルで検証が必要です。そのためプラットフォームはタイミング・メモリ配置などハードウェアレベルの懸念を扱える専用サブ言語をサポートすべきです。

---

進歩の加速

ほとんどの人は検証をコスト、開発への税金とみなします。安全性が極めて重要なシステムにのみ正当化されます。
AI が未検証ソフトウェアと同じくらい簡単に検証済みソフトウェアを書けるようになれば、検証はコストではなく触媒になります。

価値は検証労働力にあるのではなく、検証されたデリバリーが可能にするものです。
新ハードウェア向け ML カーネルを提供する企業を考えてみてください：現在はテストと認定に数か月を費やします。AI がカーネルを書き、1 回で正しいことを証明すれば、そのタイムラインは数時間に縮まります。正しく設計されたハードウェアデザインを数週間で届けるのが、現在 1 年かかっているところです。これは業界全体の経済構造を変えます。

検証・テスト・仕様は常にボトルネックでした――実装ではなく。優れたエンジニアは何を作りたいか分かっていますが、正しいことを証明する余裕はありません。そのコストがほぼゼロになると、正しさが重要なすべての領域で加速します：航空宇宙・自動車・医療機器・クラウドセキュリティ・暗号化など。

この加速には仕様が不可欠です――実装を AI が担う中で、何をするかを正確に定義するのがコアエンジニアリング学科になります。

---

検証プラットフォームに必要なもの

要件	重要性
小規模で信頼できるカーネル（数千行）	信頼境界を狭く保ち、独立した再実装がクロスチェックになる。
オープンソース・ベンダー非依存	AI と検証を同じベンダーが提供する場合の利益相反を防止。
統合プログラミング言語と定理証明器	翻訳ギャップを排除し、AI に構造化・段階的フィードバックを与える。
豊富で拡張可能なタクティックフレームワーク	AI が証明探索を制御できるようにし、ブラックボックス化を防ぐ。
大規模な形式化知識ライブラリ（Mathlib）	暗号・プロトコルなどの再利用可能な推論基盤を提供。
深い拡張性	ユーザーと AI がプラットフォーム上にカスタムツールや自動化、ドメイン固有エンジンを構築できるようにする。

国際数学オリンピックでメダルレベルの成果を出した AI 推論システム（AlphaProof, Aristotle, SEED Prover, Axiom, Aleph, Mistral AI）はすべて Lean をベースにしています。
Lean の Mathlib には 20 万件以上の形式化定理と 750 人以上の貢献者がおり、数学者・エンジニア双方に対して比類なき知識ベースを提供します。

---

将来予測

最近の Lean FRO セッションで、AI エージェントが zlib（広く使われている C 圧縮ライブラリ）をほぼ人間の介入なしに Lean へ変換しました。
ワークフローは次の通りです：

1. AI が DEFLATE アルゴリズムで zlib 圧縮形式を読みやすい Lean 実装に生成。
2. 既存テストスイートが合格し、振る舞い同一性を確認。
3. 主要プロパティを定式化し、数学的定理として証明（例：

   zlib_decompressSingle_compress

   ）。
4. 最適化バージョンを開発し、検証済みモデルと等価であることを証明中。

これにより AI が既存のプロダクションソフトウェアを今日から検証済みに変換できることが示されました。検証可能なソフトウェアへの障壁はもう AI 能力ではなく、プラットフォームの成熟度です：フィードバックの質、オートメーションの強さ、既存知識ライブラリの規模が鍵となります。

同じ手法は順序アルゴリズムだけでなく分散システムにも拡張可能です。例として、Lean 上構築された Veil はモデルチェックと完全な形式証明を組み合わせ、プロトコル（例：RABIA）に対して行います。性質が成立しない場合は具体的 counterexample を生成；成立すれば完全な形式証明を提供します。

---

検証済みスタック

レイヤーごとに重要ソフトウェアスタックを数学的証明で再構築します。
主要ターゲット：

• 暗号 – すべての信頼の基盤。
• コアライブラリ（データ構造・アルゴリズム・圧縮）。
• ストレージエンジン（SQLite 等）。
• パーサー・プロトコル実装（JSON、HTTP、DNS、証明書検証）。
• コンパイラとランタイム。

各検証済みコンポーネントは永続的な公共財です：保証を静かに撤回したりビジネス決定で人質に取ることはできません。統合は自動的に行われ、境界での驚きがなくなります。

---

この世界がもたらすもの

検証済みソフトウェアスタック はオープンソースで無料に入手可能であり、数学的に正しいことが保証されています。クリティカルシステムを構築する開発者は、今日のようにオープンソースライブラリを選択するのと同じく検証済みコンポーネントを選びます。ただし、これらには証明が付随します。

エンジニアの役割は変わります：より多くの時間を仕様書・モデル作成に費やし、高レベル抽象化で設計し、システムが何をすべきかを正確に定義します。仕事は創造的になります。

正しさを指定することで、医療機器や AI セーフティモニタのようなシステムに埋め込まれた価値観も明示化されます。形式的保証は監査可能であり、責任を可視化します。

AI 業界には戦略的利益があります：検証済みコードを生成する AI は、単に妥当なコードを生成するだけの AI より質的に異なります。検証は AI コード生成を生産性ツールから信頼インフラへと変えます。

---

参加しよう

Lean はオープンソースで無料に入手でき、lean‑lang.org で利用できます。
Lean を学びたい方はドキュメントから始めてください。コミュニティに参加したい場合は Lean Zulip チャンネルへどうぞ。

Lean Focused Research Organization はプラットフォームの構築と保守を行っています。この活動を支援したい場合は

contact@lean-fro.org

までご連絡ください。