有限状態モデルで判断に必要な観測項目を最小化する
Compiling Sufficient Governance Context from Declared Losses and Reachable States: Exact Observation-Contract Synthesis with Cardinality and Cost Objectives
この論文をやさしく読む
ひとことで言うと
許可や拒否などの判断に本当に必要な観測項目を、有限の状態モデルの中で漏れなく特定し、項目数や費用を抑えて選びます。
何に役立つ？
考えられる用途は、判断ゲートで集める情報を減らしつつ、あらかじめ決めた判定を全到達状態で再現する設計です。
この研究の面白いところ
個々に欠かせない属性を集めるだけでは十分とは限らない点を示し、最小項目数と最小費用の目的も区別しています。費用が同率だった結果も報告しています。
どこまで分かった？
保証は与えた有限モデルと宣言済み判定に対するものです。成功時の出力は検査要約で、独立検証可能な証明書ではありません。全工程の事例研究は今後の作業です。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
本論文が導出し検証する対象を、最小十分ガバナンス文脈と呼ぶ。有限の到達可能状態モデル、決定的な宣言済み判定、観測候補属性が与えられたとき、十分な観測集合を計算し、個別に不可欠な属性と、集合として十分な契約を区別し、要素数または宣言済み費用の目的に従って十分な契約から選択する。観測契約とは、その値によってすべての到達可能状態で宣言済み判定が決まる候補属性の集合である。権限契約とは、目的に従って選ばれ、ゲートのスキーマに結び付けられた契約である。全列挙の費用が許容できる場合は包含関係に関して極小な十分契約をすべて合成し、それ以外の場合はSAT/MaxSAT符号化によって要素数最小または費用最小の契約を合成し、十分性を直接検査する。人工的に構成したコード・クラウド領域では、個別に不可欠な属性の中核だけでは観測契約として十分でなく、異なる二つの縮約が存在する。事前登録した費用モデルは両者を厳密に区別する。第二の、より大きな人工領域でも同じパターンが現れるが、その領域の費用モデルでは代替案を区別できない。理由を完全に説明できる費用の同率であり、得られたまま報告する。識別可能性集合族のスケーリングを測定し、登録したタイムアウト内では全列挙が不可能であることを確認する一方、SAT/MaxSATによる合成は1秒を大幅に下回る時間で解けた。MaxSATには、通常のSATに対する要素数上の測定された優位性はなかった。AuthorityBenchは三領域で四つの比較手法を比較し、宣言のみを使う比較手法はいずれの領域でも厳密に十分ではなかった。選ばれたすべての契約について十分性を検査し、失敗時には反例を、成功時には持ち運び可能な証明書ではなく検査要約を出す。これは、二つの範囲を整理した表におけるコンパイラ中心の範囲に当たる。独立に仕様を定めた一貫した全工程の事例研究は、登録済みの後続作業であり、本稿で達成を主張するものではない。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
We call the object this paper derives and certifies a minimal sufficient governance context: given a finite reachable-state model, a deterministic declared verdict, and candidate observable attributes, we compute sufficient observation sets, distinguish attributes that are individually indispensable from contracts that are jointly sufficient, and select among sufficient contracts under a cardinality or declared-cost objective. An observation contract is a set of candidate attributes whose values determine the declared verdict on every reachable state; an authority contract is one selected under an objective and bound to a gate schema. We synthesize every inclusion-minimal sufficient contract where exhaustive enumeration is affordable, and a minimum-cardinality or minimum-cost contract by SAT/MaxSAT encoding otherwise, checking sufficiency directly. On a constructed code/cloud domain, the individually-indispensable core is not sufficient as an observation contract and two distinct reducts exist; a preregistered cost model separates them exactly. On a second, larger, constructed domain, the same pattern recurs, but that domain's cost model does not separate the alternatives: a fully explained cost tie, reported as found. We measure discernibility-family scaling where exhaustive enumeration is confirmed infeasible within a registered timeout, while SAT/MaxSAT synthesis solves in well under a second; MaxSAT showed no measured cardinality advantage over plain SAT. AuthorityBench compares four baselines across three domains; the declared-only baseline is not exactly sufficient on any. Every selected contract is checked for sufficiency, with a counterexample on failure and a check summary, not a portable certificate, on success -- the compiler-focused scope of a two-scope table; an independently specified end-to-end case study is registered follow-up work, not claimed here.
著者のコメント
Code, data, preregistration tags, review record, and independent reproduction (repository issue #3): https://github.com/besanson/sarc-authority-derivation. Artifact DOI: 10.5281/zenodo.22884173
arXiv ID: 2609.26016 ／ 要約の誤りについて