論文の概要: 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) 探索の痕跡に基づくトップダウンコンパイラの提案を行う。
関連論文リスト
- A Neural Rewriting System to Solve Algorithmic Problems [51.485598133884615]
本稿では,特殊なモジュールで構成されたニューラルアーキテクチャとして,書き換えシステムを実装可能であることを示す。
シンボリック・フォーミュラの簡素化を必要とする3種類のアルゴリズムタスクに対して,本モデルの評価を行った。
論文 参考訳(メタデータ) (2024-02-27T10:57:07Z) - 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) - A Symbolic Language for Interpreting Decision Trees [7.143485463760098]
決定木を解釈するシンボリック言語であるExplainDTを提示する。
StratiFOILedは評価の表現性と複雑さをバランスさせる。
提案式としてStratiFOILedクエリを符号化するための最適化された実装を提供する。
論文 参考訳(メタデータ) (2023-10-18T00:07:38Z) - 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) - Explaining Patterns in Data with Language Models via Interpretable
Autoprompting [143.4162028260874]
本稿では,データを説明する自然言語文字列を生成するアルゴリズムである,解釈可能なオートプロンプト(iPrompt)を提案する。
iPromptは、基盤となるデータセット記述を正確に見つけることで、意味のある洞察を得ることができる。
fMRIデータセットを用いた実験は、iPromptが科学的発見に役立つ可能性を示している。
論文 参考訳(メタデータ) (2022-10-04T18:32:14Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。