論文の概要: Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
- arxiv url: http://arxiv.org/abs/2608.29134v1
- Date: Sat, 29 Aug 2026 08:23:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:35.597793
- Title: Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
- Title（参考訳）: セキュリティトークンに対する型付き規制アクションの機械化:セマンティックス、ファルシフィケーション、境界EVMエビデンス
- Abstract要約: セキュリティ標準は、特権転送、凍結、リカバリ、コンプライアンスメカニズムを公開している。
メカニズムは、実行中の法的効果や、それに付随する証拠やリバース義務をそれ自体は特定しない。
本稿では,ERC-8319の6つの規制行動候補であるFREEZE Seizeに対する参照実行セマンティクスを示す。
- 参考スコア（独自算出の注目度）: 9.32030540168344
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Security-token standards expose privileged transfer, freezing, recovery, and compliance mechanisms, but a mechanism does not by itself identify the legal effect being executed or the evidence and reversal obligations attached to it. We formalize in Isabelle/HOL a reference execution semantics for the six regulatory-action meanings proposed in ERC-8319: FREEZE, SEIZE, CONFISCATE, LIQUIDATE, RESTRICT, and RECOVER. The model distinguishes applied, rejected, and operational-failure outcomes and mechanizes reversal, replay, epoch, frame, case-local terminality, and receipt properties; the build has no unproved placeholders or added axioms. It proves an external-truth boundary: two concrete worlds that disagree about title, settlement, and entitlement induce the same kernel observation, so those external facts cannot be established from bound inputs. Constructive witnesses and direct mutations show reachability and falsification 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 current publication profile qualifies all seven evidence packages and all 49 Core and 24 mandatory Supporting obligations with no partial credit; six optional obligations remain unclaimed. A mechanized abstraction relation is proved unique and functional under pinned-runtime premises, and package and row corollaries yield conditional, profile-scoped refinement theorems from hash-bound certificates. These results do not constitute a complete Isabelle-to-Solidity-to-EVM refinement theorem, compiler correctness, an audit, production readiness, or deployment verification. The contribution is a machine-checked domain semantics and a falsifiable map of what is proved, what is bounded evidence, what is assumed, and what remains open for a regulated-token execution standard.
- Abstract（参考訳）: 安全基準は、特権移転、凍結、回復、コンプライアンスのメカニズムを規定するが、そのメカニズムは、実行中の法的効果や、それに付随する証拠やリバース義務をそれ自体が特定するものではない。
我々はIsabelle/HOLにおいて、FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT、RECOVERの6つの規制アクションの意味の参照実行セマンティクスを定式化した。
モデルは適用、拒否、運用の失敗の結果を区別し、リバーサル、リプレイ、エポック、フレーム、ケースローカルの終端性、レセプションプロパティを機械化する。
タイトル、解決、権利について意見の一致しない2つの具体的な世界は、同じカーネル観察を誘導するので、これらの外部事実は境界入力から確立できない。
建設的な目撃者や直接突然変異は、宣言された欠陥セットの到達性とファルシフィケーションを示す。
1つのERC-TRUST Solidity/EVM候補に対して、Foundry、Certora、Kontrol/KEVM、突然変異、決定論的ビルド、実行時同一性エビデンスを別々に報告する。
現在の出版プロファイルは、7つのエビデンスパッケージと、49のコアと24の強制的なサポート義務の全てを、部分的な信用を持たないものと定めているが、6つのオプション義務は未定のままである。
機械的抽象化関係はピン付き実行時の前提の下で一意かつ機能的に証明され、パッケージと行の行はハッシュバウンド証明書から条件付き、プロファイルスコープ化された洗練定理を導出する。
これらの結果は、完全な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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。