論文の概要: Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
- arxiv url: http://arxiv.org/abs/2604.03844v1
- Date: Sat, 04 Apr 2026 19:50:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-07 15:49:18.79475
- Title: Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
- Title（参考訳）: ビザンチン断層下のクロスドメイン状態保存の安全性と活力:Isabelle/HOLにおける機械的証明
- Authors: Jinwook Kim,
- Abstract要約: 本稿では,Isabelle/HOLにおける2,348行の機械的証明について述べる。
第一に、クロスドメイン状態保存(安全): 1つのドメインで実行される規制状態遷移は、構造保存を伴うすべての連結ドメインに忠実に反映される。
第2に、ビザンツの断層の下での生活: 最大 f n/3 のビザンツのノードの存在下で、我々は、矛盾する規制行動、デッドロックの自由、飢餓の自由の決定論的解決を証明した。
- 参考スコア（独自算出の注目度）: 9.32030540168344
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formally guaranteeing the safety and liveness of regulatory state transitions in cross-domain state synchronization systems is a problem of growing importance as tokenized assets are increasingly operated across heterogeneous blockchain networks and off-chain ledgers. This paper presents a mechanized proof of 2,348 lines in Isabelle/HOL establishing two complementary properties. First, cross-domain state preservation (safety): a regulatory state transition performed on one domain is faithfully reflected across all connected domains with structural preservation. This guarantee encompasses bidirectional roundtrip preservation, consistency across an arbitrary finite set of domains, and per-asset isolation. Second, liveness under Byzantine faults: in the presence of up to f < n/3 Byzantine nodes, we prove deterministic resolution of conflicting regulatory actions, deadlock freedom, and starvation freedom. In the combination of these two properties, the liveness proof discharges the honest-node assumption of the safety proof under Byzantine faults, promoting conditional safety to an unconditional guarantee. The seven generic locales derived in this process are domain-independent and reusable for arbitrary domains via Isabelle/HOL's interpretation mechanism. The application context is a regulatory state transition model based on the RCP framework (arXiv:2603.29278), which systematizes 31 requirements from 15 global financial regulatory authorities. All proof artifacts build in Isabelle/HOL without sorry or oops, have been submitted to the Archive of Formal Proofs (under review), and are publicly available on GitHub.
- Abstract（参考訳）: クロスドメイン状態同期システムにおける規制状態遷移の安全性と活力を保証することは、異種ブロックチェーンネットワークとオフチェーン台帳の間でトークン化された資産がますます運用されるにつれて、重要性が増す問題である。
本稿では,Isabelle/HOLにおける2,348行の機械的証明について述べる。
第一に、クロスドメイン状態保存(安全): 1つのドメインで実行される規制状態遷移は、構造保存を伴うすべての連結ドメインに忠実に反映される。
この保証には、双方向のラウンドトリップ保存、任意の有限個のドメイン間の一貫性、アセット単位の分離が含まれる。
第2に、ビザンツの断層下での生活: 最大 f < n/3 のビザンツのノードの存在下では、矛盾する規制行動、デッドロックの自由、飢餓の自由の決定論的解決が証明される。
これら2つの性質を組み合わせることで、活力証明はビザンツ断層の下での安全証明の真正極仮定を放出し、条件付き安全を無条件保証に促進する。
この過程で引き起こされた7つの一般的なローカライズはドメインに依存しず、イザベル/HOLの解釈機構を介して任意のドメインに対して再利用可能なものである。
アプリケーション・コンテキストはRCPフレームワーク(arXiv:2603.29278)に基づく規制状態遷移モデルであり、世界15の金融規制当局から31の要件を体系化している。
Isabelle/HOLにビルドされたすべての証明成果物は、残念なことに、あるいは、おっしゃらずに、形式的証明のアーカイブ(レビュー)に提出され、GitHubで公開されている。
関連論文リスト
- Towards Domain-Generalized Open-Vocabulary Object Detection: A Progressive Domain-invariant Cross-modal Alignment Method [59.30562121800656]
Open-Vocabulary Object Detectionは、新しいカテゴリへの一般化において大きな成功を収めた。
我々は、OVODパラダイムの原則的な見直しを行い、根本的な脆弱性を明らかにする。
PICA(Progressive Domain-invariant Cross-Modal Alignment)を提案する。
論文 参考訳（メタデータ） (2026-03-29T07:39:31Z) - PEB Separation and State Migration: Unmasking the New Frontiers of DeFi AML Evasion [9.196953891529043]
転写層属性の完全性を損なう2つの構造機構を定式化する。
転送層トレーシング機能の拡張は、基礎となる属性の曖昧さを解決するのに失敗する、と我々は主張する。
我々は,実行セマンティクスに基づくAMLへのパラダイムシフトを提唱する。
論文 参考訳（メタデータ） (2026-03-27T10:58:54Z) - Byzantine-Robust and Differentially Private Federated Optimization under Weaker Assumptions [89.52532304099522]
フェデレートラーニング(FL)は、クライアントが生データを集中せずに共有モデルを共同でトレーニングすることを可能にし、固有のプライバシーレベルを提供する。
グラデーションとモデル更新は機密情報を漏洩する可能性があるが、悪意のあるサーバはビザンティン操作のような敵攻撃をマウントする可能性がある。
これらの脆弱性は、統合されたフレームワーク内の差分プライバシー(DP)とビザンチンの堅牢性に対処する必要性を強調している。
Byz-Clip21-SGD2Mを提案する。
論文 参考訳（メタデータ） (2026-03-24T17:39:09Z) - 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) - On the Formal Limits of Alignment Verification [0.24049560288708582]
AIの安全性に関する根本的な疑問は、アライメントが正式に認定されるかどうかである。
検証手順が3つの特性を同時に満たさないことを証明する。音性(不整合系が認定されない)、一般性(検証は時間内に実行される)、トラクタビリティである。
その結果、完全なニューラルネットワーク検証の計算複雑性、行動観察による内部目標構造の非識別性、無限領域上で定義された特性に対する有限証拠の限界という3つの独立した障壁が導かれる。
論文 参考訳（メタデータ） (2026-03-08T23:03:21Z) - Why Does the LLM Stop Computing: An Empirical Study of User-Reported Failures in Open-Source LLMs [50.075587392477935]
オープンソースのDeepSeek、Llama、Qwenのエコシステムから、705の現実世界の失敗に関する大規模な実証的研究を行った。
ホワイトボックスオーケストレーションは、モデルアルゴリズムの欠陥からデプロイメントスタックのシステム的脆弱性へと、信頼性のボトルネックを移動させます。
論文 参考訳（メタデータ） (2026-01-20T06:42:56Z) - Global-focal Adaptation with Information Separation for Noise-robust Transfer Fault Diagnosis [48.69961294481149]
ノイズ条件下でのドメイン横断故障診断のための情報分離グローバル焦点対向ネットワーク(ISGFAN)を提案する。
ISGFANは、ドメイン不変のフォールト表現を分離するために、逆学習と改善された損失を統合する情報分離アーキテクチャ上に構築されている。
3つの公開データセットで行った実験は、提案手法が他の顕著な既存手法よりも優れていることを示した。
論文 参考訳（メタデータ） (2025-10-16T01:13:06Z) - Boundary-to-Region Supervision for Offline Safe Reinforcement Learning [56.150983204962735]
バウンダリ・トゥ・レギオン(Bundary-to-Region, B2R)は、コスト信号による非対称な条件付けを可能にするフレームワークである。
B2Rは、CTGを固定された安全予算の下で境界制約として再定義し、すべての実行可能な軌道のコスト分布を統一する。
実験の結果,B2Rは38項目中35項目の安全制約を満たすことがわかった。
論文 参考訳（メタデータ） (2025-09-30T03:38:20Z) - Core Safety Values for Provably Corrigible Agents [2.6451153531057985]
我々は,複数段階の部分的に観察された環境において,検証可能な保証を付与し,適応性のための最初の実装可能なフレームワークを紹介した。
私たちのフレームワークは、単一の報酬を5つの*構造的に分離された*ユーティリティヘッドに置き換えます。
敵がエージェントを修正できるオープンエンド設定では、任意のポストハックエージェントが調整性に反するかどうかを判断することは不可能である。
論文 参考訳（メタデータ） (2025-07-28T16:19:25Z) - Fast quantum transfer mediated by topological domain walls [0.0]
指数依存を欠くマルチドメインSSHチェーンとクロイツはしごにおける転送プロトコルを提案する。
また,Creutzはしごの局所化特性の活用方法についても検討する。
これにより、全接続可能な1Dネットワークが提供され、量子情報の目的に役立てることができる。
論文 参考訳（メタデータ） (2022-08-01T12:26:11Z) - Bi-Directional Generation for Unsupervised Domain Adaptation [61.73001005378002]
教師なしのドメイン適応は、確立されたソースドメイン情報に依存するラベルなしのターゲットドメインを促進する。
従来の手法では、潜在空間におけるドメインの不一致を強制的に低減することで、本質的なデータ構造が破壊される。
本稿では、2つの中間領域をブリッジソースとターゲットドメインに補間する一貫した分類器を用いた双方向生成ドメイン適応モデルを提案する。
論文 参考訳（メタデータ） (2020-02-12T09:45:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。