論文の概要: Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation
- arxiv url: http://arxiv.org/abs/2605.01037v1
- Date: Fri, 01 May 2026 19:04:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-05 20:33:49.549592
- Title: Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation
- Title（参考訳）: 認知的ワークフロー実行者に対する認証された純度:静的解析から暗号検査へ
- Abstract要約: 以前の3層ガバナンスアーキテクチャは、ガバナンスの完全性、証明の完全性、そして過度な効果の不可能性を証明します。
本稿は4つのメカニズムを通してギャップを埋める。
構成による構造的純度、BEAMの5つのバイパスクラスすべてに対する排除、証明書の完全性、ゲート完全性という4つの定理を証明します。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: We present a certified purity architecture that converts governance enforcement in cognitive workflow systems from a runtime convention into a structural capability boundary. A prior three-layer governance architecture proves governance completeness, provenance completeness, and the impossibility of ungoverned effects, conditional on the pure module constraint: that step executors cannot perform effects. That constraint was enforced by module import graph analysis, which is insufficient against adversarial bypass on the BEAM virtual machine. This paper closes the gap through four mechanisms: (1) a restricted WebAssembly compilation target where effect-producing instructions are structurally absent; (2) purity certificates, cryptographically signed proofs binding executor binaries to their import classifications; (3) a runtime verification gate that rejects uncertified executors before they enter the governance pipeline; and (4) portable governance credentials via remote attestation for cross-organizational verification. We prove four theorems: structural purity by construction, bypass elimination for all five BEAM bypass classes, certificate integrity, and gate completeness. The guarantee holds relative to an explicit Trusted Computing Base. Evaluation on four implemented executors shows verification latency of 39--42 us, full plan cycle under 400 us, runtime overhead under 0.4% of a 100 ms HTTP request, and zero determinism divergences across repeated invocations.
- Abstract（参考訳）: 本稿では,認知ワークフローシステムにおけるガバナンスの実施をランタイムの慣行から構造的能力境界に変換する,認定された純粋度アーキテクチャを提案する。
以前の3層ガバナンスアーキテクチャは、ガバナンスの完全性、証明の完全性、そして、純粋なモジュール制約に条件づけられた、余分なエフェクトの不可能性を証明します。
この制約は、BEAM仮想マシンの逆バイパスに対して不十分なモジュールインポートグラフ解析によって実行された。
本稿では,(1)エフェクト生成命令が構造的に欠落している制限されたWebAssemblyコンパイルターゲット,(2)純粋性証明,(2)暗号署名された暗号署名によるエグゼクタバイナリのインポート分類へのバインディング,(3)ガバナンスパイプラインに入る前に未認証エグゼクタを拒否する実行時検証ゲート,(4)組織間検証のためのリモート認証によるポータブルガバナンス認証,の4つのメカニズムでギャップを埋める。
構成による構造的純度、BEAMの5つのバイパスクラスすべてに対する排除、証明書の完全性、ゲート完全性という4つの定理を証明します。
この保証は、明示的なTrusted Computing Baseに対して保持される。
4つの実装されたエグゼキュータの評価では、検証のレイテンシは39-42 us、400 us未満のフルプランサイクル、100ミリ秒のHTTPリクエストの0.4%未満のランタイムオーバーヘッド、繰り返し呼び出しにまたがる決定性はばらばらである。
関連論文リスト
- Who Can Make the Action Happen? An Authority-Decomposition Framework for High-Risk Automated Systems [8.71734630214811]
本稿では,信頼領域の連立関係が保護された実行を引き起こすのに十分である行動関連手法を提案する。
これは、実行に対する因果制御と、操作の権威的アカウントの制御を分離する。
インクルージョン最小限の連立と、要求される実行境界が指定された上流ドメインから独立しているかどうかのテストが導かれる。
論文 参考訳（メタデータ） (2026-08-19T14:30:58Z) - ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。
itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
論文 参考訳（メタデータ） (2026-07-07T22:05:55Z) - A Five-Plane Reference Architecture for Runtime Governance of Production AI Agents [0.0]
本稿では,生産AIエージェントのガバナンスのための参照アーキテクチャを提案する。
我々は、許容と否定を一般化する6つの割り込みプリミティブの分類を定義し、4つの正当性不変量について主張する。
5つの具体的判断にまたがる7つの生産エージェントの脅威の隠蔽を実証する。
論文 参考訳（メタデータ） (2026-06-10T16:54:47Z) - Sovereign Assurance Boundary: Certificate-Bound Admission for Agentic Infrastructure [2.124730017640531]
Sovereign Assurance境界は、自動実行権限のための証明書バウンドランタイムアクセス層である。
本稿では,エアロックブローカーのアーキテクチャを詳述し,その入力と取り消しの不変性を定式化し,Goプロトタイプの予備実現可能性の測定結果を報告する。
論文 参考訳（メタデータ） (2026-06-10T03:49:57Z) - Ontological Knowledge Blocks: Executable Compliance and Profile-Based Validation for Trustworthy AI Systems [0.0]
本稿では,規制義務を機械チェック可能な制約にコンパイルするプログラム可能なガバナンス基盤であるオントロジー知識ブロック(OKB)を紹介する。
決定論的規制コンパイラは構造化された中間表現(IR)レコードを構成可能なKBモジュールに変換し、プロファイルベースのガバナンス前駆を可能にする。
その結果、プロファイルに敏感な検証、厳密な付加的な違反の蓄積、SHACL検証の再設定のレイテンシーが12.6msから100.3ms、プロファイル等価性テストが厳密な包括的プロファイルとして確認された。
論文 参考訳（メタデータ） (2026-05-22T07:14:31Z) - Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
本稿では,大規模言語モデルを取り巻く決定論的構造化計算を検証するためのフレームワークを提案する。
リーン4の信頼境界アーキテクチャを,現代的なLLMパイプラインの汎用インターフェースに拡張しています。
論文 参考訳（メタデータ） (2026-05-13T12:01:41Z) - TRUST: A Framework for Decentralized AI Service v.0.1 [47.384270414446604]
大規模推論モデル (LRM) とマルチエージェントシステム (MAS) は, 信頼性の高い検証を必要とする。
TRUST(Transparent, Robust, and Unified Services for Trustworthy AI)は,3つのイノベーションを備えた分散フレームワークである。
我々は、悪質な俳優が損失を被っている間、正直な監査人の利益を確実に確保する安全利益理論を証明する。
論文 参考訳（メタデータ） (2026-04-29T19:32:58Z) - GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
マルチチェーンエコシステムの重要な基盤であるクロスチェーンブリッジは、攻撃者にとって主要なターゲットとなっている。
バイトコードレベルの静的解析のような既存の防御は、チェーン間の相互作用のセマンティックな複雑さを扱うには不十分である。
パターンマッチングから体系的な第一原理検証へ自動的なクロスチェーンスマートコントラクト監査を移行するフレームワークであるGoAT-Xを提案する。
論文 参考訳（メタデータ） (2026-04-27T11:34:21Z) - Structural Enforcement of Goal Integrity in AI Agents via Separation-of-Powers Architecture [0.10152838128195464]
Policy-Execution-Authorization (PEA)アーキテクチャは、システムレベルでの安全性を強制する"パワーの分離"設計である。
PEAはインテントの生成、承認、実行を、暗号的に制約された機能トークンを介して接続された独立した分離されたレイヤに分離する。
論文 参考訳（メタデータ） (2026-04-26T10:31:13Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - enclawed: A Configurable, Sector-Neutral Hardening Framework for Single-User AI Assistant Gateways [0.0]
Enclawedは、証明不可能なピア信頼、非定型外部接続、署名付きモジュールローディング、タンパー・エビデント監査パスを必要とするデプロイメントをターゲットとする。
フレームワークには2つのフレーバーがある。オープンフレーバーはOpenClawとの互換性を維持しつつ、監査、分類、データロス防止シグナルを出力する。
実装には、セキュリティレビュー、204ケースのテストスイート、継続的インテグレーション対応のGitHub Actionsが伴います。
論文 参考訳（メタデータ） (2026-04-18T05:10:11Z) - ElephantBroker: A Knowledge-Grounded Cognitive Runtime for Trustworthy AI Agents [45.88028371034407]
ElephantBrokerはオープンソースの認知ランタイムで、Neo4jナレッジグラフとQdrantベクトルストアを統合する。
このシステムは、ハイブリッド5ソース検索パイプラインからなる完全な認知ループ(ストア、検索、スコア、構成、保護、学習)を実装している。
論文 参考訳（メタデータ） (2026-03-26T07:03:12Z) - Agent Control Protocol: Admission Control for Agent Actions [0.4929694290403903]
エージェントコントロールプロトコル(エージェントコントロールプロトコル、ACP)は、B2Bの機関環境における自律エージェントの受け入れ制御ガバナンスのための正式な仕様である。
ACPは、暗号ID、能力に基づく認可、決定論的リスク評価、連鎖デリゲート、および暗号化連鎖監査を定義する。
ACPはRBACとZero Trustの上で動作し、どちらのモデルも解決しない問題に対処する。
論文 参考訳（メタデータ） (2026-03-19T12:28:28Z) - Governing Dynamic Capabilities: Cryptographic Binding and Reproducibility Verification for AI Agent Tool Use [0.0]
既存のセキュリティレイヤでは、AIエージェントに何ができるか、それが主張するものを実行したのか、マルチエージェントインタラクションで何が起きたのかを検証できない。
既存のフレームワークはこれら2つを詳述し、サイレントな能力のエスカレーションを可能にし、検証済みの証明なしに相互作用を残す。
我々は3つのエージェントガバナンス要件を導出する:能力の完全性(G1)、行動の妥当性(G2)、相互作用監査性(G3)。
基本(Ed25519, SHA-256; 97 us verify)と拡張(BBS+選択開示、Groth16 DV-SNARK; 13.8 ms)の2つの暗号に依存しないインスタンス化で検証する。
論文 参考訳（メタデータ） (2026-03-15T11:46:57Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。
最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。
推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
論文 参考訳（メタデータ） (2026-01-19T07:21:19Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Making LLMs Reliable When It Matters Most: A Five-Layer Architecture for High-Stakes Decisions [51.56484100374058]
現在の大規模言語モデル(LLM)は、実行前にアウトプットをチェックできるが、不確実な結果を伴う高い戦略決定には信頼性が低い検証可能な領域で優れている。
このギャップは、人間と人工知能(AI)システムの相互認知バイアスによって引き起こされ、そのセクターにおける評価と投資の持続可能性の保証を脅かす。
本報告では、7つのフロンティアグレードLDMと3つの市場向けベンチャーヴィグネットの時間的圧力下での系統的質的評価から生まれた枠組みについて述べる。
論文 参考訳（メタデータ） (2025-11-10T22:24:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。