論文の概要: Canonical Decision Diagrams Modulo Theories

• arxiv url: http://arxiv.org/abs/2404.16455v1
• Date: Thu, 25 Apr 2024 09:34:49 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-26 14:19:10.419821
• Title: Canonical Decision Diagrams Modulo Theories
• Title（参考訳）: 正準決定ダイアグラムによるモデュロ理論
• Authors: Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani,
• Abstract要約: 決定図は命題公式を表現する強力なツールである。 いくつかの形式(例えば OBDD や SDD など)は標準的であり、(原子リスト上の与えられた条件の下では)公式の同値類を単項的に表す。 DDをSMTレベルに活用する新しい手法を提案する。
• 参考スコア（独自算出の注目度）: 0.19285000127136376
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.
• Abstract（参考訳）: 決定図(Decision diagrams, DD)は、多くの領域、特に形式的検証や知識コンパイルにおいて、効果的に命題式を表現する強力なツールである。 DDのいくつかの形式(例: OBDDs, SDDs)は標準的であり、(原子リスト上の与えられた条件の下では)公式の同値類を一意的に表す。 命題論理の限られた表現性を考えると、DDをSMTレベルに活用する試みが文献で紹介されている。 残念なことに、これらの技術は依然としていくつかの制限に悩まされている: ほとんどの手順は理論固有のものであり、いくつかの生成理論DD(T-DDs)は T-valid 式や T-consistent 式を単項的に表さない。 また、これらの手順は実装が簡単ではなく、実際に実装できるものはほとんどありません。 本稿では,全SMT ソルバと DD パッケージをブラックボックスとして実装することは極めて容易であり,すべての DD の形式や,AllSMT ソルバがサポートする理論,あるいはその組み合わせに対して有効であり,提案 DD が正則であれば理論-正準 T-DD を生成するという,SMT レベルに DD を活用するための新しい手法を提案する。 我々は,OBDDとSDDパッケージとMathSAT SMTソルバ上に,T-OBDDとT-SDDのプロトタイプツールを実装した。 いくつかの予備的な経験的評価は、アプローチの有効性を支持する。

関連論文リスト

• The role of slicing in test-driven development [39.01665062857323]
  テスト駆動開発(TDD)は広く使われているアジャイルプラクティスです。 TDDの理論的枠組みとして,次のような特徴を持つフレームワークを提案する。 業界で実施されたコントロールされた実験を使用して、TDD、契約、スライス間の接続をチェックしました。
  論文  参考訳（メタデータ） (2024-07-18T08:10:38Z)
• Partial-differential-algebraic equations of nonlinear dynamics by Physics-Informed Neural-Network: (I) Operator splitting and framework assessment [51.3422222472898]
  偏微分代数方程式の解法として, 新規な物理情報ネットワーク(PINN)の構築法が提案されている。 これらの新しい手法には PDE 形式があり、これは未知の従属変数が少ない低レベル形式からより従属変数を持つ高レベル形式へと進化している。
  論文  参考訳（メタデータ） (2024-07-13T22:48:17Z)
• A Formal Analysis of Iterated TDD [0.0]
  テスト駆動開発(TDD)と呼ばれるソフトウェア方法論を正式に分析します。 反復されたTDDが、反復されたコードチャーンの観点から安定しながら、'証明可能な正しいコード'を確実に生成するコンテキストを見つけます。 我々は、以前の研究で見いだされた'有効'の反復TDDの発見は、この文脈を欠いたことによるものであり、'有効'の反復TDDの発見は、誤ってコンテキストに落ちたり、単にプラセボに落ちてしまうことによるものである、と論じている。
  論文  参考訳（メタデータ） (2024-07-04T08:07:35Z)
• Disperse-Then-Merge: Pushing the Limits of Instruction Tuning via Alignment Tax Reduction [75.25114727856861]
  大規模言語モデル(LLM)は、スーパービジョンされた微調整プロセスの後半で劣化する傾向にある。 この問題に対処するための単純な分散結合フレームワークを導入する。 我々のフレームワークは、一連の標準知識と推論ベンチマークに基づいて、データキュレーションや正規化の訓練など、様々な高度な手法より優れています。
  論文  参考訳（メタデータ） (2024-05-22T08:18:19Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• MDD-UNet: Domain Adaptation for Medical Image Segmentation with Theoretical Guarantees, a Proof of Concept [3.376269351435396]
  理論的保証付きU-Netのための教師なしドメイン適応フレームワークを提案する。 MDD-UNetは、ターゲットドメインのラベルに関する知識のない、ドメイン不変の機能を学ぶことができる。 この研究は、モダンな拡張なしに標準形式でのU-Netの改善を示すことによって、概念実証として機能する。
  論文  参考訳（メタデータ） (2023-12-19T15:30:10Z)
• An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
  Algebraic Data Types (ADT) は関数型プログラミング言語で古典的に見られる構造である。 我々は,基本的に異なるアプローチ,エフェーガーアプローチを採るSMTソルバを提案する。
  論文  参考訳（メタデータ） (2023-10-18T18:14:18Z)
• AdaNPC: Exploring Non-Parametric Classifier for Test-Time Adaptation [64.9230895853942]
  ドメインの一般化は、ターゲットのドメイン情報を活用することなく、任意に困難にすることができる。 この問題に対処するためにテスト時適応(TTA)手法が提案されている。 本研究では,テスト時間適応(AdaNPC)を行うためにNon-Parametricを採用する。
  論文  参考訳（メタデータ） (2023-04-25T04:23:13Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Belief Revision in Sentential Decision Diagrams [126.94029917018733]
  本研究では,Dalリビジョンの構文的特徴化に基づくSDDの一般的なリビジョンアルゴリズムを開発する。 ランダムに生成した知識ベースを用いた予備実験は、SDDフォーマリズム内で直接リビジョンを行う利点を示している。
  論文  参考訳（メタデータ） (2022-01-20T11:01:41Z)
• Variable Shift SDD: A More Succinct Sentential Decision Diagram [10.91026094237478]
  Sentential Decision Diagram (SDD) はブール関数の抽出可能な表現である。 可変シフトSDD(VS-SDD)という,より簡潔なSDD変種を提案する。 我々は,VS-SDDがSDDよりも大きくなることはなく,VS-SDDのサイズがSDDよりも指数関数的に小さいケースがあることを示した。
  論文  参考訳（メタデータ） (2020-04-06T09:18:19Z)

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

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