論文の概要: Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams

• arxiv url: http://arxiv.org/abs/2604.27008v1
• Date: Wed, 29 Apr 2026 09:14:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-01 16:31:53.717545
• Title: Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams
• Title（参考訳）: 2値決定図を用いたACAS-Xuルックアップテーブルの圧縮
• Authors: Martin Boniol, Julien Brunel, Jean-Baptiste Chaudron, Christophe Garion, Xavier Thirioux,
• Abstract要約: 本稿では、ACAS-Xu LUTの正確なセマンティクスを保持する2値決定図(BDD)に基づくシンボリック圧縮手法を提案する。 結果の表現は標準的で決定論的であり、元のテーブルと完全に等価である。 提案したBDDベースの表現はメモリ使用量を大幅に削減し,予測可能な低レイテンシ実行を実現し,組込みプラットフォームにデプロイ可能であることを実証する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Airborne Collision Avoidance System Xu (ACAS-Xu) relies on large certified Look-Up Tables (LUTs) that encode the exact decision logic used in operation. Neural-network-based approximations have been proposed to reduce memory requirements, but they inherently introduce approximation errors and complicate formal verification. This paper presents a symbolic compression approach based on Binary Decision Diagrams (BDDs) that preserves the exact semantics of the ACAS-Xu LUTs. The resulting representation is canonical, deterministic, and fully equivalent to the original tables, enabling sound and exact reasoning over the complete decision logic. By expressing both the system behavior and domain-specific operational properties within a common Boolean framework, verification reduces to efficient BDD operations and emptiness checks, with precise counterexamples generated when properties are violated. We demonstrate that the proposed BDD-based representation significantly reduces memory usage, achieves predictable and low-latency execution, and can be deployed on embedded platforms. These results highlight BDDs as a compelling alternative for exact, verifiable, and embedded deployment of ACAS-Xu decision logic.
• Abstract（参考訳）: Airborne Collision Avoidance System Xu (ACAS-Xu) は、Look-Up Tables (LUT) と呼ばれる、運用で使用する正確な決定ロジックをエンコードする大型の認証済みのLook-Up Tables (LUT) に依存している。 ニューラルネットワークに基づく近似は、メモリ要求を減らすために提案されているが、本質的に近似誤差を導入し、形式的検証を複雑化する。 本稿では、ACAS-Xu LUTの正確なセマンティクスを保持する2値決定図(BDD)に基づくシンボリック圧縮手法を提案する。 結果として得られる表現は正準的で決定論的であり、元の表と完全に等価であり、完全な決定論理に対する健全かつ正確な推論を可能にする。 共通のBooleanフレームワーク内でのシステム動作とドメイン固有の運用特性の両方を表現することで、検証はBDDの効率的な操作と空虚性チェックに還元され、プロパティに違反した場合に正確な反例が生成される。 提案したBDDベースの表現はメモリ使用量を大幅に削減し,予測可能な低レイテンシ実行を実現し,組込みプラットフォームにデプロイ可能であることを実証する。 これらの結果は、正確な、検証可能な、ACAS-Xu決定ロジックの組み込み配置のための魅力的な代替手段として、BDDを強調します。

関連論文リスト

• Calibrated Speculative Decoding: Frequency-Guided Candidate Selection for Efficient Inference [27.59556627479635]
  Calibrated Speculative Decodingは、標準検証によって破棄された有効なトークンを復元する。 Online Correction Memory は歴史的拒絶を集約し、繰り返し発散パターンを救助候補者として提案する。 Semantic Consistency Gatingは、正確なトークンマッチングの代わりに確率比を用いて候補許容性を検証する。
  論文  参考訳（メタデータ） (2026-04-15T09:01:54Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。 本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。 我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
  論文  参考訳（メタデータ） (2026-01-30T07:01:25Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• Randomized Smoothing Meets Vision-Language Models [6.224335082856828]
  ランダムスムーシング(RS)は、機械学習モデルの正確性を保証するために使用される。 生成モデルではRSが引き続き有効であることを示す。 我々は,検体数に対する検体半径と精度を解析的に関連づけたスケーリング法を導出した。 これらの進歩は、最先端のVLMに対して、明確に定義され、計算的に実現可能なロバストネス認証を実現する。
  論文  参考訳（メタデータ） (2025-09-19T15:33:22Z)
• Pseudo-Boolean Proof Logging for Optimal Classical Planning [9.688823478031852]
  擬似ブール制約に基づく下界証明書を生成するための一般的なフレームワークについて述べる。 A*$アルゴリズムを改良して,過度なオーバーヘッドで最適性の証明を生成する方法を示す。
  論文  参考訳（メタデータ） (2025-04-25T15:54:09Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Mitigating Algorithmic Bias with Limited Annotations [65.060639928772]
  機密属性が公開されていない場合、バイアスを軽減するために、トレーニングデータの小さな部分を手動でアノテートする必要がある。 本稿では,アルゴリズムバイアスの影響を最大限に排除するために,限定アノテーションを誘導する対話型フレームワークであるアクティブペナライゼーション・オブ・差別(APOD)を提案する。 APODは完全なアノテートバイアス緩和と同等のパフォーマンスを示しており、機密情報が制限された場合、APODが現実世界のアプリケーションに利益をもたらすことを実証している。
  論文  参考訳（メタデータ） (2022-07-20T16:31:19Z)
• Optimizing Binary Decision Diagrams with MaxSAT for classification [3.2894524838755608]
  説明可能な人工知能への関心の高まりは、解釈可能な機械学習(ML)モデルの必要性を動機付けている。 近年、従来の手法の弱点を克服するために、そのようなモデルを計算するためのいくつかの正確な方法が提案されている。 本稿ではまず,最適なバイナリ決定図(BDD)を学習するためのSATモデルを提案する。 次に、符号化をMaxSATモデルに上げ、限られた深さで最適なBDDを学習します。 最後に、MaxSATモデルを介して見つけたBDDの互換性のあるサブツリーをマージする手法を導入することにより、フラグメンテーションの問題に取り組む。
  論文  参考訳（メタデータ） (2022-03-21T23:17:37Z)
• Probabilistic Case-based Reasoning for Open-World Knowledge Graph Completion [59.549664231655726]
  ケースベース推論(CBR)システムは,与えられた問題に類似した事例を検索することで,新たな問題を解決する。 本稿では,知識ベース(KB)の推論において,そのようなシステムが実現可能であることを示す。 提案手法は,KB内の類似エンティティからの推論パスを収集することにより,エンティティの属性を予測する。
  論文  参考訳（メタデータ） (2020-10-07T17:48:12Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。