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

EU AI Act（欧州AI法、Regulation (EU) 2024/1689）は段階的に適用が進んでおり、高リスクAIシステムについては、技術文書、自動ログ、人間による監督、ログ保存、適合性評価、市場投入後モニタリングなどの要件が定められています。2026年のDigital Omnibusによる改正後、高リスクAI規則の適用時期も段階化されています。

条文はこれらの要求を定めていますが、それを実装上どのような条件や不変条件として表現し、機械的に検証するかは別の設計問題です。この間を仕様の形で接続する一つの試みを公開しました。

• リポジトリ: https://github.com/GhostDriftTheory/responsibility-os-eu-ai-act-mapping
• 一次文献: https://eur-lex.europa.eu/eli/reg/2024/1689/oj
• 使用ツール: Lean 4（定理証明支援系）、mathlib4、GitHub Actions

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

何を作ったか

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

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

中核となる型は、次のようなものです（抜粋・簡略化）。

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 := ...

ポイントは、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 によるソース検査を実行します。現在公開している EUAIActMapping.lean はこの検証を通過しており、ソース中に sorry / admit は含まれていません。 ただし、現在のCIは別途 #print axioms による公理依存監査までは実施していません。

再現したい方は、次のコマンドで手元でも実行できます。

lake update
lake exe cache get
lake build EUAIActMapping
lake env lean -DwarningAsError=true EUAIActMapping.lean

何を証明していないか

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

• 法文→形式仕様の対応の妥当性は、Leanの外にあります。 たとえば「コンテキストの完全一致」をsupportの判定条件に採用していますが、これは私たちの保守的な実装選択であって、Actがこのデータ構造を要求しているという主張ではありません。対応の妥当性は、法務・標準化の専門家による評価の対象です。
• 物理的なsafe stop、耐久性のあるストレージ、人間のオペレータの能力、文書の真正性は、モデルに含まれません。stop が「論理的に停止扱いになる」ことと、現実のAIシステムが安全に止まることは別です。
• advance を経由しない実装は、この証明の射程外です。デプロイ時に実行経路がこの参照遷移を迂回できるなら、Leanの証明は何も保証しません。
• 過去ログに依存して制御判断を行う実装（異常検知、傾向ベースの判断など）に対しては、run_without_pruning の前提が成立しません。別途、精緻化（refinement）の議論が必要です。これは市場投入後モニタリングの実務的な本丸でもあり、次の拡張テーマの一つです。
• CIは #print axioms の監査を現在は行っていません。 Leanによるビルドとstrict source checkを通していますが、公理依存の追加監査は今後の拡張候補です。

これらは「できていないからダメ」というより、「形式検証プロジェクトとして、どこまでが機械で担保されていて、どこからが人間の判断に委ねられているか」を明示することそのものに価値がある、という立場です。

曖昧な全称主張ではなく、具体的なpredicateと反例可能な前提で境界線を引く。これがassuranceの技術的な作法だと考えています。

実務のどこに接続できるか

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

• 適合性評価の準備: 「どの不変条件を、どのコード経路で保っているか」を事前に仕様として外部化しておくことで、第三者による評価の論点を「ドキュメントの解釈」だけでなく「仕様と実装の対応確認」に移せる
• 内部監査・デューデリジェンス: ガバナンスの建付けを曖昧なスライドではなく、反証可能なpredicateの集合として提示できる
• ベンダー間・部門間のコントラクト: 「ログを保存している」ではなく、「advance を経由した全操作について、retainUntil 期限前の prune は行わない」のような、検証可能な条件に落とせる
• 技術標準化・業界団体での議論: 共通の参照モデルがあると、各社の実装差を比較可能な軸をつくれる

もちろん、公開した参照モデルがそのまま商用システムに使えるわけではありません。本物のデプロイには、認証・物理的な停止機構・耐久ストレージ・組織的なフォローアップ・運用プロセスなど、Leanの外側の設計が大量に必要です。

この公開は、その一番内側の「仕様の核」を叩き台として置いた、という位置づけです。実際のシステム設計・監査・適合性評価プロセスへの接続について、共同検討・実証のご相談を歓迎します。

なぜ公開したか

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

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

内容への批判・改善提案・「ここは実務とズレている」という指摘を、Issueまたは直接の連絡で歓迎します。特に、法務・標準化側の方から「このpredicateはActのこの箇所の意図と違う」というレビューをいただけると、プロジェクトの価値は大きく上がります。

---

技術スタック: Lean 4.26.0, mathlib4, GitHub Actions
依存: ResponsibilityOS Kernel（圏論ベースのカーネル。本リポジトリはこれをimportし、改変なしで利用）
https://github.com/GhostDriftTheory/responsibility-os-kernel
ライセンス: All rights reserved（問い合わせベース）
連絡先: （ここに連絡手段を記載）