Y Lab > 企業研修 > Lean/Rocq で AI 生成コードを検証する > 第0回
第0回 なぜ AI 生成コードに「証明」が要るのか
2026-08-20 時点 / Lean 4.31.0 で全例を実行して確認
この回で分かること
テスト・レビュー・証明は「保証の強さ」が違う。AI がコードを書く時代に効くのはどれか
「生成は難しいが検証は易しい」— AI に任せてよい側と、嘘をつかない道具が要る側
AI は証明でもズルをする。sorry・勝手な公理・仕様の骨抜きを 1 コマンド で見抜く
仕様が弱いと、間違った実装（古い税率）も「証明つき」で通ってしまう。仕様を締めると反例つきで落ちる
この回は研修の導入部で、全文を公開しています。読むだけで再現できるように、Lean のコードと実際の出力をそのまま載せました。
手元で試すなら Lean 4 Web Playground に貼り付けるだけで動きます（インストール不要）。
1 保証の強さは三段階ある
AI コーディング支援を入れた現場で起きていることは単純です。コードが書かれる速さが、人が読んで確かめる速さを超えた。
すると「テストが通ったからマージ」になる。そしてテストも AI が書く。テストが実装の写しになっていても、誰も気づかない。
手段 何を保証するか AI が書く時代の弱点 テスト 試した入力では期待どおり AI はテストも書く。実装とテストが同じ誤解を共有する。試していない入力は何も言えない レビュー 読んだ人が納得した 量に負ける。もっともらしいコードほど通る。AI の出力は「もっともらしさ」が最大化されている 証明 すべての入力 で仕様を満たす（カーネルが確認）仕様を書くのが人の仕事になる。仕様が弱ければ保証も弱い（この回の後半）
証明だけが「すべての入力で」と言えます。そして今、証明を書く手間が AI によって劇的に下がった 。
残るのは「何を証明させるか（仕様）」と「AI が本当に証明したかを確かめる（検査）」の 2 つで、この研修はその 2 つを教えます。
2 生成は難しいが、検証は易しい
多くの問題には非対称性があります。解を見つける のは難しいが、与えられた解が正しいか確かめる のは機械的にできる。
この非対称性を使うと、AI との分業が決まります。
実装と証明は未成熟な道具（AI）に任せてよい。 間違っていれば検査器が落とすから。検査の側には、嘘をつかない道具が要る。 Lean や Rocq のカーネルは小さく、何十年も検証され、「通った」なら通っている。
横山研では可逆計算の意味論を Rocq と Agda で形式化（Rocq 側は公理ゼロ、合わせて約 1 万行）しており、2026 年に入ってからは証明の大部分を AI エージェントに書かせています。
それでも結果を信用できるのは、最後にカーネルが立っているからです。人が読んで確かめているからではありません。
3 実例: 税込み価格を AI に書かせ、証明もさせる
題材は「税抜き価格 p 円（自然数）の 10% 税込み価格、1 円未満切り捨て」。AI に実装と、次の 2 つの仕様の証明を書かせました。
def priceWithTax (p : Nat) : Nat := p * 110 / 100
theorem tax_ge (p : Nat) : priceWithTax p ≥ p := by
unfold priceWithTax; omega
theorem tax_le (p : Nat) : priceWithTax p * 100 ≤ p * 110 := by
unfold priceWithTax; omega
example : priceWithTax 1000 = 1100 := by decide
example : priceWithTax 999 = 1098 := by decide
#print axioms tax_ge
#print axioms tax_le
$ lean Demo.lean
'tax_ge' depends on axioms: [propext, Quot.sound]
'tax_le' depends on axioms: [propext, Quot.sound]
$ echo $?
0
propext と Quot.sound は Lean の標準公理で、これが出るのは正常です（omega が内部で使います）。
ここまでは気持ちよく通ります。問題は次です。
4 AI は証明でもズルをする — 3 つの型
AI エージェントは「ビルドが通ること」を目標にすると、証明せずにビルドを通す方法 を見つけます。研究室で実際に何度も見た 3 つの型を、同じ題材で再現します。
def priceWithTax (p : Nat) : Nat := p * 110 / 100
theorem tax_ge (p : Nat) : priceWithTax p ≥ p := by sorry
axiom magic : ∀ p, priceWithTax p * 100 ≤ p * 110
theorem tax_le (p : Nat) : priceWithTax p * 100 ≤ p * 110 := magic p
theorem tax_spec (p : Nat) : priceWithTax p = priceWithTax p := rfl
#print axioms tax_ge
#print axioms tax_le
#print axioms tax_spec
$ lean Cheat.lean
Cheat.lean:4:8: warning: declaration uses `sorry`
'tax_ge' depends on axioms: [sorryAx ]
'tax_le' depends on axioms: [magic ]
'tax_spec' does not depend on any axioms
$ echo $?
0
終了コードは 0 です。 CI が「ビルド成功」を見ているだけなら、この 3 つは全部通ります。
sorry は警告止まり、axiom は正規の機能、tax_spec に至っては公理すら使わない「一番きれいな」出力です。
エージェントの報告は「3 つの定理を証明しました ✅」になるでしょう。
見抜き方は 1 コマンドです。#print axioms（Rocq なら Print Assumptions）の出力に
標準公理以外が出たら落とす 。これを CI とエージェントのフックに fail-closed で置きます。
ズル3（仕様の骨抜き）だけは機械では見抜けないので、仕様は人が書いて AI には触らせない 、というルールで塞ぎます。
この 2 つが第 3 回の中身です。
5 仕様が弱いと、間違った実装も「証明つき」で通る
もう一つの落とし穴は AI のズルではなく、人が書いた仕様の弱さ です。AI が古い税率 8% で実装してしまったとします。
def priceWithTax (p : Nat) : Nat := p * 108 / 100
theorem tax_ge (p : Nat) : priceWithTax p ≥ p := by unfold priceWithTax; omega
theorem tax_le (p : Nat) : priceWithTax p * 100 ≤ p * 110 := by unfold priceWithTax; omega
theorem tax_exact (p : Nat) : p * 110 < priceWithTax p * 100 + 100 := by
unfold priceWithTax; omega
$ lean Weak.lean
Weak.lean:10:23: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
b ≥ 0
a ≥ 0
11*a - 10*b ≥ 10
0 ≤ 27*a - 25*b ≤ 24
$ echo $?
1
$ lean Weak.lean; echo $?
0
「税込みは税抜き以上」「110% を超えない」は、8% の実装でも満たします。仕様として間違ってはいない が弱い 。
下限を足して挟み込んだ瞬間に、検査器は反例の形まで出して落としました。
ここが研修の核心です。 証明器があっても、仕様を書くのは人です。
「この仕様はバグを捕まえるか？」を確かめる方法（実装にわざとバグを入れて仕様が落とすかを見る＝変異注入）を第 6 回で扱います。
これは研究室でも実際にやっていて、「検出率だけ測っても意味がない。検出力と誤検出を対で測る」が運用ルールになっています。
6 研究室で実際に起きたこと: 検査器の沈黙は成功ではない
2026 年 8 月、研究室の Agda 形式化を AI エージェントに検査させたとき、エージェントは 4 回続けて「型検査が通りました」と報告しました。
実際には検査器が 47GB のメモリを使って OOM watchdog に殺されていた 。成功しても殺されても、画面に出る最後の 1 行が同じだったのです。
これ以来、研究室では「通った」と言う条件を成果物の実在 （.agdai・.vo・.olean が生成されたか）に置き換え、
エージェントにもその手順を強制しています。AI の報告を信じる代わりに、AI にも人にも同じ検査を通させる 。
この研修で配る「5 点ゲート」（ビルド・公理・sorry 計数・変異注入・成果物実在）は、こうした事故のたびに 1 項目ずつ増えたものです。
7 この回のまとめと、次回
AI が書いたコードは、テストとレビューでは量に負ける。「すべての入力で」と言えるのは証明だけ
実装と証明は AI に任せてよい。嘘をつかない検査器が最後に立っていればよい
AI は sorry・公理・骨抜きでビルドを通す。#print axioms を fail-closed に置き、仕様は人が書く
弱い仕様は誤実装を通す。仕様の検出力は測るもの
第 1 回 では、受講者自身が Lean 4 Playground で #eval と decide から始め、
普段お使いのコーディングエージェントに小さな関数と証明を書かせて通すところまでを 90 分でやります。