Satisfiability and Synthesis Modulo Oracles

• URL: http://arxiv.org/abs/2107.13477v1
• Date: Wed, 28 Jul 2021 16:36:26 GMT
• Title: Satisfiability and Synthesis Modulo Oracles
• Authors: Elizabeth Polgreen, Andrew Reynolds and Sanjit A. Seshia
• Abstract summary: Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. We also formalize the problem of satisfiability modulo theories and oracles, and present an algorithm for solving this problem.
• Score: 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.

Related papers

• OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling [62.19438812624467]
  Large language models (LLMs) have exhibited their problem-solving abilities in mathematical reasoning. We propose OptiBench, a benchmark for End-to-end optimization problem-solving with human-readable inputs and outputs.
  arXiv  Detail & Related papers  (2024-07-13T13:27:57Z)
• Quantum State Synthesis: Relation with Decision Complexity Classes and Impossibility of Synthesis Error Reduction [0.3376269351435395]
  This work investigates the relationships between quantum state synthesis complexity classes and traditional decision complexity classes. We especially investigate the role of the synthesis error parameter, which characterizes the quality of the synthesis in quantum state synthesis complexity classes.
  arXiv  Detail & Related papers  (2024-07-03T08:26:38Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  We study the synthesis of six datasets, covering topic classification, sentiment analysis, tone detection, and humor. We find that SynthesizRR greatly improves lexical and semantic diversity, similarity to human-written text, and distillation performance.
  arXiv  Detail & Related papers  (2024-05-16T12:22:41Z)
• Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
  In this paper, we evaluate the abilities of Large Language Models to solve formal synthesis benchmarks. When one-shot synthesis fails, we propose a novel enumerative synthesis algorithm. We find that GPT-3.5 as a stand-alone tool for formal synthesis is easily outperformed by state-of-the-art formal synthesis algorithms.
  arXiv  Detail & Related papers  (2024-03-06T19:13:53Z)
• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  We propose a novel decomposition algorithm based on modes. The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable the full specification is realizable.
  arXiv  Detail & Related papers  (2023-12-14T08:01:35Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  Large language models (LLMs) excel at implementing code from functionality descriptions but struggle with algorithmic problems. We propose ALGO, a framework that synthesizes Algorithmic programs with LLM-Generated Oracles to guide the generation and verify their correctness. Experiments show that when equipped with ALGO, we achieve an 8x better one-submission pass rate over the Codex model and a 2.6x better one-submission pass rate over CodeT.
  arXiv  Detail & Related papers  (2023-05-24T00:10:15Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  We use a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize synthesis.
  arXiv  Detail & Related papers  (2019-12-31T17:09:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.