はじめに

この記事は、次の2つの記事の間にある問いを、対話形式で丁寧に掘り下げるものです。

Pythonの型ヒントの限界を超える「篩型」入門 ―― "x > 0" を型に書くと何が起きるのか（LiquidHaskell・F*・Typed Racket・Idris 2 への誘い）
AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中する

前者の記事では、篩型（refinement types）や依存型（dependent types）について解説しました。さらに、 Lean 4・Coq・F* といった証明支援系の言語が、コードの正しさを機械的に証明できることを取り上げました。

後者の記事では、AI Agent が生成したコードは、もっともらしく動いているように見えても、人間の設計者・開発者・運用者が意図した仕様から逸脱している可能性があると述べました。

これら２つの記事の間には、次の問いが横たわっています。

形式証明を使えば、AI Agent が生成したコードが「人間の意図通りに動いているか」を判定できるのだろうか？。

この記事では、上記の問いに向き合ってみたいと思います。

この問いを、学部生のタロウくんが、専任講師のもとを訪ねて問いかけます。
以下、対話形式でお届けします。

なお、この記事で「仕様」と言うとき、それは人間が自然言語や数理的記述によって外部化した要求全体を指します。

自然言語で書かれた要求仕様
Lean 4 や Rocq（旧称・Coq）や F* のような証明支援系の言語で書かれた形式仕様
その中間にある半形式的な仕様など

「仕様」という言葉は、少なくともこの記事では、上記のすべてを包含する広い意味で用います。

対話の始まり

タロウくん
先生、少しお時間よろしいですか。先日読んだ Qiita の記事で、少し気になったことがあります

専任講師
もちろん構わないよ。掛けていいよ。何の記事だい？

タロウくん
篩型についての入門記事と、AI Agent についての記事の２本です。
同じ著者の方が書かれていて、両方とも興味深く拝読しました。

専任講師
ああ、Etale Cohomology さんの記事だね。私も読んだよ。

タロウくん
はい、その２つの記事を読んでいて、どうしても分からない点が出てきたのです。
それが、次の問いです。

タロウくん
形式証明を使うと、『人間が意図した仕様通りに動いている』かどうか判別できますか？

専任講師
いい問いだね。
その問いは、形式手法の世界で長く議論されてきた問いの核心にある。

タロウくん
そんなに深い問いなのですか？

専任講師
そうだ。

結論から言うと、答えは 「条件付きで、はい」 だ。

ただし、ここには注意すべき点がある。

Correctness と Appropriatenessという２つの概念を正しく識別することだ。
両概念を混同してしまうと、形式証明の本当の力と、その限界が見えてこない。

タロウくん
その２つの概念の境界について、教えてください。

専任講師
その境界を掴むためには、まず一つ、下ごしらえが要る。

AI Agentが生成したコードが、人間の意図通りに動くまでには、実は４つの段階がある。

この４段階を頭に入れておくと、Correctness と Appropriateness の境界が、解像度高く浮かび上がってくる。

順に見ていこう

4つの段階の整理

専任講師
AI Agent が生成したコードが、人間の意図通りに動くまでには、実は4つの段階がある。順に見ていこう

専任講師
まず、次の4段階だ

段階	誰が担うか	形式証明で保証できるか
① 人間が何をしたいか考える	人間が決める	❌
② 仕様を書く	人間が決める	❌
③ 実装が仕様を満たす	機械が担える	✅ 形式証明で証明できる
④ コンパイラや証明器が証明を検査する	機械が担える	✅ 機械的に保証できる

タロウくん
先生、少し腑に落ちない箇所があります。
④の「コンパイラや証明器が証明を検査する」の部分です。

③で「実装が仕様を満たす」ことを形式証明で証明できる、とありました。

しかし、④で急に「証明を検査する」と出てきます。
証明を作ることと、証明を検査することは、別の営みなのですか？

専任講師
いい嗅覚だね。ここは、形式証明を初めて学ぶ人が、ほぼ全員つまずくところだ。
順に説明しよう。

専任講師
まず、③と④は、実は別の営みなんだ。

専任講師
③ ── 「実装が仕様を満たす」を形式証明で示す。

これは、Lean 4 のようなプログラミング言語の中で、「この実装は、この仕様を満たす」という主張の証拠をデータとして構築する営みだ。

この「証拠のデータ」のことを、証明（proof） と呼ぶ。

専任講師
証明を作ることは、実は、プログラミングと極めてよく似た創造的な営みだ。

人間（あるいは AI Agent）が、頭を使って、証明を組み立てる。
これは、機械には完全には自動化しきれない創造的な仕事の側面を持つ。

専任講師
④ ── 「コンパイラや証明器が証明を検査する」。

他方でこちらは、機械が担うべき役割だ。

③で作られた証明のデータが、形式的なルールに従って正しく組み立てられているかを、機械が一つ一つ、機械的にチェックする。

これを、証明検査（proof checking） と呼ぶ。

専任講師
面白いのはね、証明を作ることは創造的だが、証明を検査することは機械的だ、ということだ。

機械は、証明を「思いつく」ことは、まだ得意ではない。

しかし、既に書かれた証明が正しいかを、機械的に検査することは得意だ。

Lean 4も、（旧称）Coqも、F* も、この「証明検査の機械化」を正確且つ高速に行ってくれる。

専任講師
この構造には、深い理由がある。

証明を作るのは、無数の可能性から一つを選ぶ、探索の営みだ。

その一方で、証明が正しいかを検査するのは、決まったルールに従って一つ一つ確かめる、機械的な営みだ。

両者は、複雑さのレベルが根本的に違う。

タロウくん
なるほど。③と④は、それぞれ別の営みで、③は創造的、④は機械的、ということですね。

そして、④が機械化できることが、形式証明の実用性の根本にあるのですね。

専任講師
その理解でほぼ正しい。

この構造は、AI Agent の時代においても、大きな意味を持つことになる。

AI Agentは、証明を「作る」ことにも、少しずつ手を出し始めているからだ。

でもね、AI Agent が作った証明が正しいかを最終的に保証するのは、あくまで機械的な証明検査だ。
これが、AI Agent の時代における形式証明の、独特の強さでもある。

タロウくん
AI Agent時代に、形式証明が担うべき社会的な役割も変わりつつあるんですね！

先ほどの表で、①と②は人間が決めることで、③と④は機械が担えるという整理の仕方も、納得がいきました。

専任講師
この４段階を、一本の流れとして書くと、こうなる

専任講師
形式証明が保証してくれるのは、この流れの下半分だけだ

専任講師
具体的には、「プログラム ⇒ 仕様」の関係、つまり「プログラムが、書かれた仕様を正しく満たしていること」 は、Lean 4・Coq・F* といった形式証明言語が厳密に保証してくれる

専任講師
しかし、**「仕様 ⇒ 人間の本当の意図」の関係、つまり「書かれた仕様が、人間が本当に望んでいたことを正しく表現していること」**は、形式証明では保証できない。

なぜなら、形式証明言語には、そもそも人間の意図を読み取る手段がないからだ

タロウくん
なるほど。

形式証明は、「仕様通りにコードが動くこと」は保証してくれるけれど、「仕様が人間の本来の意図を正しく表しているか」は保証してくれない、ということですね？

専任講師
その理解でほぼ正しい。

Correctness と Appropriateness

専任講師
この点、形式手法の世界では、昔から次のように言われている

専任講師
Correctness ≠ Appropriateness

タロウくん
correctness と appropriatenessですか？

専任講師
そうだ。日本語に訳すと、こうなる

Correctness（正しさ）： 実装コードが、書かれた仕様の通りに動くこと
Appropriateness（適切さ）：書かれた仕様が、本当に人間が欲しかったものであること

専任講師
補足しておくとね、形式手法の専門的な用語では、Correctness とは 「実装が形式仕様を満たしていること」 を指す。

「仕様通りに動く」というのは、その平易な言い換えだ。

専門書でCorrectness という語に出会ったときは、この定義 を思い出すといい

専任講師
そして、この２つは、全く異なる概念だ。

しかし、多くの人がこの２つを混同してしまう。

「コードが仕様通り動く」ことと、「そのコードが人間の望みを叶える」ことは、別の話だ。

タロウくん
冒頭で挙げたAI Agentの記事の主張とつながりますね！

専任講師
まさにそうだ。

あの記事で述べられていた 「AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう」 という主張は、形式手法の世界で長年議論されてきた、この Correctness と Appropriateness を互い区別すべきだという認識と互いに通底している。

Lean 4 で何が証明できるか

タロウくん
具体的に、Lean 4 では何が証明できるのか、例を見せていただけますか

専任講師
もちろん。

ソートのアルゴリズムを例に見てみよう

専任講師
たとえば、君が「整数のリストを昇順にソートする関数 sort を書いてくれ」と AI Agent に依頼したとする。

AI Agent は、次のようなコードを提示してくるだろう

# Python での例
def sort(xs: list[int]) -> list[int]:
    return sorted(xs)

タロウくん
これは、Python の組み込みの sorted を呼び出しているだけですね。
たしかにこのコードは動きます。

専任講師
ここで問いを一つ立てよう。

このコードは本当に 正しく 動くだろうか？

タロウくん
テストで確かめれば良いのではないでしょうか。

専任講師
テストで、いくつかの入力については確かめられる。

しかし、あらゆる入力について、この関数が本当に正しく動くと保証するには、テストではなく形式証明が必要だ。

専任講師
Lean 4 では、次のような証明を書くことができる

theorem sort_correct (xs : List Int) :
    Permutation xs (sort xs) ∧ Sorted (sort xs)

専任講師
実際にはこの後ろに証明（proof term または tactic）が続き、Lean はその証明を機械的に検査する。
ここでは紙面の都合で証明の中身は省略している。

専任講師
この定理は、次の２つを主張している。

Permutation xs (sort xs)
── sort xs は、元のリスト xs の並び替えである（要素を失わず、要素を増やさず、順序だけを変えたものである）
Sorted (sort xs)
── sort xs は、昇順に並んでいる

タロウくん
Lean 4 のコードは初めて見ますが、なんとなく読めます。
何を意味しているか、教えてください。

専任講師
一緒に読み解いてみよう

専任講師
theorem sort_correct は、この定理に sort_correct という名前をつけている宣言だ。
Pythonでいえば、関数名をつけているのに近い。

専任講師
(xs : List Int) は、この定理が「任意の整数のリスト xs について成り立つ」ということを言っている。Python の型ヒントの xs: list[int] に相当する。

専任講師
そして、コロンの後の Permutation xs (sort xs) ∧ Sorted (sort xs) が、証明すべき命題だ。
∧ は「かつ」を意味する

タロウくん
なるほど。

この定理を Lean 4 で証明できれば、あらゆる整数のリストについて、sort 関数が「並び替えであり、かつ昇順である」ことが数学的に保証される、ということですね？

専任講師
そうだ。
テストで一つ一つの入力を確かめるのとは、根本的に違う保証の強さだ。

専任講師
ここが、形式証明のいちばん美しいところだ。

このたった１行の型定義が、あらゆる入力に対するテストを兼ねている。

テストコードを1万行、10万行書いても、それは有限個の入力を確かめるだけだ。

しかし、この定理を Lean 4 で証明できれば、この世に存在するあらゆる整数のリストに対して、sort 関数が正しく動くことが、一度に、数学的に保証される

専任講師
Lean 4 の型システムは、この定理を証明として構築できたときに限り、コンパイルを通す。

証明が完成しない限り、コードは受け入れられない。

この意味で、Lean 4 は Correctness を厳密に保証してくれる。

タロウくん
「型」 が登場しましたね!

このあたりは、兄貴が、型システム論と関数型言語と形式証明・定理証明器の関係性について、強い興味を寄せているようです。

また別の対話篇で、型システム論との今日の議論の関係性についても、教えてください。

専任講師
いい着眼点だね。

今日の対話で少しだけ触れた依存型理論（Dependent Type Theory） は、実は、その大きな地図の中の一つの峰なんだ。

関数型プログラミング言語の型システム
Curry-Howard 対応
線形型、篩型、依存型

これらは、それぞれ独立した話題のように見えるが、深いところでひとつにつながっている。

そのつながりの全体像を、また別の機会に、腰を据えて話そう。

タロウくん
はい、楽しみにしています!

しかし、Lean 4 に分からないこと

タロウくん
Lean 4 は、Correctness の保証、つまり、実装が仕様を満たしていることの保証について、素晴らしい仕組みを提供してくれるのですね！

専任講師
そうだね。
ただし、ここで一つ、極めて重要な問いが残る。

専任講師
そもそも、「昇順に並べる」という仕様は、顧客の本当の要求だったのだろうか

タロウくん
え？

専任講師
例えば、きみの顧客が「商品のリストを、売れ筋の順に並べたい」と考えていたとしよう。

君は、その要求を「商品リストを、売上高が高い順にソートする」と仕様に書き下ろした。

そして、AI Agent がその仕様を正しく実装するコードを書いた。
Lean 4 でも、そのコードが仕様通りに動くことが証明できた

専任講師
しかし、実は顧客が本当に欲しかったのは「先週の売上高」の順ではなく、「向こう1か月の予測売上」の順だったとしたら、どうだろう？

タロウくん
その場合、コードは仕様通りに正しく動いていても、顧客の本当の意図とは違うものになっています・・・

専任講師
そうだ。

この乖離は、Lean 4 には、原理的に検出できない。

Lean 4 に分かるのは、書かれた仕様と、書かれたコードの関係だけだ。

顧客の頭の中にある「本当の望み」は、Lean 4 の視野の外にある。

専任講師
ここで、少し数学的な背景に触れておこう。

Lean 4 が扱えるのは、依存型理論（Dependent Type Theory） という厳密な形式体系の上に定義された命題と証明だけだ。

タロウくん
依存型理論、というのは何ですか？

専任講師
簡単に言うとね、**「型が、値に依存できる」**という理論だ。

専任講師
Python でも Java でも普通の関数型言語でも、型は「整数」や「文字列」といった、値とは独立に決まる分類だ。

でもね、依存型理論では、**「長さが３の整数のリスト」とか、「正の整数」とか、「ソート済みの整数のリスト」**といった、値の性質そのものを型として書き下ろすことができる。

専任講師
このおかげで、「関数の入力と出力の間の関係」を、型として 厳密に書き下ろすことができる。

例えば、先ほどの sort 関数なら、「入力の並び替えであり、かつ昇順である出力を返す関数」という性質そのものを、型として書き下すことができるんだ。

すると、Lean 4 のコンパイラは、その性質を満たさない実装をコンパイル・エラーとして拒否してくれる。

タロウくん
値の性質を、型として書ける ── これが依存型理論の力ですね！

タロウくん
値の性質を、型として書きあらわすことができる。
これが依存型理論の力ですね。

具体的には、どんなコードになるのですか？

専任講師
うん、いい問いだ。実際のコードを見てみよう。

まず、依存型を扱う代表的な２つの言語 ── Lean 4 と、依存型に特化した関数型プログラミング言語 Idris ── で、「長さが３の整数のリスト」をどう書くか、順に見てみよう。

専任講師
Lean 4 では、次のように書ける。

-- 長さが n の要素型 α のリスト(Lean 4 の Vector 型の定義)
inductive Vector (α : Type) : Nat → Type where
  | nil  : Vector α 0
  | cons : α → Vector α n → Vector α (n + 1)

-- 長さがちょうど 3 の整数のリスト
def myList : Vector Int 3 :=
  Vector.cons 1 (Vector.cons 2 (Vector.cons 3 Vector.nil))

専任講師
一行ずつ読み解こう。

専任講師
inductive Vector (α : Type) : Nat → Type where の行は、
「Vector という新しい型を定義する」 という宣言だ。

(α : Type) は「Vector が要素の型 α を受け取る」ことを示し、
Nat → Type は「さらに自然数 n を受け取って、型を返す」ことを示している。

この「値(自然数 n)を受け取って、型を返す」という性質こそが、依存型の本質だ。

専任講師
| nil : Vector α 0 の行は、
「nil(空のベクトル)は、長さがちょうど 0 の Vector である」 という主張だ。

つまり、空のベクトルの型そのものに「長さが 0」という情報が刻まれている。

専任講師
| cons : α → Vector α n → Vector α (n + 1) の行は、
「cons は、要素 α と、長さ n の Vector を受け取り、長さ n + 1 の Vector を返す」 という主張だ。

要素を一つ足すと、長さの型が自動的に n から n + 1 に増える。

この関係が、型のレベルで厳密に管理されている。

専任講師
そして、def myList : Vector Int 3 := ... の行が、
「myList は、長さがちょうど 3 の Int のリストである」 という宣言だ。

ここで、もし右辺の要素の個数を間違えたら、Lean 4 のコンパイラは即座にコンパイル・エラーを出す。
実行前に、型のレベルで検出されるんだ。

タロウくん
なるほど。
「長さ 3」という情報が、型そのものに埋め込まれているのですね！

専任講師
そうだ。

次に、Idris のコード例を見てみよう。

Idris は、依存型を扱うことに特化した関数型プログラミング言語だ。

Lean 4 は「定理証明系と汎用プログラミング言語の両方」を目指しているが、
Idris は「依存型を持つ実用的なプログラミング言語」の側に軸足を置いている。

-- 長さが n の要素型 a のリスト(Idris の標準ライブラリに Vect がある)
data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

-- 長さがちょうど 3 の整数のリスト
myList : Vect 3 Int
myList = [1, 2, 3]

専任講師
Idris の書き方は、Lean 4 と極めてよく似ている。

Vect : Nat -> Type -> Type の行は、
「Vect は、自然数 n と要素型 a を受け取って、型を返す」という宣言だ。

Z は 0(zero)、S k は k の後継(k + 1)を表している。

そして、myList : Vect 3 Int は、「myList は、長さ 3 の Int のリストである」という宣言だ。

タロウくん
Lean 4 と Idris で、書き方の細部は違うけれど、依存型の考え方は共通なのですね。

専任講師
まさにそうだ。

依存型理論という同じ数学的な土台の上に、Lean 4 も Idris も、Coq(現在は Rocq)も、Agda も、F* が構築されているんだ。

それぞれの言語の顔つきは違うが、根っこの発想は共通している。

専任講師
そして、この「長さ３のリスト」の例は、依存型の一つの応用に過ぎない。

「正の整数」
「ソート済みのリスト」
「特定の性質を満たす関数」

など、値の性質を型として書けるすべての場面で、依存型の力が発揮される。

タロウくん
なるほど。
依存型は、コードの安全性を、実行前の型検査の段階で保証してくれる強力な道具なのですね。

専任講師
その理解でほぼ正しい。

専任講師
ところでね、この依存型理論は、Curry-Howard 対応という、論理学とプログラミングの間の深い対応を通じて、数学の証明そのものをプログラムとして書き下ろせるという驚くべき性質を持つ。

これが、Lean 4 が定理証明系として使える理由だ。

専任講師
でもね、ここに重要な限界があるんだ。

依存型理論という形式体系の中に書き下ろせるのは、あくまで形式的な命題と証明だけだ。

**「顧客が本当に望んでいたこと」**という、**まだ数式や型として定義されていない曖昧な概念（非形式的な世界）**を、依存型理論の形式的な世界にマッピングすること 自体は、数学や論理学の力ではどうにもならない

タロウくん
なるほど。

形式的な世界と、非形式的な現実の世界の間のギャップは、形式体系の力ではどうにもならないのですね

専任講師
その理解でほぼ正しい。

これが、Lean 4 が原理的に、仕様と人間の意図のギャップを検出できない、真の理由だ。

３段階の役割分担

専任講師
ここまでの議論を、次の３段階の図として整理できる

専任講師
この3つの段階には、それぞれ役割分担がある

① 論理的に動く ── AI Agent が、比較的得意な領域
② 仕様通りである ── Lean 4・Coq・F* などの形式証明が、強力な武器を提供する領域
③ 人間が本当に望んでいたもの ── 人間が責任を負う領域

タロウくん
なるほど。
それぞれの段階で、担い手が違うのですね。

専任講師
そうだ。
そして、この役割分担こそが、すでに取り上げたAI Agentに関する記事の主張と、深く響き合っている。

専任講師
あの記事の論点２で提示された 「もっともらしい挙動と、人間が意図した仕様の区別」 は、形式証明がまさに埋めようとしているギャップの一部だ。

専任講師
ただし、形式証明でも埋められるのは「実装と仕様のギャップ」であり、「仕様と人間の意図のギャップ」は残る

タロウくんの新しい問い ── 意図を持つとはどういうことか

タロウくん
先生、ここでもう一つ、深い問いが浮かびました。

専任講師
うん、聞かせてくれ。

タロウくん
仕様と人間の意図のギャップがあるかないかをチェックできるのは、意図を持つ人間だけなのでしょうか？

タロウくん
AI Agent も、形式証明言語も、そもそも意図を持たない存在ですよね。

意図を持たない存在には、他者の意図が正しく反映されているかを、原理的に判定できないのではないかと思います。

専任講師
きみ、それは、この分野で最も深い問いの一つだ。

専任講師
順に考えていこう

専任講師
まず、「意図を持つ」とはどういうことか、という問いから始める必要がある

タロウくん
はい。

専任講師
意図を持つとは、少なくとも次の３つの要素を含む。

① 何かを望む（欲求、価値、目的）
② その望みを、外部の記述（言葉、記号、仕様書、コード）に変換する試みを行う
③ 外部の記述が、自分の望みを正しく表現しているかを、内省的に判断する能力を持つ

専任講師
AI Agent は、これらのうち、②の作業は、極めて高度に行える。
人間の指示を受けて、それをコードに変換する作業は、AI Agent の得意分野だ。

専任講師
しかし、現在実用化されている AI Agent は、人間のような主体的な価値判断や目的を、自律的に持つわけではない。

タロウくん
AI Agent には、そもそも「これがしたい」という主体的な望みがない、ということですね？

専任講師
そうだ。

AI Agent が生成するコードは、きみの指示から推測した仕様に対して、正しく動くコードだ。

しかし、AI Agent 自身が「こういうコードを書きたい」と主体的に望んでいるわけではない。
現在実用化されている AI Agent には、人間のような主体的な価値判断や、自律的に選び取る目的や価値観がない。

専任講師
したがって、AI Agent には 「きみの指示を、AI Agent が推測した仕様」と「きみが本当に望んでいたもの」の間に乖離があるかどうかを判定する、根拠となる基準がない。

タロウくん
なるほど。
判定する基準そのものが、AI Agent には存在しない のですね。

専任講師
そうだ。

同じことが、Lean 4・Coq・F* にも当てはまる。

これらの証明支援系の言語は、極めて強力な論理体系を持っているが、そこには「何を望むか」という価値の次元は存在しない

専任講師
Lean 4 は「この定理は、この公理系から導ける」ことを厳密に判定する。

しかし「この定理を証明する意味があるか、この公理系を採用する意味があるか、そもそも何を証明対象にすべきか」は、Lean 4 の視野の外 にある。

タロウくん
つまり、仕様と人間の意図のギャップを判定できるのは、意図を持つ人間だけという私の推論は、原理的に正しかったのでしょうか？

専任講師
その理解でほぼ正しい。── ただし、この結論には、少し補足が必要だ

補足 ── 「意図を持つ人間」とは誰か

専任講師
君の結論は正しい。

ただし、実務の場面では、「意図を持つ人間」が誰なのかが、常に明確とは限らない

タロウくん
といいますと？

専任講師
大きな組織でソフトウェアを開発する場面を考えてみよう。

仕様を書き下ろすのは、プロダクトマネージャーだ。
しかし、その仕様の背後にある「本当の意図」は、その組織の経営者、顧客、あるいはその業界の慣習の中にある。

専任講師
プロダクトマネージャーが書き下ろした仕様が、経営者の意図と一致しているか、顧客の望みと一致しているか、これを判定するのは、プロダクトマネージャー自身ではない。

組織全体の中で、意図を持つ複数の人間が、対話を通じて、少しずつ仕様と意図の一致を確かめていくのだ。

タロウくん
なるほど。
「意図を持つ人間」は、一人ではないのですね！

専任講師
そうだ。

そして、この対話のプロセスこそが、AI Agent には代替できない、人間の役割の核心だ。

AI Agent は、仕様を書き、コードを書くところまでは、高度に手伝ってくれる。

しかし 「組織の意図と、書かれた仕様の一致を、対話を通じて確かめる」作業は、意図を持つ複数の人間が集まって、担うしかない

要求工学という学問

専任講師
ここで、君に一つ紹介しておきたい学問がある。

タロウくん
何ですか？

専任講師
要求工学（Requirements Engineering） と呼ばれる分野だ。

実務では、この「人間の意図と、書かれた仕様の間のギャップを埋める」ために、要求工学という研究分野が長く発展してきた。

タロウくん
要求工学 ── 初めて聞きます。
どんな学問ですか？

専任講師
簡単に言うとね、顧客や利用者や経営者が本当に望んでいることを、正確に掘り起こし、それを仕様として書き下ろすまでの体系的な方法論を扱う学問だ。

専任講師
この学問は、ソフトウェア工学の中でも、実務で最も生々しく重要な分野の一つと位置付けられている。

理由は単純で、現実の大きなソフトウェア開発の失敗の多くは、コーディングの失敗ではなく、要求の掘り起こしの失敗だからだ。

タロウくん
コーディングよりも、要求の掘り起こしの方が、失敗の原因になりやすいのですか？

専任講師
そうだ。実際、Standish Group の CHAOS Report のような有名な調査でも、プロジェクトの失敗の主要な原因として、 「要求の不完全さ」「要求の変化」「利害関係者の関与の不足」 が繰り返し挙げられている。

専任講師
要求工学の中には、いくつかの重要な下位分野がある。
順に紹介しよう。

要求分析(Requirements Analysis)
── 顧客や利用者から集めた要求を整理し、矛盾や欠落を発見し、洗練させていく営み
ステークホルダー分析(Stakeholder Analysis)
── そのソフトウェアに関わる利害関係者(顧客、利用者、経営者、規制当局、運用者など)を体系的に洗い出し、それぞれの立場からの要求を明らかにする営み
ゴールモデリング(Goal Modeling)
── 個別の要求の背後にある「なぜそれが必要なのか」という上位のゴールを、木構造で階層的に整理する営み。KAOS や i* といった記法がある

タロウくん
ゴールモデリング、というのは、要求の背後にある「本当の望み」を掘り起こす作業のことですか？

専任講師
その理解でほぼ正しい。ゴールモデリングでは、例えば「商品リストを売上高順にソートしたい」という要求の背後に、「売れ筋の商品を目立たせたい」というより上位のゴールがあることを見つけ出す。

さらにその上には、「顧客の購入体験を向上させたい」という、もっと大きなゴールがあるかもしれない。

専任講師
こうやって、要求の階層を上へ上へと辿ることで、顧客が本当に望んでいたのは「先週の売上高順」ではなく「向こう1か月の予測売上順」だった、というような気付きが得られる。

この気付きが、仕様と人間の意図の一致を確かめる、決定的な手がかりになる。

タロウくん
なるほど。

仕様と人間の意図のギャップを埋めるための、体系的な学問があるのですね。

専任講師
そうだ。

そして、要求工学は、まさに今日の議論のテーマ
── 形式証明が到達できない「仕様と人間の意図の間」を、対話と方法論で埋めようとする学問なのだ。

専任講師
君が AI Agent 時代の実務者として仕事をするなら、形式手法だけでなく、要求工学の基本的な考え方も、身につけておくといい。

形式手法と要求工学は、AI Agent 時代における人間の役割を、両側から支える二本の柱だからね。

タロウくん
先生、質問があります。

要求工学は、仕様と人間の意図のギャップを埋める人間の営みだと理解しました。

では、AI Agent は、この要求工学の営みの中では、全く役に立たないのでしょうか？

専任講師
いい問いだね。
答えは、そうではない。

専任講師
現在の LLM（Large Language Model）は、意図を持たない存在だ。この事実は変わらない。

しかし、意図を持たないからといって、要求工学の営みの中で無力かというと、そうではない。

専任講師
現在の LLM は、**「ステークホルダー分析」や「ゴールモデリング」**の壁打ち相手として、極めて優秀だ。

人間が「なぜこの機能が必要か」を掘り下げるとき、LLM は、まだ人間が言葉にしていない前提を、質問の形で引き出してくれる。

ゴールを木構造で整理するとき、LLM は、抜けているノードを指摘してくれる。

ステークホルダーを洗い出すとき、LLM は、忘れがちな利害関係者を挙げてくれる。

タロウくん
なるほど。
AI Agent が要求を「決める」わけではないけれど、人間が要求を「掘り起こす」作業を、手伝ってくれるのですね。

専任講師
その理解でほぼ正しい。
この位置付けを、次のように表現できる

専任講師
AI Agent は意図を持たない。しかし、人間が自らの意図を掘り起こすための「対話の鏡(リフレクション)」としては、極めて強力に機能する。

専任講師
ここが、AI Agent 時代の要求工学の面白いところだ。

AI Agent は、単なる「コード生成機」ではない。

要求分析のパートナーでもある。
ただし、パートナーであって、決定者ではない。

意図を決めるのは、依然として人間だ

タロウくん
先生、AI Agent の役割が、今日の対話の最初の頃と比べて、少し豊かに見えてきました。

専任講師
そうだね。AI Agent は、コードを書く能力においても、意図を掘り起こす対話の鏡としての能力においても、極めて強力だ。

しかし、「これがしたい」という主体的な望みそのものは、依然として人間だけが持つ。ここが、AI Agent 時代における人間の役割の核心だ。

まとめ

タロウくん
先生、今日の議論を、私なりにまとめてみます。

専任講師
うん、聞かせてくれ。

タロウくん
まず、AI Agent が生成したコードが、人間の意図通りに動くまでには、4つの段階があります。

① 人間が何をしたいか考える
② 仕様を書く
③ 実装が仕様を満たす
④ コンパイラや証明器が証明を検査する

タロウくん
このうち、形式証明が保証してくれるのは、③と④だけです。①と②は、依然として人間の役割として残ります

タロウくん
形式手法の世界では、これを Correctness ≠ Appropriateness と表現します。
Correctness(仕様通り)と Appropriateness(本当に欲しかったもの)は、別のことなのです

タロウくん
そして、この２つを分ける鍵は「意図」にあります。

AI Agent も、Lean 4 も、Coq も、F* も、意図を持ちません。意図を持つのは、人間だけです。

タロウくん
したがって、仕様と人間の意図のギャップを判定できるのは、意図を持つ人間だけです。

タロウくん
ただし、大きな組織では、意図を持つ人間は一人ではありません。

複数の人間が対話を通じて、少しずつ仕様と意図の一致を確かめていきます。

この対話のプロセスこそが、AI Agent には代替できない、人間の役割の核心です。

タロウくん
そして、この「仕様と人間の意図のギャップを埋める」営みには、要求工学（Requirements Engineering）という学問があることを、今日、初めて知りました。

形式手法と要求工学は、AI Agent 時代における人間の役割を、両側から支える二本の柱 だと、先生からお教えいただきました。

専任講師
うまくまとめたね。今日の議論を、正確に掴んでくれた。

タロウくん
先生、今日は本当にありがとうございました。

形式証明の本当の力と、その限界 が、少し見えてきた気がします。

専任講師
形式手法を学ぶ意味は、まさにこの「どこまで機械が保証できて、どこから人間の責任が残るのか」を、明確に見極めることにある。

この見極めができる人が、AI Agent 時代の実務者として、最も価値のある働きができる人だ。

タロウくん
はい。もっと勉強します

結び

この記事は、次の４つの主張を、対話形式でお届けしました。

形式証明は、実装が書かれた仕様を満たすことは、厳密に保証してくれる
しかし、書かれた仕様が、人間が本当に望んでいたことを正しく表現しているかは、形式証明の視野の外にある
仕様と人間の意図の一致を確かめられるのは、意図を持つ人間だけであり、それは大きな組織では、複数の人間が対話を通じて担う作業である
この「仕様と人間の意図のギャップを埋める」ための体系的な学問として、要求工学（Requirements Engineering）がある

AI Agent が生成したコードを、業務に導入する際、皆様は次の問いを、常に胸に置いてください。

「AI Agent が書いた仕様は、私たちの組織が本当に望んでいたことを、正しく表現しているだろうか」

この問いに答えるのは、AI Agent でも、形式証明言語でもありません。皆様と、皆様の組織の中の、意図を持つ人間たちです。

付録 ── Lean 4 という言語について

対話の本筋からは外れますが、Lean 4 という言語そのものについて、タロウくんが最後に専任講師に質問した対話を、付録として掲載します。Lean 4 の歴史や、汎用プログラミング言語としての側面に興味のある皆様は、こちらもお読みください。

タロウくん
先生、最後に一つだけ。今回の対話の本筋からは外れるのですが、気になっていることを伺ってもよろしいですか

専任講師
もちろん構わないよ。何だい

タロウくん
Lean 4 は、単なる定理証明言語や形式証明言語ではなく、汎用的なプログラミング言語でもある、という解説を目にすることがあります。これは、どういうことですか

タロウくん
定理証明や形式証明を目的としない利用場面でも、プログラミング言語として、何かソフトウェアやスクリプトを実装する際の言語として、Lean 4 が採用されることがある、ということでしょうか

タロウくん
それと、Lean 4 という名前ということは、Lean 3 とか Lean 2 も、過去にはあったのでしょうか

専任講師
いい問いだね。順に答えていこう

専任講師
まず、Lean 4 は、確かに汎用の関数型プログラミング言語でもある。単なる定理証明系ではない

専任講師
Lean 4 は、依存型理論と実用的な関数型プログラミング言語を組み合わせたものとして位置付けられている。

Lean 4 の公式サイトでは、Lean 4 について、"Lean is a functional programming language and theorem prover built for formalizing math and for formal verification, but is flexible enough for general coding." と紹介されている

Lean is a functional programming language and theorem prover built for formalizing math and for formal verification, but is flexible enough for general coding. If you’re a beginner, we recommend the Natural Number Game. If you feel ready to dive deeper, there are great textbooks, tutorials and interactive games to be found on this page.

公式には、Lean 4の用途として、次の３つが並列に挙げられている

汎用の関数型プログラミング ： CLI ツール、ライブラリ、アプリケーションの構築
形式検証 ：ソフトウェアの正しさの証明
数学の定理証明 ─：研究や教育のための形式的な数学の記述

専任講師
Lean 4 のコンパイラは、C コードを出力する。

だから、Lean 4で書かれたプログラムは、Cコンパイラを通じて、効率的な実行可能ファイルにコンパイルできる。本番運用にも耐える性能を持つよ。

専任講師
面白いことにね、Lean 4 のコンパイラや処理系そのものが、Lean 4で書かれているんだ。

セルフホスティング といって、その言語自身でその言語を実装する、という設計だ。
これは、Lean 4 が汎用プログラミング言語として実用的であることの、一つの証拠でもある

タロウくん
そんなに実用的なのですね！

専任講師
そうだ。

ライセンスもApache 2.0で、商用利用にも制限がない。

Python や Rust や Go のような、既に確立された汎用プログラミング言語ほど、Lean 4 でアプリケーション開発が広く行われているわけではない。

しかし、定理証明系のバックエンドとしての内部ツール、証明支援系の周辺ツール、独自ドメイン言語(DSL)の実装基盤、SQL クエリビルダーのようなスタンドアロン・アプリケーションなどの実例が、既に存在している

専任講師
そして、Leanの歴史だね

専任講師
Leanは、Leonardo de Moura（レオナルド・デ・モウラ）が Microsoft Research で開発を始めた定理証明系だ。順に見ていこう

Lean 2
2015年に公式にリリース。依存型理論に基づく対話的な定理証明系（interactive theorem prover）としての基本形が、ここで確立された
Lean 3
2017年にリリース。ユーザー拡張可能な自動化 と、メタプログラミング言語 としての機能を導入。この時期、数学者コミュニティの間で Lean が広く使われるようになり、Mathlib と呼ばれる大規模な数学ライブラリがここで大きく成長した
Lean 4
2018年に開発が始まり、2023年9月8日 に最初の安定版(4.0.0)がリリースされた。Lean 3 の限界を乗り越えるための、大規模な再実装だ

タロウくん
Lean 4 は、Lean 3 の単なるバージョンアップではなく、大きな再実装だったのですね

専任講師
そうだ。Lean 3 と Lean 4 は、実質的に互換性がない。Mathlib の全体を Lean 3 から Lean 4 に移植する、という数年がかりの大規模な移植プロジェクトが、コミュニティによって進められた

専任講師
Lean 4 では、Lean 3 の時代にはなかった、次のような特徴が加わった

汎用プログラミング言語としての完成度 ── C コードへのコンパイル、効率的な実行時性能
セルフホスティング ── Lean 4 の処理系そのものが Lean 4 で書かれている
拡張可能な構文 ── ユーザーが自分で構文を拡張できる
衛生的なマクロシステム(hygienic macro system) ── メタプログラミングがより安全になった
効率的な型クラス解決 ── Lean 3 の時代にあった性能上の問題を解決

専任講師
── なお、Lean 1 も存在した。ただし、Lean 1 は、Leonardo de Moura が Microsoft Research で 2013年頃に開発を始めた、極めて初期の実験的なバージョンだ。公式リリースの主流は Lean 2 以降だから、実用としては Lean 2、3、4 の系譜を掴んでおけば十分だろう

タロウくん
なるほど。Lean 4 は、単なる定理証明系ではなく、汎用の関数型プログラミング言語でもある、というのがよく分かりました

タロウくん
そして、Lean 2、Lean 3、Lean 4 という進化の中で、定理証明系としての機能に、汎用プログラミング言語としての機能が加わっていった、という流れなのですね

専任講師
その理解でほぼ正しい。── そして、この流れは、実は今日の対話の本筋とも、深く繋がっている

専任講師
Lean 4 が汎用プログラミング言語としての性格を強めたことによって、「形式的な仕様を書くための言語」と「実装のための言語」が、同じ言語で書けるようになった。仕様と実装の間のギャップが、言語のレベルで、より近くなったわけだ

専任講師
しかし、「仕様と人間の意図のギャップ」は、Lean 4 が汎用プログラミング言語になっても、依然として残る。この点は、Lean 2、Lean 3、Lean 4 のどのバージョンでも、変わらない真理だ

タロウくん
先生、今日はたくさんのことを教えていただき、本当にありがとうございました

専任講師
うん、また質問があったら、いつでもおいで

Pythonの型ヒントの限界を超える「篩型」入門 ―― "x > 0" を型に書くと何が起きるのか（LiquidHaskell・F*・Typed Racket・Idris 2 への誘い）
AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中する
定理証明・形式検証はいまから学ぶ価値があるか ── なぜ「人が仕様を書く」必要があるのか、Lean 4 から始める学習ロードマップ](https://qiita.com/etale_cohomology/items/de81f8a93f7391681821)

はじめに

対話の始まり

4つの段階の整理

Correctness と Appropriateness

Lean 4 で何が証明できるか

しかし、Lean 4 に分からないこと

３段階の役割分担

タロウくんの新しい問い ── 意図を持つとはどういうことか

補足 ── 「意図を持つ人間」とは誰か

要求工学という学問

まとめ

結び

付録 ── Lean 4 という言語について

関連記事