論文の概要: Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
- arxiv url: http://arxiv.org/abs/2608.29134v2
- Date: Tue, 01 Sep 2026 08:16:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:35.599186
- Title: Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
- Title（参考訳）: セキュリティトークンに対する型付き規制アクションの機械化:セマンティックス、ファルシフィケーション、境界EVMエビデンス
- Abstract要約: セキュリティ標準は、実行された法的効果や、それが持つ証拠やリバース義務を特定せずに、特権的なコントロールを公開します。
我々はIsabelle/HOLで、FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT、RECOVERの6つのERC-8319の参照実行セマンティクスを定式化する。
- 参考スコア（独自算出の注目度）: 9.32030540168344
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Security-token standards expose privileged controls without identifying the legal effect executed or the evidence and reversal obligations it carries. We formalize in Isabelle/HOL a reference execution semantics for the six ERC-8319 meanings: FREEZE, SEIZE, CONFISCATE, LIQUIDATE, RESTRICT, and RECOVER. It distinguishes applied, rejected, and operational-failure outcomes and mechanizes action-specific reversals, replay and epoch rules, complete frames, case-local terminality, and final receipts; the session builds without unproved placeholders or additional axioms. An indistinguishability theorem shows that bound kernel inputs cannot establish external facts about title, settlement, or entitlement. Constructive witnesses and direct mutations establish reachability and sensitivity for the declared fault set. For one ERC-TRUST Solidity/EVM candidate, we report separately scoped Foundry, Certora, Kontrol/KEVM, mutation, deterministic-build, and runtime-identity evidence. The publication profile qualifies 7/7 reusable packages, 49/49 Core obligations, and 24/24 mandatory Supporting obligations; six optional ERC-3643 obligations remain unclaimed. A current-state abstraction relation is unique and functional under pinned-runtime premises, while package and row corollaries remain conditional on hash-bound certificates. These results do not establish complete Isabelle-to-Solidity-to-EVM refinement, compiler correctness, audit completion, production readiness, deployment verification, or external legal truth. They provide a machine-checked domain semantics and an explicit map of proved, bounded, assumed, and open results.
- Abstract（参考訳）: 安全基準は、実行された法的効果や、それが持つ証拠や反逆的な義務を特定せずに、特権的なコントロールを公開する。
我々はIsabelle/HOLで、FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT、RECOVERの6つのERC-8319の参照実行セマンティクスを定式化する。
適用、拒否、運用の失敗の結果を区別し、アクション固有のリバーサル、再生、エポックルール、完全なフレーム、ケースローカルの終端性、最終レシートを機械化する。
不明瞭性定理は、境界核入力がタイトル、解決、権利に関する外部事実を確立できないことを示している。
構成的目撃者や直接突然変異は、宣言された欠陥セットの到達性と感度を確立する。
1つのERC-TRUST Solidity/EVM候補に対して、Foundry、Certora、Kontrol/KEVM、突然変異、決定論的ビルド、実行時同一性エビデンスを別々に報告する。
7/7再利用可能なパッケージ、49/49コアの義務、24/24強制支援義務を定めているが、6つのオプションのERC-3643義務は未定のままである。
現状の抽象化関係はピン留めされた実行時の前提下ではユニークで機能的だが、パッケージと行のログはハッシュバウンド証明書で条件付きである。
これらの結果は、完全なIsabelle-to-Solidity-to-EVMの洗練、コンパイラの正しさ、監査の完了、製品の準備、デプロイメントの検証、外部の法的な真実を確立していない。
それらは、マシンチェックされたドメインセマンティクスと、証明された、バウンドされた、仮定された、そしてオープンな結果の明示的なマップを提供する。
関連論文リスト
- Cognitive Admission Control: Risk-Conditioned Assurance for Consequential Actions in Agentic Distributed Systems [2.124730017640531]
エージェント分散システムでは、エージェントは外部のインフラを変更できるが、突然変異の実行準備が整っているという証拠は欠如している。
CAC(Cognitive Admission Control)は、この証拠を明示する。
ポリシーは、型付けされた行動とそのモデル化されたリスクを、述語、エビデンスクラス、スコープ、鮮度、証人セットの制約を指定する保証義務にマップする。
承認が成功すると、アクション、証人マニフェスト、ディスパッチタイムガードを結び付ける証明書が生成される。
論文 参考訳（メタデータ） (2026-09-14T20:20:54Z) - From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions [9.27474112226667]
EBL-Coreは、1つの標準的な、完全に実体化されたAI生成候補が、明示的な条件下でアクションスコープ実行権限を受け取ることができるかどうかを決定する。
拘束力、政策非監視、エビデンス処理、決定論的判断、検証、ライフサイクル行動の付与などである。
100回の試験で32回の同時再空輸試験が成功し、1回の試行で完全に1回成功し、テスト効果が保護された。
論文 参考訳（メタデータ） (2026-09-10T14:21:45Z) - ContractEval: Query-Conditioned Execution Matching for Procedural Instruction Conformance [2.547425976804939]
手続き的義務を明確にするための診断フレームワークであるConTRACTEVALを紹介する。
これは、手続き的な指示をクエリアクティブな義務として表現し、それらを応答や痕跡証拠と照合する。
ContractEvalはコンプライアンス保証ではない。最終回答の品質を暗黙にするのではなく、手続き順応を監査可能にする。
論文 参考訳（メタデータ） (2026-09-08T21:21:16Z) - Twin Worlds: Equivariance-Based Abstention for Evidence-Grounded Reasoning [38.63002496590365]
本稿では,知識集約的推論における信頼性向上のための枠組みを提案する。
重要な要因は、文脈における実体の言及が記憶された関連を活性化し、モデルが証拠に埋もれていないプラウシブルな応答を生成することである。
我々は、パラメトリックな先行値を減らしながら関係構造を保ちつつ、元の入力の型付き置換によって複数の世界を構築する。
論文 参考訳（メタデータ） (2026-08-28T07:33:29Z) - AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
AIスロープ(AI slop)は、アーティファクト、幻覚的脆弱性、可視だが正しくないパッチ、セマンティックに再パッケージされたバグレポートである。
本稿では,実証的証拠を調査し,統一メカニズムを特定し,信頼に値するトリアージへの道筋をたどる。
論文 参考訳（メタデータ） (2026-08-26T11:48:38Z) - Testing and Evaluation of Agentic AI Systems In Military Command and Control [0.6273214774587439]
エージェントAIシステムは、厳格なテストと人間の監視に対する公的なコミットメントの下で、軍事指揮統制(C2)のために調達されている。
提案手法は,テスト項目を4つのクラスタに分類した8つの仮定を定式化したものである。
最初の3つの仮定クラスタに対して10の保証クレームを導出し、現在および新興メソッドがそれぞれに対処できるかどうかを評価する。
論文 参考訳（メタデータ） (2026-08-20T22:31:23Z) - EnterpriseRAG: Benchmarking LLM Instruction Adherence and Robustness under Non-Ideal Enterprise Retrieval [41.53357936032648]
既存のベンチマークでは、単純なクエリでクリーンな検索を前提としており、ノイズの多いドキュメントと多次元制約が共存する生産条件をキャプチャできない。
6つのドメインにわたる983のエキスパート検証サンプルのベンチマークであるEnterpriseRAGを紹介します。
ベンチマークと評価のフレームワークを公開していきます。
論文 参考訳（メタデータ） (2026-08-12T02:51:04Z) - From Trajectories to Evidence: Auditable Experimental Records for Industrial Research Agents [47.678562263387214]
研究エージェントは、産業レコメンデーション設定において、多段階の機械学習実験をますます実施している。
生成されたアーティファクトは、サポートされないか、不完全かもしれないし、実行されたラウンドは無効かもしれないし、あるいは廃止されるかもしれないし、後の修正は、以前の発見を曖昧にするかもしれない。
本稿では,連続的アーティファクトのバウンダリ検証と実行後のクレーム資格を結合するエビデンス・グラウンド・フレームワークを提案する。
論文 参考訳（メタデータ） (2026-08-05T13:37:38Z) - Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair [36.56438114281786]
正しいパッチの発見と保持、検証、提出のギャップについて検討する。
我々はエビデンスバウンド型ループ契約を導出し、その機械的に強制可能なサブセットを参照実装でインスタンス化する。
論文 参考訳（メタデータ） (2026-07-27T16:05:23Z) - TRACE-CTI: Auditable Post-Extraction Governance of TTP Claims with Knowledge Graphs [4.960649631468518]
TRACE-CTIは、抽出後のクレーム管理フレームワークである。
実行レベルの予測を構成レベルのGraphAssertionに集約する。
これはConsensusAssertionsとしてセットアップdedlicated corroborationを具体化する。
論文 参考訳（メタデータ） (2026-07-27T15:33:18Z) - The SIGReg Objective as Variational Free Energy: A Theoretical Active-Inference Account of JEPA World Models [47.471225029744424]
JEPA(Joint-Embedding Predictive Architectures)は、潜在世界モデルの主要な設計である。
本稿では,JEPAのトレーニング目標である予測損失と重み付き埋め込み正規化の選択肢が,有効能動推論(AIF)変動自由エネルギーであるか否かを判定する。
論文 参考訳（メタデータ） (2026-07-15T08:59:36Z) - Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs [0.564046562677526]
リーン4ベースのツールコールアーキテクチャが経験的クレームを管理するのにどのように使用できるかを示します。
検証されたすべての出力は、検査済みのツールコールと、有効な推論のカーネルチェックされたチェーンから構造的に下降する。
正式なサイドカーは、目標命題、ソーススコープ、エビデンス境界、証明義務、棄権条件を監査可能にする。
時間とともに、データセット、API、公開レコード、AI生成ドキュメントの型付きサイドカーは、この形式化の負担を再利用可能なインフラストラクチャに戻すことができる。
論文 参考訳（メタデータ） (2026-07-14T11:33:44Z) - DeepSciVerify: Verifying Scientific Claim--Citation Alignment via LLM-Driven Evidence Escalation [39.146761527401424]
本稿では,科学的クレーム引用検証のための2段階パイプラインであるDeepSciVerifyを紹介する。
このシステムはまず, 要約を用いてクレームを検証し, 必要な場合にのみ全文を検索, 解析する。
論文 参考訳（メタデータ） (2026-05-26T21:33:29Z) - Partial Evidence Bench: Benchmarking Authorization-Limited Evidence in Agentic Systems [0.0]
本稿では、その故障モードを測定するための決定論的ベンチマークであるPartial Evidence Benchを紹介する。
このベンチマークでは、デューディリジェンス、コンプライアンス監査、セキュリティインシデント対応の3つのシナリオファミリが提供されている。
答えの正しさ、完全性意識、ギャップレポートの品質、安全でない完全性行動の4つの面に沿ってシステムを評価する。
論文 参考訳（メタデータ） (2026-05-06T19:01:29Z) - Preregistered Belief Revision Contracts [2.28438857884398]
PBRC(Preregistered Belief Revision Contracts)は,オープン通信と許容可能な変更を分離するプロトコルレベルのメカニズムである。
PBRC契約は、ファーストオーダーのエビデンストリガー、許容可能なリビジョンオペレータ、優先ルール、フォールバックポリシーを公に修正する。
本報告では,信頼軌道と正準化された監査トレースを保存したPBRC正規形式を,監査可能なトリガープロトコルで認めていることを示す。
論文 参考訳（メタデータ） (2026-04-16T22:22:54Z) - When Verification Fails: How Compositionally Infeasible Claims Escape Rejection [30.404615085122046]
既存の検証ベンチマークでは,厳密なクレーム検証と簡易な塩分制約依存を区別できないことを示す。
有意な制約が支持されるが、非有意な制約が矛盾する場合に、構成的に不可能なクレームを構築する。
モデル間の差は,基礎的推論能力よりも検証しきい値の差を反映していることを示す。
論文 参考訳（メタデータ） (2026-04-13T04:48:20Z) - DEFAME: Dynamic Evidence-based FAct-checking with Multimodal Experts [35.952854524873246]
Dynamic Evidence-based FAct-checking with Multimodal Experts (DEFAME)は、オープンドメイン、テキストイメージクレーム検証のためのゼロショットMLLMパイプラインである。
DEFAMEは6段階のプロセスで動作し、ツールと検索深度を動的に選択し、テキストおよび視覚的証拠を抽出し、評価する。
論文 参考訳（メタデータ） (2024-12-13T19:11:18Z) - AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
実世界の情報ニーズから10kクレームを抽出したファクトチェックデータセットであるAmbiFCを提示する。
アンビFCの証拠に対する主張を比較する際に,曖昧さから生じる不一致を分析した。
我々は,このあいまいさをソフトラベルで予測するモデルを開発した。
論文 参考訳（メタデータ） (2021-04-01T17:40:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。