top of page
検索

責任OS × EU AI Act——Lean 4で責任証拠を保つ参照モデルを形式化する

執筆者の写真: kanna qed
kanna qed
5 日前
読了時間: 6分

EU AI Act（欧州AI法、Regulation (EU) 2024/1689）は段階的に適用が進んでおり、高リスクAIシステムについては、技術文書、自動ログ、人間による監督、ログ保存、適合性評価、市場投入後モニタリングなどの要件が定められています。2026年のDigital Omnibusによる改正後、高リスクAI規則の適用時期も段階化されています。条文はこれらの要求を定めていますが、それを実装上どのような条件や不変条件として表現し、機械的に検証するかは別の設計問題です。この間を仕様の形で接続する一つの試みを公開しました。

なお、本実装は Regulation (EU) 2024/1689 の原始テキストにおける上記6条項の選択的な技術要件を基準にした参照プロファイルです。2026年のDigital Omnibusによる改正後の統合テキスト全体を形式化したものではありません。


責任OSをLeanでEU AI Actマッピング
責任OSをLeanでEU AI Actマッピング

何を作ったか

AI 法の Art. 11(技術文書)、12(自動ログ)、14(人間による監督)、19(ログ保存)、43(適合性評価の支援)、72(市販後モニタリング) の6条項を対象に、小さな参照状態機械と、その上の不変条件を Lean 4 で記述し、機械的に証明可能な形にしました。本体は1ファイル・約 700 行。外部に自作カーネル(ResponsibilityOS)を1つ依存として持ち、mathlib4 と合わせてリビジョンを固定しています。

中核となる型は次のようなものです(抜粋・簡略化):

lean

structure Context where
  system, release, specification, boundary, documentation : Nat

inductive Request where | allow | withhold | stop
inductive Decision where | executed | held | stopped

def gate (halted ready : Bool) (request : Request) : Decision := ...

structure Event (E) where
  context : Context
  trace   : source ⟶ target     -- 圏の射として表現された操作
  createdAt retainUntil : Nat
  validWindow : createdAt ≤ retainUntil

structure Record (E) where
  event, profileContext, request, ready, haltedBefore, decision : ...

def advance (s : State E) (e : Event E) (req : Request) (ready : Bool) : State E

copy

ポイントは、attempt(操作の試行)・prune(保存期限切れの削除)・reprofile(プロファイル変更) という3種のコマンドを任意順に並べたコマンド列に対して、監査時点で生き残る各レコードについての一貫性を証明したところにあります。中核定理 history_evidence_chain は、空の履歴から任意のコマンド列を実行した後の状態について、次を同時に保証します:

  • ログ保存(Art. 12 / 19): pruning を挟んでも、カットオフ時点で有効期限内のレコードは失われない

  • 実行の権限条件(Art. 14): executed 状態のレコードは、必ず「停止していない・allow 要求・ready・コンテキスト一致」で捕捉されている

  • プロファイル変更の無害性(Art. 14): 後からのプロファイル書き換えが、過去レコードの意味を遡って変えない。停止状態は再開されない

  • 分類の排他網羅(Art. 72): 残ったレコードは、監視プランに照らして「正常」と「レビュー要」に重複なく過不足なく分かれ、重複回数も保存される

  • 文書・プラン整合(Art. 11 / 72): 「正常」判定を受けるには現行の文書とそれが指すプラン版が一致している必要がある。不一致なら強制的にレビュー送り

  • 証拠出力の情報保存(Art. 43): 左逆関手(事後に復元可能なエクスポート)が与えられたとき、ポリシー上区別すべき証拠は出力後も区別可能なまま

一番地味で、しかし一番効くのは run_without_pruning という補題です。これは「attempt・prune・reprofile が任意に交ざった実行」と「同じ操作列から prune だけ抜いた参照実行」の間に、SameAt という関係(プロファイル一致・停止状態一致・残存履歴一致)が終始保たれることを、コマンド列への帰納法で示します。これにより、「retention 処理が最終的な監査対象を silently 変えていない」ことがモデル上で担保される。参照実行との関係不変量を維持する設計で、コマンド列への帰納を必要とする証明です。

CI は GitHub Actions 上で Lean 4.26.0 をインストールし、EUAIActMapping をビルド、ソースを warningAsError=true で検査します。CIはGitHub Actions上でLean 4.26.0を導入し、EUAIActMapping のビルドと warningAsError=true によるソース検査を実行します。現在公開している EUAIActMapping.lean はこの検証を通過しており、ソース中に sorry / admit は含まれていません。 ただし、現在のCIは別途 #print axioms による公理依存監査までは実施していません。

再現したい方は lake update && lake exe cache get && lake build EUAIActMapping で手元でも走ります。


何を証明していないか

ここが、おそらく技術側の読者が一番見たい箇所です。README に書いてある通りですが、記事側でも明示します。

  • 法文→形式仕様の対応の妥当性は、Lean の外にあります。たとえば「コンテキストの完全一致」を support の判定条件に採用していますが、これは私たちの保守的な実装選択であって、Act がこのデータ構造を要求しているという主張ではありません。対応の妥当性は、法務・標準化の専門家による評価の対象です。

  • 物理的な safe stop、耐久性のあるストレージ、人間のオペレータの能力、文書の真正性は、モデルに含まれません。stop が「論理的に停止扱いになる」ことと、現実の AI システムが安全に止まることは別です。

  • advance を経由しない実装は、この証明の射程外です。デプロイ時に実行経路がこの参照遷移を迂回できるなら、Lean の証明は何も保証しません。

  • 過去ログに依存して制御判断を行う実装(異常検知、傾向ベースの判断など)に対しては、run_without_pruning の前提が成立しません。別途、精緻化(refinement)の議論が必要です。これは市販後モニタリングの実務的な本丸でもあり、次の拡張テーマの一つです。

  • CI は #print axioms の監査を現在は行っていません。全証明が標準公理(propext, Classical.choice, Quot.sound)のみに依存していることまで CI で担保するのは、次のアップデートで戻す予定です。

これらは「できていないからダメ」というより、「形式検証プロジェクトとして、どこまでが機械で担保されていて、どこからが人間の判断に委ねられているか」を明示することそのものに価値がある、という立場です。曖昧な全称主張ではなく、具体的な predicate と反例可能な前提で境界線を引く——これが assurance の技術的な作法だと考えています。


どうしてこれが仕事になりうるか

AI assurance / 規制対応の技術側に関わる方なら、この種の仕様固定が実務のどこで効くか、イメージがつくと思います。参考までに具体的な接点を挙げると、次のようなものです。

  • 適合性評価の準備: 「どの不変条件を、どのコード経路で保っているか」を事前に仕様として外部化しておくことで、第三者による評価の論点が「ドキュメントの解釈」から「仕様の確認」にずれます。

  • 内部監査・デューデリジェンス: ガバナンスの建付けが曖昧なスライドではなく、反証可能な predicate の集合として提示できる。

  • ベンダー間・部門間のコントラクト: 「ログを保存している」ではなく「advance を経由した全操作について、retainUntil 期限前の prune は行わない」のような、検証可能な契約条項に落とせる。

  • 技術標準化・業界団体での議論: 共通の参照モデルがあると、各社の実装差を比較可能な軸ができる。

もちろん、公開した参照モデルがそのまま商用システムに使えるわけではありません。本物のデプロイには、認証・物理的な停止機構・耐久ストレージ・組織的なフォローアップ・運用プロセスなど、Lean の外側の設計が大量に必要です。この公開はその一番内側の「仕様の核」を叩き台として置いた、という位置づけです。この層を実際のシステム設計に接続する部分で、仕事を募集しています(連絡先は末尾)。


なぜ公開したか

形式手法 × AI規制の接続について、具体的な参照モデルと機械検証可能な仕様を公開し、議論できる形にすることには意味があると考えています。

各社がクローズドに取り組んでも、「仕様の書き方」自体が共通言語化されないと、評価者・被評価者・ベンダーの間で噛み合わない議論が繰り返されます。叩き台を一つ公開することで、同じ問題意識の人と技術レベルの対話を始めたい、というのが主な動機です。


 
 
 

コメント

bottom of page