これは何か
問題定義から始める検討 Issue(研究余地の記録)。 #88(IA 退行)は実務的に「MODIFY は決定論ルールのみ/LLM は変換を生成しない/隙間は DENY か素の a への STEP_UP」と DENY 側に倒した。本 Issue は、その判断の背後にある理論的構造(なぜ倒したか、倒した先に何があったか)を前向きに記録する。個人活動・学習目的での研究余地であり、即時の実装方針ではない。#27(SIEM 連携)と同型の「いつか取り組む可能性を開けておく」Issue。
出発点
#88 で確定した着地「LLM 由来の変換提案はランタイムで採用しない」。一見「LLM 由来=即 DENY」は短絡に見えるが、短絡ではない理由(match(a,C) と正統性)を掘ると、逆に「LLM の正当な持ち場はどこか」という研究余地が見える。
二層のパラドックス
着地案「LLM が a' を提案 → 決定的述語で検証 → auto-apply」には二層のパラドックスが埋まっている。
浅い層(解ける): 「決定的述語で a' の安全性を検証できるなら LLM はいらない(決定的システムが自分で a' を作ればよい=modify_transform)。LLM が要る場面ではその安全性は決定的に検証できない」。一見、中間地帯は空に見える。
→ 生成と検証の非対称性で解ける。検証が生成より安いケースは現に存在する(P/NP 的直観)。「曖昧な意図に合うファイル名を作る」は生成に意図理解が要るが、検証(root 内か・衝突しないか)は自明な決定的述語。LLM の正当な持ち場は「生成が難しく、かつ検証が形式化できる」交差点。
深い層(解けない・移るだけ): 決定的述語は「我々が形式化できた不変条件」しか検証できない。だが LLM に手を伸ばす理由(自由文 PII 墨消し等)は、まさに安全性が形式化しきれないから。
- 述語で書ける安全性 = すでに符号化できたもの = そもそも modify_transform で機械が持てたもの。
- 述語で書けない安全性 = LLM が要るもの = 構造上、決定的検証が不可能なもの。
→ 検証器の有能さと LLM の必要性は反比例する。 検証器が強いところでは LLM は不要、LLM が必要なところでは検証器が弱い。これがパラドックスの芯で、消えない。
検証は安全性証明ではなく封じ込め境界
述語が certify するのは「a' はこの不変条件を満たす」であって「a' は安全」ではない。a' は境界内で間違えうる(root 内に留まったまま墨消し対象を取り違える)。本当の判断軸は「検証可能か」ではなく 述語が検証する範囲と要求される安全性の差(残差リスク)を auto-apply してよいか。これは検証の事実ではなくリスク判断で、「残差を評価できるか」は #82 の confidence(= evaluability)そのもの。パラドックスは消えずに confidence 軸へ移る。
検証者能力の昇順の梯子
残差を誰が評価できるかで経路が決まる:
- 決定的述語(形式化できる不変条件を検証)→ 残差≈0 なら auto-apply MODIFY。
- 人間 STEP_UP(形式化できないが、提示から判断できる残差を検証)→ modified_params 付き STEP_UP 拡張の正当化はここ。ただしゴム印リスクは「LLM 由来だから」でなく「残差が人間の検証能力を超えるとき」に発生(50ページ文書の PII 漏れを人間が y/n で検証しきれない)。
- DENY(述語でも人間でも評価できない/残差が大きすぎる)=梯子の床。
→ DENY は「LLM 由来=即」ではなく床。禁じるべきは一点「LLM の a' が、検証も人間承認も経ずに auto-apply される」。
さらに深い層: 正統性は計算の外部から調達される
ここまでは「a' の安全性検証」の話だが、本丸はさらに降りる。match(a,C) の C は組織的合意文脈。「この変換を今この C で適用してよいか」は a' の安全性ではなく正統性の問題。
- AARM の match(a,C) は純粋関数(照合)。だが実務では Π の各ルールが「組織の合意形成(委任・黙認込み)の符号化」。
- ランタイムの計算は正統性を生成できない。 正統性は組織の合意形成からしか来ず、計算の外部にある。LLM をどれだけ強くしても合意形成の代理はできない(黙認を「学習した一般通念」で代替しようとすると、それは組織の黙認ではなく一般通念の密輸)。
- enforcement の時間軸(ランタイム)と、ルール正統性の時間軸(組織合意)は別。LLM をランタイムに置く限り、合意形成の時間軸に追いつけない。LLM 提案の正しい行き先は ログ→分析→組織の合意形成→Π/実装更新 という正統性を調達する回路。
→ これが「ランタイムで LLM 提案を採用できる余地はゼロに近い」の深い理由。「LLM が劣るから」でも「検証できないから」でもなく、正統性の出所(組織合意)を欠くから。
詰めるべき最後の一点(未決)
「ゼロに近い」を「構造的にゼロ」まで強められるか。match(a,C) を要しない変換が本当に皆無か:
- 反例候補: 組織非依存・純機械的で、かつ生成に意図理解が要る変換があれば非ゼロ。
- 潰し方: 組織非依存なら C に依存しない=決定的に書ける=modify_transform 領域に落ちる。生成に意図理解が要るならその意図は文脈 C の一部で組織依存に戻る。二つは両立しないように見える。
- ただしこれを「構造的ゼロ」と断定するのは行き過ぎの懸念がある(一例: 組織が事前に「この変換クラスは自動でよい」と合意し、LLM は適用対象の同定=分類だけする経路。正統性はクラス定義時に組織が持ち、LLM は分類器。完全なゼロの反例になりうるが、分類を LLM に委ねた時点で injection 面が開くため実務で潰される公算が高い)。
→ 「実務的にはゼロに倒す」が公平な着地。「構造的にゼロ」を主張できるかは本 Issue で詰める価値のある最後の一点。
scalable oversight の縮図
これは AARM が内側に抱える scalable oversight(弱く信頼できる検証者が、強く信頼できない生成者の出力をどこまで検証できるか)の縮図。研究としてはこの中間地帯を攻めるが、実用システム(laarma の実装)はそこに踏み込まず DENY 側に倒す——実装の単純さと理論の射程を両方記録するのが本 Issue の価値。
実務(SIer 観点)との対比
仮に SIer が実用化するなら、保証可能性(保証をコードに閉じる)・テスト可能性(決定論変換は回帰テストが書ける)・監査可能性(規則で説明できる)・攻撃面(LLM 提案経路は injection 面を増やす)の四点で「DENY・MODIFY は決定論のみ」に倒すのが合理。laarma は実装ではそれに倣いつつ、なぜそこに倒したか=中間地帯に何があったかを記録に残す。
留保: 「黙認」を正統性に含めることの危うさ
match(a,C) ⇔ 組織合意形成の対応で「黙認」を正統性に含めるのは、実務記述としては妥当だが規範的には危うい縁がある。黙認=「誰も止めなかった」は合意の不在を正統性に読み替える操作でもあり、「誰がいつ承認したか」の証跡を欠く= TCB の中に正統性の出所が追跡できない領域を作る。laarma が監査可能性(#81)を重視するなら、明示的合意/委任/黙認の濃淡を Π のメタdata として区別できた方が誠実。これは本 Issue の派生論点。
関連
これは何か
問題定義から始める検討 Issue(研究余地の記録)。 #88(IA 退行)は実務的に「MODIFY は決定論ルールのみ/LLM は変換を生成しない/隙間は DENY か素の a への STEP_UP」と DENY 側に倒した。本 Issue は、その判断の背後にある理論的構造(なぜ倒したか、倒した先に何があったか)を前向きに記録する。個人活動・学習目的での研究余地であり、即時の実装方針ではない。#27(SIEM 連携)と同型の「いつか取り組む可能性を開けておく」Issue。
出発点
#88 で確定した着地「LLM 由来の変換提案はランタイムで採用しない」。一見「LLM 由来=即 DENY」は短絡に見えるが、短絡ではない理由(match(a,C) と正統性)を掘ると、逆に「LLM の正当な持ち場はどこか」という研究余地が見える。
二層のパラドックス
着地案「LLM が a' を提案 → 決定的述語で検証 → auto-apply」には二層のパラドックスが埋まっている。
浅い層(解ける): 「決定的述語で a' の安全性を検証できるなら LLM はいらない(決定的システムが自分で a' を作ればよい=modify_transform)。LLM が要る場面ではその安全性は決定的に検証できない」。一見、中間地帯は空に見える。
→ 生成と検証の非対称性で解ける。検証が生成より安いケースは現に存在する(P/NP 的直観)。「曖昧な意図に合うファイル名を作る」は生成に意図理解が要るが、検証(root 内か・衝突しないか)は自明な決定的述語。LLM の正当な持ち場は「生成が難しく、かつ検証が形式化できる」交差点。
深い層(解けない・移るだけ): 決定的述語は「我々が形式化できた不変条件」しか検証できない。だが LLM に手を伸ばす理由(自由文 PII 墨消し等)は、まさに安全性が形式化しきれないから。
→ 検証器の有能さと LLM の必要性は反比例する。 検証器が強いところでは LLM は不要、LLM が必要なところでは検証器が弱い。これがパラドックスの芯で、消えない。
検証は安全性証明ではなく封じ込め境界
述語が certify するのは「a' はこの不変条件を満たす」であって「a' は安全」ではない。a' は境界内で間違えうる(root 内に留まったまま墨消し対象を取り違える)。本当の判断軸は「検証可能か」ではなく 述語が検証する範囲と要求される安全性の差(残差リスク)を auto-apply してよいか。これは検証の事実ではなくリスク判断で、「残差を評価できるか」は #82 の confidence(= evaluability)そのもの。パラドックスは消えずに confidence 軸へ移る。
検証者能力の昇順の梯子
残差を誰が評価できるかで経路が決まる:
→ DENY は「LLM 由来=即」ではなく床。禁じるべきは一点「LLM の a' が、検証も人間承認も経ずに auto-apply される」。
さらに深い層: 正統性は計算の外部から調達される
ここまでは「a' の安全性検証」の話だが、本丸はさらに降りる。match(a,C) の C は組織的合意文脈。「この変換を今この C で適用してよいか」は a' の安全性ではなく正統性の問題。
→ これが「ランタイムで LLM 提案を採用できる余地はゼロに近い」の深い理由。「LLM が劣るから」でも「検証できないから」でもなく、正統性の出所(組織合意)を欠くから。
詰めるべき最後の一点(未決)
「ゼロに近い」を「構造的にゼロ」まで強められるか。match(a,C) を要しない変換が本当に皆無か:
→ 「実務的にはゼロに倒す」が公平な着地。「構造的にゼロ」を主張できるかは本 Issue で詰める価値のある最後の一点。
scalable oversight の縮図
これは AARM が内側に抱える scalable oversight(弱く信頼できる検証者が、強く信頼できない生成者の出力をどこまで検証できるか)の縮図。研究としてはこの中間地帯を攻めるが、実用システム(laarma の実装)はそこに踏み込まず DENY 側に倒す——実装の単純さと理論の射程を両方記録するのが本 Issue の価値。
実務(SIer 観点)との対比
仮に SIer が実用化するなら、保証可能性(保証をコードに閉じる)・テスト可能性(決定論変換は回帰テストが書ける)・監査可能性(規則で説明できる)・攻撃面(LLM 提案経路は injection 面を増やす)の四点で「DENY・MODIFY は決定論のみ」に倒すのが合理。laarma は実装ではそれに倣いつつ、なぜそこに倒したか=中間地帯に何があったかを記録に残す。
留保: 「黙認」を正統性に含めることの危うさ
match(a,C) ⇔ 組織合意形成の対応で「黙認」を正統性に含めるのは、実務記述としては妥当だが規範的には危うい縁がある。黙認=「誰も止めなかった」は合意の不在を正統性に読み替える操作でもあり、「誰がいつ承認したか」の証跡を欠く= TCB の中に正統性の出所が追跡できない領域を作る。laarma が監査可能性(#81)を重視するなら、明示的合意/委任/黙認の濃淡を Π のメタdata として区別できた方が誠実。これは本 Issue の派生論点。
関連