論文の概要: Top-Down Knowledge Compilation for Counting Modulo Theories

• arxiv url: http://arxiv.org/abs/2306.04541v2
• Date: Thu, 30 Nov 2023 16:21:18 GMT
• ステータス: 処理完了
• システム内更新日: 2023-12-01 20:20:34.670999
• Title: Top-Down Knowledge Compilation for Counting Modulo Theories
• Title（参考訳）: モジュラー理論を数えるためのトップダウン知識コンパイル
• Authors: Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb, Paolo Morettin
• Abstract要約: 入力式が決定論的分解可能な否定正規形(d-DNNF)である場合、仮説モデルカウントは効率的に解ける。 トップダウン知識コンパイルは#SAT問題を解決する最先端技術である。 我々は,DPLL(T)探索の痕跡に基づくトップダウンコンパイラを提唱する。
• 参考スコア（独自算出の注目度）: 11.086759883832505
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows inference tasks, such as counting, to be performed efficiently, is called knowledge compilation. Top-down knowledge compilation is a state-of-the-art technique for solving #SAT problems that leverages the traces of exhaustive DPLL search to obtain d-DNNF representations. While knowledge compilation is well studied for propositional approaches, knowledge compilation for the (quantifier free) counting modulo theory setting (#SMT) has been studied to a much lesser degree. In this paper, we discuss compilation strategies for #SMT. We specifically advocate for a top-down compiler based on the traces of exhaustive DPLL(T) search.
• Abstract（参考訳）: 入力式が決定論的分解可能な否定正規形(d-DNNF)である場合に、仮説モデルカウント(#SAT)を効率的に解くことができる。 任意の式を計算などの推論タスクを効率的に実行できる表現に変換することは知識コンパイル(英語版)と呼ばれる。 トップダウン知識コンパイル(Top-down knowledge compilation)は、DPLL探索のトレースを利用してd-DNNF表現を得る#SAT問題の解法である。 知識コンパイルは命題的アプローチでよく研究されているが、(量子化子を含まない)数乗法理論設定(#SMT)のための知識コンパイルはより少ない程度に研究されている。 本稿では,#SMTのコンパイル戦略について議論する。 具体的には, dpll(t) 探索の痕跡に基づくトップダウンコンパイラの提案を行う。

関連論文リスト

• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  形式言語理論は、特に認識者に関するものである。 代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。 ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
  論文  参考訳（メタデータ） (2024-11-11T16:33:25Z)
• CASET: Complexity Analysis using Simple Execution Traces for CS* submissions [0.0]
  CS1 や CS2 コースで学生の提出を自動アップグレードする最も一般的な方法は、事前に定義されたテストスイートに対して実行し、結果と参照結果を比較することである。 この手法は、解の正しさが、結果を得るために使われるアルゴリズムのような単純な出力を超えると利用できない。 動的トレースと教師なし機械学習を用いてアルゴリズムの時間的複雑さを解析する新しいツールCASETを提案する。
  論文  参考訳（メタデータ） (2024-10-20T15:29:50Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• IASCAR: Incremental Answer Set Counting by Anytime Refinement [18.761758874408557]
  本稿では,CNFの知識コンパイルを前提として,サポート対象モデルを符号化する手法を提案する。 予備的な実証分析では,有望な結果を示す。
  論文  参考訳（メタデータ） (2023-11-13T10:53:48Z)
• An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
  Algebraic Data Types (ADT) は関数型プログラミング言語で古典的に見られる構造である。 我々は,基本的に異なるアプローチ,エフェーガーアプローチを採るSMTソルバを提案する。
  論文  参考訳（メタデータ） (2023-10-18T18:14:18Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。 ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。 CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
  論文  参考訳（メタデータ） (2023-06-04T17:02:59Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs [2.28438857884398]
  我々は、型チェックがプログラムの仮説空間の大部分を掃引することができることを示した。 我々は合成節とプログラム全体の多形型を推測することができる。
  論文  参考訳（メタデータ） (2021-02-18T13:40:16Z)

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

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