論文の概要: 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エビデンス
- Authors: Jinwook Kim,
- 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の洗練、コンパイラの正しさ、監査の完了、製品の準備、デプロイメントの検証、外部の法的な真実を確立していない。
それらは、マシンチェックされたドメインセマンティクスと、証明された、バウンドされた、仮定された、そしてオープンな結果の明示的なマップを提供する。
関連論文リスト
- Twin Worlds: Equivariance-Based Abstention for Evidence-Grounded Reasoning [38.63002496590365]
本稿では,知識集約的推論における信頼性向上のための枠組みを提案する。
重要な要因は、文脈における実体の言及が記憶された関連を活性化し、モデルが証拠に埋もれていないプラウシブルな応答を生成することである。
我々は、パラメトリックな先行値を減らしながら関係構造を保ちつつ、元の入力の型付き置換によって複数の世界を構築する。
論文 参考訳（メタデータ） (2026-08-28T07:33:29Z) - From Trajectories to Evidence: Auditable Experimental Records for Industrial Research Agents [47.678562263387214]
研究エージェントは、産業レコメンデーション設定において、多段階の機械学習実験をますます実施している。
生成されたアーティファクトは、サポートされないか、不完全かもしれないし、実行されたラウンドは無効かもしれないし、あるいは廃止されるかもしれないし、後の修正は、以前の発見を曖昧にするかもしれない。
本稿では,連続的アーティファクトのバウンダリ検証と実行後のクレーム資格を結合するエビデンス・グラウンド・フレームワークを提案する。
論文 参考訳（メタデータ） (2026-08-05T13:37:38Z) - 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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。