論文の概要: Satisfiability and Synthesis Modulo Oracles
- arxiv url: http://arxiv.org/abs/2107.13477v1
- Date: Wed, 28 Jul 2021 16:36:26 GMT
- ステータス: 処理完了
- システム内更新日: 2021-07-29 13:45:02.100513
- Title: Satisfiability and Synthesis Modulo Oracles
- Title(参考訳): 満足度と合成モジュロオラクル
- Authors: Elizabeth Polgreen, Andrew Reynolds and Sanjit A. Seshia
- Abstract要約: 多くの合成アルゴリズムは、満足度変調理論(SMT)に基づくホワイトボックスオラクルを用いて反例を提供する。
本稿では,分子誘導合成問題の一般クラスを解くための枠組みについて述べる。
また、満足度モジュロ理論やオラクルの問題を定式化し、この問題を解くアルゴリズムを提案する。
- 参考スコア(独自算出の注目度): 7.246701762489972
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In classic program synthesis algorithms, such as counterexample-guided
inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase
and an oracle (verification) phase. Many synthesis algorithms use a white-box
oracle based on satisfiability modulo theory (SMT) solvers to provide
counterexamples. But what if a white-box oracle is either not available or not
easy to work with? We present a framework for solving a general class of
oracle-guided synthesis problems which we term synthesis modulo oracles. In
this setting, oracles may be black boxes with a query-response interface
defined by the synthesis problem. As a necessary component of this framework,
we also formalize the problem of satisfiability modulo theories and oracles,
and present an algorithm for solving this problem. We implement a prototype
solver for satisfiability and synthesis modulo oracles and demonstrate that, by
using oracles that execute functions not easily modeled in SMT-constraints,
such as recursive functions or oracles that incorporate compilation and
execution of code, SMTO and SyMO are able to solve problems beyond the
abilities of standard SMT and synthesis solvers.
- Abstract(参考訳): 反例誘導インダクティブ合成(cegis)のような古典的なプログラム合成アルゴリズムでは、合成フェーズとオラクル(検証)フェーズの間で代替されるアルゴリズムである。
多くの合成アルゴリズムは、満足度変調理論(SMT)に基づくホワイトボックスオラクルを用いて反例を提供する。
しかし、もしホワイトボックスのオラクルが利用できないか、簡単に扱えないとしたら?
我々は,oracle が指導する合成問題の一般クラスを解くためのフレームワークを提示する。
この設定では、オーラクルは合成問題によって定義されたクエリ応答インタフェースを持つブラックボックスである。
また, この枠組みの必要成分として, 満足度モジュロ理論とオラクルの問題を定式化し, この問題を解くアルゴリズムを提案する。
本研究では,SMT制約でモデル化されていない関数,例えば再帰的関数や,コードのコンパイルと実行を組み込んだオーラクルなど,オーラクルを用いて,SMTOとSyMOが,標準的なSMTや合成ソルバの能力を超えた問題を解決できることを実証する。
関連論文リスト
- Guiding Enumerative Program Synthesis with Large Language Models [17.420727709895736]
本稿では,形式的合成ベンチマークを解くための大規模言語モデルの能力を評価する。
ワンショット合成が失敗すると,新しい列挙合成アルゴリズムを提案する。
形式的合成のためのスタンドアロンツールとしてGPT-3.5は,最先端の形式的合成アルゴリズムにより容易に性能が向上することがわかった。
論文 参考訳(メタデータ) (2024-03-06T19:13:53Z) - Efficient Reactive Synthesis Using Mode Decomposition [0.0]
そこで本研究では,モードに基づく新しい分解アルゴリズムを提案する。
我々のアルゴリズムへの入力は、元の仕様とモードの記述である。
サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
論文 参考訳(メタデータ) (2023-12-14T08:01:35Z) - ExeDec: Execution Decomposition for Compositional Generalization in
Neural Program Synthesis [59.356261137313275]
プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。
次に,ExeDecを提案する。ExeDecは,実行サブゴールを予測して問題を段階的に解決する,新しい分解ベースの戦略である。
論文 参考訳(メタデータ) (2023-07-26T01:07:52Z) - Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis [19.044613696320628]
構文誘導合成(syntax-guided synthesis)は、文法の形で構文テンプレートによって候補解の探索空間が制約されるパラダイムである。
本研究では,ルールの行列として構文テンプレートの空間をモデル化し,この行列を学習データを用いて効率的に探索する方法を実証する。
論文 参考訳(メタデータ) (2023-06-01T10:22:22Z) - ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle
Verifiers [60.6418431624873]
大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。
我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。
実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
論文 参考訳(メタデータ) (2023-05-24T00:10:15Z) - Optimal Algorithms for Stochastic Complementary Composite Minimization [55.26935605535377]
統計学と機械学習における正規化技術に触発され,補完的な複合化の最小化について検討した。
予測と高い確率で、新しい過剰なリスク境界を提供する。
我々のアルゴリズムはほぼ最適であり、このクラスの問題に対して、新しいより低い複雑性境界によって証明する。
論文 参考訳(メタデータ) (2022-11-03T12:40:24Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Resource Optimisation of Coherently Controlled Quantum Computations with
the PBS-calculus [55.2480439325792]
量子計算のコヒーレント制御は、いくつかの量子プロトコルやアルゴリズムを改善するために使用できる。
我々は、量子光学にインスパイアされたコヒーレント制御のためのグラフィカル言語PBS計算を洗練する。
論文 参考訳(メタデータ) (2022-02-10T18:59:52Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳(メタデータ) (2019-12-31T17:09:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。