論文の概要: KBX: Verified Model Synchronization via Formal Bidirectional Transformation
- arxiv url: http://arxiv.org/abs/2404.18771v2
- Date: Wed, 1 May 2024 15:08:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-05-02 10:59:25.983494
- Title: KBX: Verified Model Synchronization via Formal Bidirectional Transformation
- Title（参考訳）: KBX:形式的双方向変換による検証モデル同期
- Authors: Jianhong Zhao, Yongwang Zhao, Peisen Yao, Fanlang Zeng, Bohua Zhan, Kui Ren,
- Abstract要約: 双方向変換(BX)は、これらのモデルを自動的に同期するアプローチである。
既存のBXフレームワークには、これらのモデルの一貫性を厳格に強制するための正式な検証がない。
本稿では,検証モデル同期のための形式変換フレームワークKBXを紹介する。
- 参考スコア（独自算出の注目度）: 10.119816058971539
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models' consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the $\mathbb{K}$ framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness $\mathbb{K}$ to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 82.8\% reduction in BX development effort compared to manual specification writing in $\mathbb{K}$.
- Abstract（参考訳）: 複雑な安全クリティカルなシステムは包括的記述のために複数のモデルを必要とするため、エラーが発生しやすい開発と厳密な検証が生じる。
双方向変換(BX)は、これらのモデルを自動的に同期するアプローチである。
しかし、既存のBXフレームワークはこれらのモデルの一貫性を厳格に強制する正式な検証を欠いている。
本稿では,検証モデル同期のための形式的双方向変換フレームワークKBXを紹介する。
まず、マッチング論理に基づくBXモデルを示し、$\mathbb{K}$フレームワーク内でBX定義を構築するための論理的基盤を提供する。
第2に,一方向定義から形式的BX定義を合成するアルゴリズムを提案する。
その後、$\mathbb{K}$を使用して、一貫性の維持と検証のために合成された定義から形式的シンクロナイザを生成する。
KBXの有効性を評価するため,既存のBXフレームワークとの比較分析を行った。
さらに,UML と HCSP 間の BX 構築における KBX の応用を実世界のシナリオに適用し,$\mathbb{K}$ のマニュアル仕様記述に比べて BX 開発作業が82.8 % 削減されたことを示す。
関連論文リスト
- RaBiT: Residual-Aware Binarization Training for Accurate and Efficient LLMs [5.782015253162346]
残留バイナライゼーションは、バイナリ層を積み重ねることで、マットルフリーな推論を可能にする。
本稿では,残差階層をアルゴリズム的に強制することでコダプタ化を解決する新しい量子化フレームワークであるRaBiTを提案する。
RaBiTは最先端のパフォーマンスを実現し、ハードウェア集約型ベクトル量子化(VQ)の手法と競合する。
論文 参考訳（メタデータ） (2026-02-05T06:41:11Z) - UniX: Unifying Autoregression and Diffusion for Chest X-Ray Understanding and Generation [98.93314262366681]
胸部X線理解・生成のための次世代統合医療基盤モデルUniXについて述べる。
UniXは2つのタスクを、理解のための自己回帰分岐と高忠実度生成のための拡散分岐に分離する。
2つの代表的なベンチマークでは、Unixは46.1%の性能向上と24.2%の世代品質向上を実現している。
論文 参考訳（メタデータ） (2026-01-16T18:59:58Z) - Matrix Factorization Framework for Community Detection under the Degree-Corrected Block Model [48.989531198582704]
我々は,DCBM推論を制約付き非負行列分解問題として再定義できることを示した。
我々のアプローチは、任意の特定のネットワーク構造に適応し、DCBMで表現可能な任意の構造を持つグラフに適用する。
合成および実ベンチマークネットワークの実験により,本手法はDCBMの推測に匹敵するコミュニティを検出する。
論文 参考訳（メタデータ） (2026-01-09T19:16:29Z) - A Bayesian Generative Modeling Approach for Arbitrary Conditional Inference [4.4876925770439415]
本稿では,任意の条件推論のためのベイズ生成モデル (BGM) を提案する。
BGMは、モデルパラメータと潜伏変数が収束するまで更新される反復ベイズ更新アルゴリズムを通してXの生成モデルを学ぶ。
経験的に、BGMはよく校正された予測間隔で優れた予測性能を達成する。
論文 参考訳（メタデータ） (2026-01-08T20:14:30Z) - SoliReward: Mitigating Susceptibility to Reward Hacking and Annotation Noise in Video Generation Reward Models [53.19726629537694]
ビデオ生成モデルと人間の好みのトレーニング後のアライメントは、重要な目標である。
現在のデータ収集パラダイムは、プロンプト内のペアワイズアノテーションに依存しており、ノイズのラベル付けに悩まされている。
ビデオRMトレーニングのための体系的フレームワークであるSoliRewardを提案する。
論文 参考訳（メタデータ） (2025-12-17T14:28:23Z) - QiMeng-CRUX: Narrowing the Gap between Natural Language and Verilog via Core Refined Understanding eXpression [48.84841760215598]
大規模言語モデル(LLM)はハードウェア記述言語(HDL)生成において有望な能力を示している。
既存のアプローチは、しばしば曖昧で冗長で構造化されていない自由形式の自然言語記述に依存している。
我々は、ハードウェアコード生成を、オープンな自然言語空間からドメイン固有の高度に制約されたターゲット空間への複雑な変換として扱う。
構造化された中間空間であるCore Refined Understanding eXpression (CRUX)を導入し、ユーザの意図の本質的な意味を捉えながら、正確なVerilogコード生成のための式を整理する。
論文 参考訳（メタデータ） (2025-11-25T09:17:32Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - Modular Delta Merging with Orthogonal Constraints: A Scalable Framework for Continual and Reversible Model Composition [0.0]
既存のモデルマージと継続的学習へのアプローチは、しばしばタスクの干渉、破滅的な忘れ込み、あるいは可逆性の欠如に悩まされる。
本稿では, 拡張性, 干渉フリー, 微調整モデルの構成が可能な新しいフレームワークである Orthogonal Constraints (MDM-OC) を用いた Modular Delta Merging を提案する。
論文 参考訳（メタデータ） (2025-07-28T17:08:49Z) - Assemble Your Crew: Automatic Multi-agent Communication Topology Design via Autoregressive Graph Generation [72.44384066166147]
大規模言語モデル(LLM)に基づくマルチエージェントシステム(MAS)は、多様な領域にわたる複雑な問題を扱うための強力なソリューションとして登場した。
既存のアプローチは、事前に定義されたエージェントセットとハードコードされた相互作用構造を持つテンプレートグラフ修正パラダイムに依存しているため、基本的に制限されている。
協調グラフをスクラッチから構築することで、このパラダイムを運用する新しい自己回帰モデルであるARG-Designerを提案する。
論文 参考訳（メタデータ） (2025-07-24T09:17:41Z) - Spectra-to-Structure and Structure-to-Spectra Inference Across the Periodic Table [60.78615287040791]
XAStructは結晶構造からXASスペクトルを予測し、XAS入力から局所構造記述子を推測できる学習フレームワークである。
XAStructは、周期表全体にわたって70以上の要素にまたがる大規模なデータセットでトレーニングされている。
論文 参考訳（メタデータ） (2025-06-13T15:58:05Z) - A SCADE Model Verification Method Based on B-Model Transformation [0.8437187555622164]
本研究では,B法に基づく形式的検証フレームワークを提案する。
SCADEで直接モデリングするのが難しい抽象仕様をうまく検証します。
本研究は,アビオニクス,鉄道輸送,その他の領域における組込み制御システムに対するクロスモデル検証パラダイムを提供する。
論文 参考訳（メタデータ） (2025-05-02T03:05:09Z) - Bidirectionalization For The Common People [0.0]
Bifronsは、ドメイン固有のプログラミング言語を置き換えるBXレンズのライブラリである。
提案手法は、双方向変換の実装作業を単純化する。
単純なレンズテストフレームワークを提供することで、合理的に正確性を保証する。
論文 参考訳（メタデータ） (2025-02-26T09:05:13Z) - COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。
我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。
当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
論文 参考訳（メタデータ） (2024-10-12T23:56:19Z) - Backward Compatibility in Attributive Explanation and Enhanced Model Training Method [0.0]
本稿では,事前および更新後のモデル間の特徴属性説明の後方互換性を評価する指標であるBCXを紹介する。
BCXは、事前および更新後のモデルの説明の間の平均合意を計算するために、実践的な合意メトリクスを利用する。
モデルの説明の中でL2距離を利用して,すべての合意基準を改善するBCXRの普遍的変種を提案する。
論文 参考訳（メタデータ） (2024-08-05T08:14:32Z) - Binarized Diffusion Model for Image Super-Resolution [61.963833405167875]
超圧縮アルゴリズムであるバイナリ化は、高度な拡散モデル(DM)を効果的に加速する可能性を提供する
既存の二項化法では性能が著しく低下する。
画像SRのための新しいバイナライズ拡散モデルBI-DiffSRを提案する。
論文 参考訳（メタデータ） (2024-06-09T10:30:25Z) - Recurrent Complex-Weighted Autoencoders for Unsupervised Object Discovery [62.43562856605473]
複雑な重み付き再帰的アーキテクチャの計算上の優位性について論じる。
本稿では,反復的制約満足度を実現する完全畳み込みオートエンコーダSynCxを提案する。
論文 参考訳（メタデータ） (2024-05-27T15:47:03Z) - A Novel Decision Ensemble Framework: Customized Attention-BiLSTM and
XGBoost for Speculative Stock Price Forecasting [2.011511123338945]
本稿では、投機的株式Bitcoin-USD(BTC-USD)の日替価格を予測するための新しいフレームワーク、CAB-XDEを提案する。
CAB-XDEフレームワークは、カスタマイズされた双方向長短期メモリ(BiLSTM)とアテンション機構とXGBoostアルゴリズムを統合している。
提案されたCAB-XDEフレームワークは、Yahoo Financeから供給された不安定なBitcoin市場で実証的に検証されている。
論文 参考訳（メタデータ） (2024-01-05T17:13:30Z) - Bidirectional Trained Tree-Structured Decoder for Handwritten
Mathematical Expression Recognition [51.66383337087724]
Handwriting Mathematical Expression Recognition (HMER) タスクは、OCRの分野における重要な分岐である。
近年の研究では、双方向コンテキスト情報の導入により、HMERモデルの性能が大幅に向上することが示されている。
本稿では,MF-SLT と双方向非同期トレーニング (BAT) 構造を提案する。
論文 参考訳（メタデータ） (2023-12-31T09:24:21Z) - OCTAL: Graph Representation Learning for LTL Model Checking [5.22145960878624]
GRLベースの新しいフレームワークモデルは、グラフ構造化システムと仕様の表現を学習するために設計されている。
実験により、モデルが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大で11倍になることが示された。
論文 参考訳（メタデータ） (2023-08-19T15:11:18Z) - The Bayesian Context Trees State Space Model for time series modelling
and forecasting [8.37609145576126]
実数値時系列に対してリッチな混合モデルを開発するための階層的ベイズフレームワークが導入された。
最上位では、有意義な離散状態が、最新のサンプルの適切な定量値として特定される。
下位レベルでは、実数値時系列(ベースモデル)の異なる任意のモデルが各状態と関連付けられている。
論文 参考訳（メタデータ） (2023-08-02T02:40:42Z) - BB-GCN: A Bi-modal Bridged Graph Convolutional Network for Multi-label
Chest X-Ray Recognition [7.110986667249555]
マルチラベル胸部X線(英語版)(CXR)認識は、異なる病理の複数のラベルを同時に診断し識別する。
従来の手法は、ローカルラベル情報をモデル化するために、状態変数の符号化とアテンションメカニズムに頼っていた。
Bi-modal Bridged Graph Convolutional Network (BB-GCN) モデルを提案する。
論文 参考訳（メタデータ） (2023-02-22T01:03:53Z) - Error-based Knockoffs Inference for Controlled Feature Selection [49.99321384855201]
本手法では, ノックオフ特徴量, エラーベース特徴重要度統計量, ステップダウン手順を一体化して, エラーベースのノックオフ推定手法を提案する。
提案手法では回帰モデルを指定する必要はなく,理論的保証で特徴選択を処理できる。
論文 参考訳（メタデータ） (2022-03-09T01:55:59Z) - On Exploiting Hitting Sets for Model Reconciliation [53.81101846598925]
ヒューマン・アウェア・プランニングにおいて、プランニング・エージェントは、その計画がなぜ最適なのかを人間に説明する必要があるかもしれない。
この手法はモデル和解と呼ばれ、エージェントはモデルと人間のモデルの違いを調和させようとする。
我々は,計画の領域を超えて拡張されたモデル和解のための論理ベースのフレームワークを提案する。
論文 参考訳（メタデータ） (2020-12-16T21:25:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。