論文の概要: An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes

• arxiv url: http://arxiv.org/abs/2310.12234v1
• Date: Wed, 18 Oct 2023 18:14:18 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-20 18:16:32.490369
• Title: An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
• Title（参考訳）: 代数データ型に対するEager Satisfiability Modulo理論
• Authors: Amar Shah, Federico Mora, Sanjit A. Seshia
• Abstract要約: Algebraic Data Types (ADT) は関数型プログラミング言語で古典的に見られる構造である。 我々は,基本的に異なるアプローチ,エフェーガーアプローチを採るSMTソルバを提案する。
• 参考スコア（独自算出の注目度）: 4.393684402895834
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent years, interest in ADTs has increased. For example, popular programming languages, like Python, have added support for ADTs. Automated reasoning about ADTs can be done using satisfiability modulo theories (SMT) solving, an extension of the Boolean satisfiability problem with constraints over first-order structures. Unfortunately, SMT solvers that support ADTs do not scale as state-of-the-art approaches all use variations of the same \emph{lazy} approach. In this paper, we present an SMT solver that takes a fundamentally different approach, an \emph{eager} approach. Specifically, our solver reduces ADT queries to a simpler logical theory, uninterpreted functions (UF), and then uses an existing solver on the reduced query. We prove the soundness and completeness of our approach and demonstrate that it outperforms the state-of-theart on existing benchmarks, as well as a new, more challenging benchmark set from the planning domain.
• Abstract（参考訳）: Algebraic Data Types (ADT) は、列挙型、リスト、ツリーなどのデータ構造をキャプチャする関数型プログラミング言語で古典的に見られる構造である。 近年,adtsへの関心が高まっている。 例えば、Pythonのような人気のあるプログラミング言語は、ADTのサポートを追加した。 ADTに関する自動推論は、一階構造上の制約を伴うブール充足可能性問題の拡張であるSMT(Satisfiability modulo theory)解決を用いて行うことができる。 残念なことに、 ADT をサポートする SMT ソルバは、最先端のアプローチでは、すべて同じ \emph{lazy} アプローチのバリエーションを使用するため、スケールしない。 本稿では, 基本的に異なるアプローチ, \emph{eager} アプローチをとるSMTソルバを提案する。 具体的には、ADTクエリを単純な論理理論、非解釈関数(UF)に減らし、その減らしたクエリに既存のソルバを使用する。 われわれのアプローチの健全性と完全性を証明し、既存のベンチマークで最先端のベンチマークを上回り、計画領域からの新しいより挑戦的なベンチマークを上回ります。

関連論文リスト

• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-Thought (CoT) は,大規模言語モデル (LLM) から推論能力を引き出すデファクト手法である。 私たちは、CoTが主に数学や論理学を含むタスクに強いパフォーマンス上の利点をもたらし、他のタスクよりもはるかに少ない利益をもたらすことを示しています。
  論文  参考訳（メタデータ） (2024-09-18T17:55:00Z)
• Automata-based constraints for language model decoding [9.137697105669142]
  言語モデル(LM)は、いくつかの形式言語で文字列を生成することがしばしば期待されている。 チューニングにはかなりのリソースが必要で、一般的でない、あるいはタスク固有のフォーマットでは実用的ではない。 我々はこれらの問題をオートマトン理論を適用して解決する。 我々のシステムは、7000倍高速に制約をコンパイルし、確実に正確であり、モジュール方式で拡張することができる。
  論文  参考訳（メタデータ） (2024-07-11T00:25:01Z)
• Top-Down Knowledge Compilation for Counting Modulo Theories [11.086759883832505]
  入力式が決定論的分解可能な否定正規形(d-DNNF)である場合、仮説モデルカウントは効率的に解ける。 トップダウン知識コンパイルは#SAT問題を解決する最先端技術である。 我々は,DPLL(T)探索の痕跡に基づくトップダウンコンパイラを提唱する。
  論文  参考訳（メタデータ） (2023-06-07T15:46:28Z)
• 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)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Text Modular Networks: Learning to Decompose Tasks in the Language of Existing Models [61.480085460269514]
  本稿では,既存のモデルで解けるより単純なモデルに分解することで,複雑なタスクを解くための解釈可能なシステムを構築するためのフレームワークを提案する。 我々はこのフレームワークを用いて、ニューラルネットワークのファクトイド単一スパンQAモデルとシンボリック電卓で答えられるサブクエストに分解することで、マルチホップ推論問題に答えられるシステムであるModularQAを構築する。
  論文  参考訳（メタデータ） (2020-09-01T23:45:42Z)

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

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