2026-08-20 版 / Lean 4.31 ・ Rocq 9 系で設計
現在、この研修の募集は行っていません。準備中のカリキュラムと第 0 回（無料公開）のみ掲載しています。開講時の案内をご希望の方は
下記までご連絡ください。
AI が書いたコードは信用できない。
しかし AI が書いた証明は、カーネルが通せば信用できる。
コーディングエージェントが書くコードの量は、人がレビューできる量を超えました。
この研修は「読んで確かめる」の代わりに 仕様を書き、AI に実装と証明を書かせ、定理証明器に嘘を弾かせる 実務の型を、
Lean 4（主軸）と Rocq（抽出・実行）で手を動かして身につけます。証明の専門家を育てる研修ではありません。
AI の出力を信用してよい条件を、自分で作れるエンジニアを育てる研修です。
第 0 回を無料で読む
開講時の案内を希望する
こんな課題をお持ちの組織へ
- Copilot / Claude Code / Cursor を導入したが、レビューが追いつかず「動いたからマージ」になっている
- テストも AI が書くようになり、テストが実装の写しになっている（テストが通っても仕様どおりとは限らない）
- 料金計算・日付・状態遷移・入力検証など、間違えると損害が出るロジックを AI に任せたいが踏み切れない
- 「形式検証」に興味はあるが、業務のどこに・どの程度の費用で入るのか見当がつかない
受講後にできること
1. 仕様を命題で書く自然言語の要件を、AI が誤魔化せない形（前提・結論・境界）に落とす。弱すぎる仕様・空虚な仕様を見抜く
2. AI のズルを機械的に弾くsorry・勝手な公理・仕様の骨抜きを #print axioms とビルドの fail-closed 設定で自動検出する
3. 検証を開発ループに組み込むコーディングエージェントのフックに検査器を置き、「通った」と言えるものだけが出てくる運用にする。変異注入で仕様の検出力を測る
この研修の特徴
- 研究室で実運用している方法をそのまま渡す。 横山研では可逆計算の意味論を Rocq・Agda で形式化し（Rocq 側は公理ゼロ、合わせて約 1 万行）、AI エージェントに証明を書かせる運用を 2026 年に入ってから日常化しています。その中で踏んだ事故（検査器が OOM で殺されたのに「通った」と報告された、など）を教材にします
- 「生成は難しいが検証は易しい」という非対称性を軸に据える。実装と証明は未成熟な道具（AI）に任せてよい。嘘をつかない道具（証明器のカーネル）が最後に立っていればよい
- インストール不要で始められる。 前半は Lean 4 Web Playground だけで演習できるので、持ち込み PC の制約が強い企業でも実施可能
- 特定の AI ツールに依存しない。 演習は受講者が普段お使いのエージェントで行えます（デモは Claude Code）
カリキュラム（全 8 回・各 90 分／1 日集中版は第 0〜4 回）
| 回 | 題 | 持ち帰るもの |
|---|
| 第 0 回無料公開 | なぜ AI 生成コードに「証明」が要るのか | テスト・レビュー・証明の保証の強さの違い。AI が sorry で誤魔化す実例と、それを 1 コマンドで見抜く方法。弱い仕様が誤った税率計算を通してしまう実例 |
| 第 1 回 | Lean 4 に触る（Playground） | #eval・decide・小さな関数の定理。AI に関数と証明を書かせて通す最初の体験 |
| 第 2 回 | 仕様の書き方 — 仕様が新しいコードになる | 前後条件を命題に落とす。常に真の仕様・弱すぎる仕様を見抜く。境界（0・上限・空）の扱い |
| 第 3 回 | AI の 3 つのズルと検知 | sorry／勝手な axiom／仕様の骨抜き。ビルドを fail-closed にする 5 点ゲート（ビルド・公理・sorry 計数・変異注入・成果物実在）を配布 |
| 第 4 回 | Rocq 回 — 証明したコードを実行する | Rocq → OCaml 抽出。Lean との使い分け。公理ゼロで形式化した実物（研究室の意味論）を読む |
| 第 5 回 | 業務に近い題材 | 料金計算・日付・状態機械・入力パーサから 1 つ。AI 実装を仕様で縛り、抜け穴を塞ぐ |
| 第 6 回 | 変異注入 — その仕様はバグを捕まえるか | 実装に故意のバグを入れて仕様が落とすかを測る。検出力と誤検出を対で見る |
| 第 7 回 | 限界と運用 | 検証できないもの（IO・性能・浮動小数）。有界全数検査と一般証明の二層。エージェントのフックへの組み込み実演。費用の見積り方 |
第 1 回以降の教材・演習リポジトリ（CI で全例が検証済み）は開講時に受講組織へ提供する予定です。内容は題材に合わせて差し替え可能です。
実施要領（予定）
| 対象 | AI コーディング支援を既に業務で使っているソフトウェアエンジニア／テックリード／QA。プログラミング経験は必須、定理証明の経験は不要 |
|---|
| 人数 | 演習つきのため 1 回あたり 12 名程度まで（講義のみの概要版は人数制限なし） |
|---|
| 形式 | オンサイト／オンライン。全 8 回（各 90 分）、1 日集中（第 0〜4 回）、90 分の概要講演のいずれか |
|---|
| 環境 | 第 0〜3 回はブラウザのみ（Lean 4 Web Playground）。第 4 回以降はローカルまたはコンテナに Lean/Rocq を導入（手順書を提供） |
|---|
| 費用 | 未定（開講時に回数・人数・題材のカスタマイズ量により個別にお見積りします） |
|---|
| 講師 | 横山哲郎（南山大学 理工学部 教授）。可逆計算・プログラム変換・プログラミング言語の意味論。研究成果の形式化（Rocq・Agda）と AI エージェントによる証明生成の運用が専門分野の一部 |
|---|
よくある質問
- Q. 形式検証は学術的で、業務には重すぎませんか？
- A. 「全部を証明する」研修ではありません。損害が出るロジック 1 箇所に仕様を書き、AI に証明を書かせ、落ちたら直させる、という局所的な使い方を教えます。費用が見合う箇所の見分け方も第 7 回で扱います。
- Q. Lean と Rocq、どちらを覚えればよいですか？
- A. 主軸は Lean 4 です（導入が軽く、AI の生成精度も高い）。Rocq は「証明したコードを実行系に抽出する」場面で使い分けます。考え方は共通で、片方ができればもう片方は読めます。
- Q. 社内の AI 利用ポリシーで特定ツールしか使えません。
- A. 演習は受講者の環境のエージェントで行えます。AI が使えない環境でも、講師が生成した出力を検証する形で成立します。
- Q. 自社の題材でやってもらえますか？
- A. 可能です。事前に題材（匿名化したロジックで構いません）を共有いただければ、第 5 回以降をそれで組みます。
現在は募集していません。開講が決まった際の案内をご希望の方は、tyokoyama [at] acm.org（横山）まで、件名に「AI 生成コード検証研修」と書いてメールをお送りください。
内容へのご意見・題材のご提案も歓迎します。
第 0 回を無料で読む →