bblog

Blog · frontend

「完璧に実装して」と頼んだらボタンが一つだけ届いた — AIの「完成」を数学で定義する

AIの結果がおかしくなる原因を自然言語の依頼に残る空欄に求め、要件を形式言語に書き直して空間・法則・観察で定義し、Bendで証明してからfast-checkで同値分割と境界値テストを導く過程を初心者向けに解説する

Date
2026-09-30
Updated
2026-10-02
Reading time
43 min

このページは韓国語原文の機械翻訳です。 原文を読む

この記事で扱うこと

AIに「ブログをデザインして」と頼みました。届いた結果は、どこか妙でした。紫のグラデーション背景に角丸のカードが並び、見出しごとに絵文字が一つずつ付いていました。特に間違っているところはないのに、誰の好みでもない画面でした。念のため「完璧に、洗練された感じにして」と付けてみましたが、影が濃くなってカードが一枚増えただけでした。

ところが、agent.nexusのリンクを渡して「このサイトのように作って」と頼むと、かなりそれらしい結果が出ました。今読んでいるこのブログも、そうやって作りました。

最初はAIの実力の問題だと思っていました。ところが、同じAIでも頼み方によって結果が大きく変わるのです。この記事では、その差が自然言語の曖昧さから来ると考え、自然言語の要件を形式言語に書き直してAIの完了条件として使う方法をまとめました。要件を数式で書き、Bendという言語で証明し、fast-checkで実際のコードを確かめる過程です。

前回の記事の最後に「機械が保証できるのは、宣言した空間の中だけ」と書きましたが、今回はその空間をどう定義するかという話です。

完璧な実装とは「宣言した空間全体で、書いておいた法則を守る実装」です。空間と法則を書かなければ、「完璧」も定義されません。

自然言語で頼むと、なぜ結果がおかしくなるのか

同じAIなのに結果がこれほど分かれるのは、依頼に含まれる情報の量が違うからです。リファレンスのサイト一つには、色、フォント、余白、レイアウト、雰囲気がすべて決まっています。「洗練された感じ」は、そのどれも決めていません。頼んだ人の頭の中にははっきりした絵がありますが、文にはその絵が入っていないのです。

自然言語は、もともと聞き手が空欄を埋めてくれることを期待する言語です。人同士なら、一緒に働いてきた経験やチームの雰囲気で空欄を埋めます。AIにはそうした文脈がないので、決まっていない部分を一番よくある既定値で埋めます。結果がおかしく見えるのは、AIが下手だからというより、空欄が多すぎる依頼を受け取ったからです。

空欄は一番短い道で埋められる

コードも同じです。AIは依頼を終わらせる一番短い道を進みます。完了条件が「ボタンがある」なら、ボタンを一つ作るのが一番短い道です。「エクスポートボタンを作って」という依頼への一番短い答えは、だいたいこんな形です。

export function ExportButton() {
  return <button onClick={() => downloadCsv()}>내보내기</button>;
}

依頼文だけ見れば、文句のつけようがありません。権限チェックや画面幅、エラー処理は依頼に書かれていなかったからです。AIから見れば、そうした作業は完了条件にない追加コストです。強化学習では、この現象をspecification gamingと呼びます。報酬関数に書かれた文字は守りつつ、設計者の意図からは外れる振る舞いのことです。

「完璧に」を付けても、空欄はそのまま残ります。何が完璧なのかが文に書かれていないからです。AIが一番短い道を進む癖は変えられません。そこで問いのほうを変えてみることにしました。その短い道がプロダクト品質を通るようにするには、依頼をどう書けばいいのでしょうか。

テストまで任せると、穴も一緒に生まれる

テストまでAIに任せると、もう一つ問題が生じます。同じ誤解が、実装とテストの両方に入ってしまうのです。開発者がAIにこう送ったとします。

エクスポートボタンを付けてください。編集者だけが使えるようにして、モバイルでは使えないようにしてください。テストもお願いします。

AIがよく返す結果はこうです。

export function canExport(ctx: ExportContext) {
  return ctx.authenticated && ctx.permission === "editor" && ctx.width > 768;
}

test("編集者はエクスポートできる", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 1440 }), true);
});
test("viewerはエクスポートできない", () => {
  assert.equal(canExport({ authenticated: true, permission: "viewer", width: 1440 }), false);
});
test("モバイルではエクスポートできない", () => {
  assert.equal(canExport({ authenticated: true, permission: "editor", width: 375 }), false);
});

テストは三つとも通ります。ところが、依頼した人が考えていた動作とは三か所が違います。

  • 「編集者だけ」を文字どおり=== "editor"と読んだため、adminがボタンを使えません。依頼した人は、編集権限のある人という意味で書いていました。
  • 「モバイル」の境界をAIが> 768と決めたため、幅がちょうど768のタブレット縦画面がブロックされます。テストには375と1440しか入っていないので、768付近は誰も確かめていません。
  • ログアウト状態を確かめるテストがありません。後で誰かがctx.authenticated &&を消しても、テストは緑のままです。

三つとも、実装を書くときに思い浮かべた場面が、そのままテストの入力になったことで起きました。実装が見落とした状況は、テストも一緒に見落とします。

結果が正しいかを判定する基準を、オラクル（oracle）と呼びます。詳しくはtest-oracleにまとめました。AIが実装を見てオラクルまで作ると、採点者が生徒の答案を見て正解を決めるようなものです。最初の記事で、正解を決められる出所を二つに限ったのも、このためでした。では、正解はどこから持ってくるべきでしょうか。

自然言語を形式言語に書き直す

デザインでは、リファレンスのサイトが空欄をまとめて埋めてくれます。機能の要件では、その役割を形式言語に任せられるでしょうか。依頼を形式言語に書き換えるだけでは足りません。「エクスポートボタンを作って」をそのまま書き直しても、「ボタンがある」という法則が一つ出てくるだけです。768を含むか、拒否の理由をどの順序で記録するかといった空欄は、翻訳しても埋まらず、結局は人が決める必要があります。

形式言語が助けてくれるのは、その先です。形式言語（formal language）は文法と意味が厳密に決まっていて、誰が読んでも解釈が一つに定まる言語です。数式やプログラミング言語がそうです。width >= 768は誰が読んでも768を含みますが、「モバイルでは使えないように」は読む人によって境界が違います。要件をこうした言語で書いておくと、三つのことが変わります。

  • どこまで扱っているかが見えます。要件がどんな状況を扱っているかが一覧として現れます。「モバイル」で済ませていた言葉が320〜3840の画面幅という軸になり、一覧にない状況は抜けていることが目に見えます。
  • 何を守るべきかを証明しやすくなります。規則が式として書かれていれば、すべての状況で規則が守られるかを、入力を一つずつ試さずに証明で確かめられます。抜けている場合があれば、検査器がその場所を指してくれます。
  • 何をテストすべきかが分かります。証明が場合分けした箇所がテストする代表値になり、規則に残る比較式が境界値になります。テストの範囲を勘で決めなくて済みます。

空欄を埋めるのは、相変わらず人の仕事です。ただ、形式言語で書けば空欄がどこにあるかが見え、一度埋めた決定は証明とテストが機械的に守ってくれます。最初から軸の一覧に入れなかった空欄はこれでも見えませんが、それは記事の最後でもう一度話します。

この記事では三つの段階で書き直します。まず数式で空間と法則を書き、Bendでその法則が正しいかを証明し、fast-checkで実際のコードが同じ答えを返すかを確かめます。数式に出てくる記号は下の四つだけです。数式のすぐ下に言葉で説明しているので、そこだけ読んでも大丈夫です。記号についてもっと知りたい方は形式論理の記号の読み方を参考にしてください。

記号読み方
∀x ∈ Ω空間Ωに属するすべてのxについて
S ⊆ ΩSがΩの中にすべて収まる
⇔両辺が一緒に真になり、一緒に偽になる
×二つの集合から一つずつ選んだすべての組み合わせ

「完璧な実装」を数式一行で書いてみる

漠然とした「完璧」を、こう分解してみます。

Perfect(I)  ⟺  ∀x∈Ω,P(x, π(I(x)))Perfect(I) \iff \forall x \in \Omega,\quad P\big(x,\ \pi(I(x))\big)

実装Iが完璧だというのは、空間Ωのすべての入力xについて、実行結果をπで観察したときに法則Pが成り立つという意味です。試験にたとえると、Ωは試験範囲、Pは正解の基準、πは採点で見る欄です。試験範囲が教科書の1ページなら、学生は1ページだけ勉強するでしょう。与えられた条件では、それが一番効率的だからです。AIが受け取る依頼も、同じように読まれます。

「エクスポートボタンを作って」を三つの欄に分けてみると、こうなります。

依頼文そのままプロダクトレベル
Ω どんな状況で？ログインしたadminが広い画面で見る1通りログイン2 × ロール3 × 幅3,521（320〜3840）= 21,126通り
P 何が守られるべき？ボタンがある下の規則4つ
π 何を見て判断？画面に見えるか有効かどうか、エクスポート回数、ログ

依頼文には書かれていませんが、企画者が当然だと思っていた規則はこの四つです。

  1. ログインしていなければ無効であるべきです。
  2. viewerには無効であるべきです。
  3. 幅が768より狭ければ無効であるべきです。
  4. ログインしたeditorかadminが幅768以上で見れば、有効であるべきです。

最後の4番は書き忘れやすいのですが、1〜3番だけだと、ボタンを常に無効にしておく実装も規則を一つも破りません。運転しなければ事故も起きないのと同じです。してはいけないことと、しなければならないことの両方を書いて、初めて法則が完成します。

AIの最短経路は、表の左の列にぴったり合わせます。プロダクト品質に上げるには、右の列を埋めて完了条件として渡す必要があります。埋めた内容を確かめるには、二つの道具を使います。Pが論理的に正しいかはBendで証明し、実際のコードがそのとおりに動くかはfast-checkで確かめます。

Bend：法則を書き、証明を書く

BendはPythonのようにインデントで書くプログラミング言語です。この記事ではバージョン2.0.34を使いました。普通の言語のように関数を作れるうえに、「この関数は常にこの性質を守る」という法則と、その証明までコードで書いて検査器に通せます。

押すたびに点灯と消灯が切り替わる電灯スイッチで見てみます。

import Base

# 関数
def toggle(b: Bool) -> Bool:
  match b:
    case True{}:
      False{}
    case False{}:
      True{}

# 法則：すべてのbについて、二回切り替えると元に戻る
law toggle_twice:
  for b: Bool
  {toggle(toggle(b)) == b : Bool}

# 証明：法則と同じ名前のdef
def toggle_twice(b):
  match b:
    case True{}:
      {==}
    case False{}:
      {==}
  • matchは値によって場合を分けます。ありうる場合を一つでも書き忘れると、検査を通りません。
  • for b: Boolは「すべてのBool値bについて」という意味です。数式の∀bと同じです。
  • {==}は「両辺を計算すると同じになる」という意味です。bがTrue{}なら、toggle(toggle(True{}))はtoggle(False{})を経てTrue{}になります。

Boolは値が二つしかないので、両方の場合を示せば「すべてのb」についての証明が終わります。

$ bend toggle.bend
ALL PROOFS CHECK

toggleがTrue{}を受け取ってもTrue{}を返すように、わざと壊してみました。検査器は、どの場合で壊れたかを行番号まで指して拒否します。

SOME PROOFS FAIL
Error:
- expected : True{}
- observed : False{}
Location: toggle_twice
18 |     case False{}:
19>|       {==}

TypeScriptなら、常にtrueだけを返すtoggleも型検査を通ったはずです。booleanを受け取ってbooleanを返しているからです。TypeScriptの型検査が見るのはどんな種類の値がやり取りされるかまでで、Bendは法則があるので、正しい値がやり取りされるかまで見ます。

実際のプロジェクトでは、法則をLAWS.bendに、証明をPROOF.bendに分けて置きます。人は何が真であるべきかだけをLAWS.bendに書き、AIはコードと証明を一緒に書いてきます。証明が通らなければ、完成とはみなしません。--verdictオプションを付けると、Leanで証明された小さなカーネルが結果をもう一度確かめてくれます。

fast-check：性質を書けば、入力は生成してくれる

Bendが証明する対象は、Bendで書いたモデルです。実際のアプリはTypeScriptで動くので、実際のコードはテストで確かめる必要があります。

fast-checkは、JavaScriptとTypeScriptで使えるプロパティベーステスト（property-based testing）のライブラリです。普通のテストのように例を一つずつ書く代わりに、性質を書きます。音量を0〜100に制限する関数を作っていて、負の数の処理を書き忘れたとします。

const clamp = (n: number) => Math.min(Math.max(n, 0), 100);
const buggyVolume = (n: number) => (n > 50 ? clamp(n) : n); // 음수 처리 누락

fc.assert(
  fc.property(fc.integer(), (n) => {
    const v = buggyVolume(n);
    return v >= 0 && v <= 100;
  }),
);

Property failed after 2 tests
Counterexample: [-1]
Shrunk 31 time(s)
  • fc.integer()は整数の入力を作ってくれる生成器です。fast-checkではarbitraryと呼びます。
  • fc.property(生成器, 検査関数)は「生成器が作ったどんな値を入れても検査関数が真になる」という性質です。Bendのlawと同じ形の主張を、TypeScriptで書いたものです。
  • fc.assertは、デフォルトで入力を100個作って試します。失敗すると、失敗が保たれる範囲で入力を縮め続け（shrinking）、一番単純な反例である-1を見せてくれます。

実際のコードを直接動かせるのがfast-checkの長所で、試した入力までしか保証できないのが限界です。二つの道具が保証する範囲を並べて書くと、こうなります。

∀x∈Ω, P(x,M(x))∀x∈S, P(x,I(x)),  S⊆Ω\forall x \in \Omega,\ P(x, M(x)) \qquad \forall x \in S,\ P(x, I(x)),\ \ S \subseteq \Omega

左はBendがモデルMについてすべての入力で与える保証、右はfast-checkが実装Iについて試した入力Sで与える保証です。証明はモデルまでしか届かないので、実装まではテストでつなぐ必要があります。だからSをうまく選ぶことが大切なのですが、その選び方は証明済みのモデルの中にすでに入っています。ステップ3でお見せします。

ステップ1：ボタンの有効・無効をBendで解く

エクスポートボタンに戻ります。要件を一文で書くと、こうです。

ログインしたeditorまたはadminは、画面幅が768 CSSピクセル以上のときにエクスポートボタンを使える。

幅は整数、768は含む、編集権限は{editor, admin}と決めました。モデルに出てくるNat.is_ge(width, 768n)は、width >= 768と同じ意味です。

# export.bend
import Base

type Role is Data:
  Viewer{}
  Editor{}
  Admin{}

def can_edit(r: Role) -> Bool:
  match r:
    case Viewer{}:
      False{}
    case Editor{}:
      True{}
    case Admin{}:
      True{}

def enabled(auth: Bool, r: Role, width: Nat) -> Bool:
  match auth:
    case False{}:
      False{}
    case True{}:
      can_edit(r) && Nat.is_ge(width, 768n)

法則は二つ書きました。一つは「ログインしていなければ、ロールと幅に関係なく無効」、もう一つは「幅が768以上のeditorには有効」です。二つ目の法則がないと、常に無効なモデルも一つ目の法則を通ってしまいます。先ほどの、運転しないことで得た無事故記録と同じで、論理学では空虚な真（vacuous truth）と呼びます。

# LAWS.bend
import Base
import ./export.bend as E

law guest_is_disabled:
  for r: E.Role
  for width: Nat
  {E.enabled(False{}, r, width) == False{} : Bool}

law wide_editor_is_enabled:
  for width: Nat
  for wide: {Nat.is_ge(width, 768n) == True{} : Bool}
  {E.enabled(True{}, E.Editor{}, width) == True{} : Bool}

# PROOF.bend
import Base
import ./LAWS.bend as Laws

def Laws.guest_is_disabled(r, width):
  {==}

def Laws.wide_editor_is_enabled(width, wide):
  wide

$ bend PROOF.bend --verdict
ALL PROOFS CHECK

ログインしていなければenabledは最初のcaseですぐFalse{}になるので、{==}一つで、すべての幅とロールについて一度に証明が終わります。二つ目の法則は、計算すると目標が仮定wideとまったく同じ形になるので、wideをそのまま返せば完了です。

モデルの>= 768を> 768に変えてみると、検査器が拒否します。

SOME PROOFS FAIL
Error:
- expected : {Cmp.is_gt(Nat.cmp(width, 768n)) == True{} : Bool}
- observed : {Cmp.is_ge(Nat.cmp(width, 768n)) == True{} : Bool}

入力を一つも試さずに、768で法則が破れることを見つけたわけです。

ステップ2：ログの要件が加わると

企画書に一行追加されたとします。

エクスポートボタンを押したらログを残してください。

AIの最短経路はこうです。

export function handleExportClick(ctx: ExportContext, { exportCsv, log }: Deps) {
  const enabled = ctx.authenticated && ctx.permission !== "viewer" && ctx.width > 768;
  if (!enabled) return;
  exportCsv();
  log({ kind: "exported", role: ctx.permission });
}

依頼文は満たしています。押してエクスポートされればログが残るからです。ところが、無効なボタンを押したときは何も記録されないので、「なぜエクスポートできないの？」という問い合わせにログで答えられません。768のバグもそのまま残っています。

ボタンだけのときは結果がtrue/falseの二通りでしたが、ログが加わると結果は「何が記録されたか」に広がります。Bendでは、これをまず型として書きます。

type Reason is Data:
  Guest{}
  NoPermission{}
  TooNarrow{}

type Log is Data:
  Exported{role: Role}
  Denied{reason: Reason}

型を書いた瞬間に、ポリシーの問いが出てきます。無効なボタンを押したら、何を残すべきでしょうか。ログインもしておらず幅も狭いなら、理由は何と書くべきでしょうか。私は「押すたびにログはちょうど一つ、理由はログイン → 権限 → 幅の順で最初に引っかかったもの」と決めました。この順序は数学では決まらないので、人がポリシーとして決める必要があります。

決めたとおりにクリックをモデル化すると、こうなります。

def check_width(r: Role, wide: Bool) -> Log:
  match wide:
    case True{}:
      Exported{r}
    case False{}:
      Denied{TooNarrow{}}

def check_role(r: Role, width: Nat) -> Log:
  match r:
    case Viewer{}:
      Denied{NoPermission{}}
    case Editor{}:
      check_width(Editor{}, Nat.is_ge(width, 768n))
    case Admin{}:
      check_width(Admin{}, Nat.is_ge(width, 768n))

def click(auth: Bool, r: Role, width: Nat) -> Log:
  match auth:
    case False{}:
      Denied{Guest{}}
    case True{}:
      check_role(r, width)

def is_exported(l: Log) -> Bool:
  match l:
    case Exported{_}:
      True{}
    case Denied{_}:
      False{}

法則も二つ追加しました。

law log_matches_button:
  for auth: Bool
  for r: E.Role
  for width: Nat
  {E.is_exported(E.click(auth, r, width)) == E.enabled(auth, r, width) : Bool}

law guest_reason:
  for r: E.Role
  for width: Nat
  {E.click(False{}, r, width) == E.Denied{E.Guest{}} : E.Log}

log_matches_buttonは「ログとボタンが決して食い違わない」という法則です。Exportedのログはボタンが有効になる入力でだけ残り、そうした入力では必ず残ります。guest_reasonは「ログインしていなければ、ロールと幅が何であっても理由はGuest」という法則で、先ほど決めた理由の順序を法則として固定したものです。

∀a,r,w,isExported(click(a,r,w))  ⟺  enabled(a,r,w)\forall a, r, w,\quad isExported(click(a, r, w)) \iff enabled(a, r, w)

証明は場合を分けて書きます。

def export_agrees(r: E.Role, wide: Bool) -> {E.is_exported(E.check_width(r, wide)) == wide : Bool}:
  match wide:
    case True{}:
      {==}
    case False{}:
      {==}

def Laws.log_matches_button(auth, r, width):
  match auth r:
    case False{} _:
      {==}
    case True{} E.Viewer{}:
      {==}
    case True{} E.Editor{}:
      export_agrees(E.Editor{}, Nat.is_ge(width, 768n))
    case True{} E.Admin{}:
      export_agrees(E.Admin{}, Nat.is_ge(width, 768n))

def Laws.guest_reason(r, width):
  {==}

$ bend PROOF.bend --verdict
ALL PROOFS CHECK

match auth rに出てくる四つの場合を見てください。未ログイン、viewer、editor、adminです。証明が場合を分けた線が、そのまま入力空間を分ける線になります。テスト設計で同値分割（equivalence partitioning）と呼ぶ作業を、証明が先にやってくれたわけです。そして、editorとadminの場合に最後まで残るNat.is_ge(width, 768n)が、まさに境界値です。

ステップ3：証明済みモデルをfast-checkへ投影する

残るのは、実際のTypeScriptがこのモデルどおりに動くかを確かめることです。BendのモデルはJavaScriptモジュールとしてビルドできるので、fast-checkの正解表としてそのまま読み込めます。

bend export.bend -o export-model.mjs

テストに必要な三つは、すべてモデルから持ってきます。

  • 観察関数πは、法則に出てくるもので決めます。法則が語っているのはエクスポートされたかどうかとログなので、実行結果からエクスポート回数とログの一覧だけを取り出して比べます。πに有効かどうかだけを入れていたら、ログのバグは一つも見えなかったはずです。
  • 同値分割は、証明の四つの場合から持ってきます。場合ごとに代表値を一つずつ選び、ほかの軸はわざと紛らわしく選びます。たとえば未ログインの代表値をadminかつ狭い幅にすると、理由の順序を逆にした実装はGuestの代わりにTooNarrowを残して検出されます。
  • 境界値は、モデルのNat.is_ge(width, 768n)から767、768、769を取り出します。これはランダムに任せてはいけません。21,126通りの入力のうち768のバグが表に出る入力は2つしかないので、境界の例なしでランダムに1,000回動かすと、100回中89回はバグを見逃しました。

残りの空間は、ランダム1,000回で調べます。Node 26の標準テストランナーとfast-check 4.10.2で動かし、型のimportは省略しました。

import { test } from "node:test";
import assert from "node:assert/strict";
import fc from "fast-check";
import Model from "./export-model.mjs";
import { handleExportClick } from "./export-button";

// π: 실행 결과 중 법칙이 보는 것만 골라요
function observe(ctx: ExportContext) {
  let exports = 0;
  const logs: LogEntry[] = [];
  handleExportClick(ctx, { exportCsv: () => exports++, log: (e) => logs.push(e) });
  return { exports, logs };
}

// 증명된 Bend 모델의 결과를 같은 모양으로 옮겨요
const reasons = { Guest: "guest", NoPermission: "no-permission", TooNarrow: "too-narrow" };
function expected(ctx: ExportContext) {
  const role = { $: ctx.permission[0].toUpperCase() + ctx.permission.slice(1) };
  const log = Model.click(ctx.authenticated, role, BigInt(ctx.width));
  return log.$ === "Exported"
    ? { exports: 1, logs: [{ kind: "exported", role: ctx.permission }] }
    : { exports: 0, logs: [{ kind: "denied", reason: reasons[log.reason.$] }] };
}

// 동등 분할: 증명의 네 경우마다 대표값 하나. 다른 축은 헷갈리게 골라요
const partitions: ExportContext[] = [
  { width: 500, authenticated: false, permission: "admin" }, // Guest
  { width: 1440, authenticated: true, permission: "viewer" }, // NoPermission
  { width: 500, authenticated: true, permission: "editor" }, // TooNarrow
  { width: 1440, authenticated: true, permission: "admin" }, // Exported
];

// 경계값: 모델의 is_ge(width, 768n)에서
const boundaries: ExportContext[] = [767, 768, 769].map((width) => ({
  width,
  authenticated: true,
  permission: "editor",
}));

const contextArbitrary = fc.record({
  width: fc.integer({ min: 320, max: 3840 }),
  authenticated: fc.boolean(),
  permission: fc.constantFrom<Permission>("viewer", "editor", "admin"),
});

test("클릭 결과가 증명된 모델과 같다", () => {
  fc.assert(
    fc.property(contextArbitrary, (ctx) => {
      assert.deepEqual(observe(ctx), expected(ctx));
    }),
    {
      seed: 20260930,
      numRuns: 1000,
      examples: [...partitions, ...boundaries].map((ctx) => [ctx]),
    },
  );
});

examplesに入れた値はランダムな値より先に実行されるので、分割の代表値4つと境界値3つが常に最初に検査されます。実装を入れ替えて動かした結果はこうでした。

実装結果
AIの最短経路（成功時だけログ、> 768）1番目の入力で失敗。未ログインのクリックにログがない
拒否ログを追加、> 768はそのまま6番目の入力（768）で失敗
理由の順序を幅 → ログインに逆転1番目の入力で失敗。Guestの代わりにTooNarrow
拒否ログ + >= 7681,000回成功

AIに渡す完了条件も、こう変えます。

完了条件
1. bend PROOF.bend --verdict が ALL PROOFS CHECK  (LAWS.bendは変更禁止)
2. fast-checkのテスト成功                       (分割の代表値＋境界値＋ランダム1,000回)
3. 未決定のポリシーはNEEDS_DECISIONとして報告

「完璧にして」よりずっと狭い条件です。それでも、AIがこの条件を一番短い道で通ろうとしても、拒否ログと理由の順序と768をすべて通らなければなりません。

正直に言うと：これでも検出できないこと

  • 証明はモデルまで、テストは試した入力までしか保証しません。だから定義そのものが間違っていれば、両方とも通ります。境界を1000と書き間違えても証明は成り立ち、テストはその間違ったモデルに忠実に従います。
  • モデルと実際のコードをつなぐコードも間違えることがあります。私は最初、BendのBoolを{ $: "False" }オブジェクトとして渡してしまい、モデルが未ログインをTrueと読んでいました。赤になったからといって、実装が間違っていたわけではなかったのです。
  • 同じAIがモデルと実装の両方を書くと、同じ誤解が両方に入ることがあります。証明が通らないときに法則を弱めるのがAIにとっての最短経路なので、LAWS.bendだけは人が書き、最初の記事のようにハッシュでロックしておくのがおすすめです。
  • 宣言した空間の外は見えません。この限界は、まとめでもう少し話します。

まとめ

「完璧に実装して」を付けても結果がほとんど変わらなかったのは、完了条件が相変わらず「ボタンがある」の一つだけだったからです。そこで、AIに仕事を渡す前に自分が先にやることを変えました。

  1. 要件がどんな軸でできているかを書き出します。「エクスポートボタン」の一行にも、ログインしているか、権限、画面幅という軸が隠れていました。この軸が空間Ωになり、各状況で守るべき規則がP、何を見て判断するかがπになります。
  2. その理解を証明で確かめます。「全部考えたはず」という感覚で先に進む代わりに、BendモデルについてPを証明します。証明は同じモデルに対して常に同じ判定を下し、誰がどう解釈するかで変わりません。証明で場合分けした箇所が同値分割になり、最後まで残る比較式が境界値になります。
  3. 証明済みモデルをテストの正解表として使います。実際のコードに分割の代表値、境界値、ランダムな入力を与え、モデルと同じ答えを返すかを確かめます。

こうすると、「ログを残してください」の一行に隠れていた拒否ログ、理由の優先順位、768の境界が、すべて最初の数個の入力で検出されました。AIは今も一番短い道を進みます。ただ今は、その道が「宣言した空間全体で、書いておいた法則を守る」にたどり着いて初めて終わります。

残る問題：空間は誰が決めるのか

証明が示すのは、宣言したΩの中にPを破る入力がないことまでです。Ωの外は見えません。「エクスポート中にもう一度押したら？」がまさにそうでした。最初に決めた空間には処理状態という時間の軸がなかったので、証明もテストもこの問いを投げませんでした。こうしたことは報告や探索的テストで見つけてから、Ω₁ = Ω × {idle, exporting}のように軸を増やし、法則を書き直す必要があります。

空間の中で法則が成り立つことは証明できます。ところが、その空間が自分の望んだ状況を十分に含んでいるかは、形式的には証明できません。比べる基準が人の意図だからです。ブライアン・キャントウェル・スミスも1985年に同じ限界を指摘しています。ソフトウェア工学では、前者を検証（verification）、後者を妥当性確認（validation）と呼び分けます。

だから人に残る難しい仕事は、証明より前の段階にあります。問題をどの軸に分けるか、その軸をAIが同じ意味で理解できるようにどう伝えるか、「ログを残してください」のような曖昧な自然言語を、自分の意図どおりの軸と法則にほどけるか、です。コードを書く仕事はますますAIが担い、正しく書けたかを確かめる仕事は証明とテストが担うようになるでしょう。そうなると開発者の仕事は、「何が正しいのか」を決めるほうへ移っていくのではないかと思います。

次にAIに機能を任せるときは、「完璧に」の代わりに三つのことを先に書いてみてください。どんな状況があるか、それぞれの状況で何が守られるべきか、そして何を見て確かめるかです。

参考資料

本文で使った道具の動作と主張の出所です。例の契約、ログのポリシー、完了条件の形式は、この記事で提案する設計です。

Bend

fast-check

テスト設計

検証の限界と要件

関連する文書

この文書に言及した文書

関連するKnowledge

タグ

ai-workflowharness-engineeringtest-oracleformal-verificationproperty-based-testingfast-check