Automated Synthesis: Functional, Reactive and Beyond

The innovations in reactive synthesis from Linear Temporal Logics over finte traces (LTLf) will be amplified by the ability to verify the correctness of the strategies generated by LTLf synthesis tools. This motivates our work on LTLf model checking. LTLf model checking, however, is not straightforward. The strategies generated by LTLf synthesis may be represented using terminating transducers or non-terminating transducers where executions are of finite-but-unbounded length or infinite length, respectively. For synthesis, there is no evidence that one type of transducer is better than the other since they both demonstrate the same complexity and similar algorithms.

In this work, we show that for model checking, the two types of transducers are fundamentally different. Our central result is that LTLf model checking of non-terminating transducers is exponentially harder than that of terminating transducers. We show that the problems are EXPSPACE-complete and PSPACE-complete, respectively. Hence, considering the feasibility of verification, LTLf synthesis tools should synthesize terminating transducers. This is, to the best of our knowledge, the first evidence to use one transducer over the other in LTLf synthesis.

We propose a novel application of syntax-guided synthesis to find symbolic representations of a model’s decision-making process, designed for easy comprehension and validation by humans. Our approach takes input-output samples from complex machine learning models, such as deep neural networks, and automatically derives interpretable mimic programs. A mimic program precisely imitates the behavior of an opaque model over the provided data. We discuss various types of grammars that are well-suited for computing mimic programs for tabular and image input data.

Our experiments demonstrate the potential of the proposed method: we successfully synthesized mimic programs for neural networks trained on the MNIST and the Pima Indians diabetes data sets. All experiments were performed using the SMT-based cvc5 synthesis tool.

Programming by example (PBE) allows users with little to no formal computation experience to carry out tasks by providing simple demonstrations (e.g. input/output-based examples). In practice, PBE has found considerable industrial uptake, particularly in end-user environments like spreadsheet software (e.g. Microsoft Excel, Google Sheets). In this talk, I’ll present a recent project on learning data-dependent formatting rules in Excel from examples. We’ll then discuss how PBE in this domain can be extended to also incorporate multimodal specifications, by supporting use of natural language. Using this as a segue into combining symbolic and neural methods, I’ll discuss recent work from the field that uses LLMs and may provide ideas for nice collaborations between formal reasoning and popular LLM-based approaches.

Given a Boolean relational specification $\phi (X,Y)$ over input variables X and output variables Y, Boolean functional synthesis concerns finding Skolem functions F(X) for Y such that $\exists Y\phi (X,Y)$ is semantically equivalent to $\phi (X,F(X))$. In this talk, we introduce the problem, survey some earlier results and then take a deeper dive into two solution approaches that have shown promise in recent years. Specifically, we discuss the guess-check-repair paradigm for synthesizing Skolem functions, and also present a knowledge compilation based approach for Boolean functional synthesis. Finally, we conclude with some perspectives on future research in this area. The talk is based on work reported in [1, 2, 3, 4, 5].

We consider the problem of synthesizing strategies in logically-specified infinite-state two-player games with LTL winning conditions. We lift classical fixpoint algorithms for synthesizing strategies in finite-states games, to our setting. Our evaluation of these algorithms show that they compare well with earlier techniques based on template-based logical synthesis and abstraction-refinement, on benchmarks from the literature.

This is joint work with Stanly Samuel and K V Raghavan.

Knowledge compilers often take as inputs a CNF formula and construct an equivalent Boolean circuit with specific properties. Generally, the size of the output circuit increases exponentially. However, for some families of CNF formulas, one can exploit the structure of the formulas to compile them efficiently. In this talk, I first give a general overview of knowledge compilation and of the circuits that knowledge compilers construct. Then, I present results on the compilation of non-CNF inputs. Seeing CNF as systems of constraints, where every constraint is a clause, I explain how positive results on the compilation of CNF with a certain structure can be extended to more general systems of constraints.

Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Furthermore, the synthesis of the resulting reactive system implementations necessitates the use of functional synthesis for theories beyond Boolean. In this talk, I will present a recent symbolic approach for the synthesis of infinite-state reactive systems, called attractor acceleration, which employs ranking arguments to improve the convergence of symbolic game-solving algorithms. I will then discuss the application and the challenges for functional synthesis in this context.

Reactive synthesis is the process of computing correct-by-construction finite-state controllers from temporal logic specifications. In this tutorial, we have a look at the basic concepts that underlie current reactive synthesis approaches. We discuss the topic on a fairly technical level in order to highlight the connections to functional and Boolean synthesis.

Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing techniques in Boolean functional synthesis, we define dependent variables in reactive synthesis as output variables that are uniquely assigned, given an assignment to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis that exploits dependent variables can solve some problems beyond the reach of existing techniques. Furthermore, we observe that among benchmarks with dependent variables, if the count of non-dependent variables is low ($\le 3$ in our experiments), our method outperforms state-of-the-art tools for synthesis.

In this talk we explore the connections between synthesis and automated reasoning techniques. Generally, synthesis, from logic perspective, is formalized as solving a formula of the following form.

where $P$ is a predicate parametrized by a vector of variables $𝐱$ and an unknown function $f$. Typically, the (second order) quantifier $\exists f$ it is omitted; in particular in Satisfiability Modulo Theories (SMT), where $f$ functions are implicitly quantified existentially.

Many approaches use solvers in a black-box fashion by assuming a certain template for $f$, such as linear, quadratic etc. [9]. Then, the synthesis problem is formulated as an SMT problem that search as for the parameters (coefficients) of the template. Interestingly, such approach can also be used to search for all the possible $f$ [1].

Some approaches integrate more deeply with the solver. A powerful technique is deskolemization of $f$ (as inverse of skolemization), which is possible, if $f$ is always applied to the same tuple of arguments everywhere in $P$. In the literature, such specifications are referred to as single-invocation properties [5, 8]. An example of such property would be $\forall x_1{x}_2.f(x_1,x_2)>x_1\wedge f(x_1,x_2)>x_2$, which would be deskolemized as $\forall x_1{x}_2\exists z.z>x_1\wedge z>x_2$.

For deskolemized version of the specification, $f$ can be that synthesized by quantifier elimination (QE) if the formula is in a theory that admits QE, such as linear real/integer arithmetic [7, 2], cf. [5, 6]. Alternatively, Reynolds et al. [8] synthesize $f$ by inspecting the SMT refutation (proof). Hozzová et al. [3] synthesize $f$ in the setting of first or logic (FOL), again from the proof, which relies on explicit axiomatization of any theory that may be used.

Specifications going beyond the single-invocation property fragment maybe tackled by embedding the language of possible solutions into the solver as than algebraic datatype [8]. More recent research shows that refutations containing mathematical induction enable synthesizing recursive functions [4].

Stochastic Boolean Satisfiability (SSAT) generalizes quantified Boolean formulas (QBFs) by allowing quantification over random variables. It is often referred to as games against nature and has applications in making decisions or optimizing under uncertainty. This talk will introduce SSAT, its recent developments, and its connection to Boolean functional synthesis.

In this talk, we will show that existing classical automated reasoning methods perform exceedingly well for computationally hard problems in quantum computing and physics. In particular, we demonstrate a linear-length #SAT encoding of the simulation and equivalence checking of universal quantum circuits. An implementation of this method, called Quokka#, outcompetes other state-of-the-art approaches using an off-the-shelve #SAT solver that supports negative weights (GPMC). While decision diagrams offer a viable alternative, we unveil their inherent limitations stemming from their inability to represent the prevalent stabilizer states. This limitation is particularly noteworthy considering the efficient classical simulatability of circuits generating such states. To address this constraint, we introduce Local Invertible Map Decision Diagrams (LIMDDs), which offer exponential improvements in succinctness compared to the combination of stabilizer formalism and existing decision diagrams. Finally, we illustrate how these findings hold relevance beyond quantum computing by translating them back to the domain of quantum physics. To achieve this, we build upon Darwiche and Marquis’ seminal “knowledge compilation map” approach, by pioneering a knowledge compilation map for quantum information. This map juxtaposes various decision diagrams against tensor networks and Boltzmann machines, two formalisms extensively utilized in physics to address quantum-hard problems such as simulating many-body systems and determining their ground energy. Our results underscore the significant potential of existing automated reasoning methods in both quantum computing and physics domains.

Temporal stream logic modulo theories (TSL-T) is used to specify the behavior of infinite state reactive systems. We present a refinement based synthesis method that works using LTL synthesis and SMT solving. First, a LTL underapproximation is computed and given to a LTL synthesis tool. In case this is unrealizable the created counter-strategy is analyzed for inconsistencies with the theory. New assumptions and predicates are added to the specification to rule out the counter-strategy and the LTL synthesis is run again. If the problem becomes realizable a program statisfying the original specification is extracted.

Bipartitioning the set of variables Var$(\mathrm{\Sigma })$ of a propositional formula $\mathrm{\Sigma }$ w.r.t. definability consists in pointing out a bipartition $⟨I,O⟩$ of Var$(\mathrm{\Sigma })$ such that $\mathrm{\Sigma }$ defines the variables of $O$ (outputs) in terms of the variables in $I$ (inputs), i.e., for every $o\in O$, there exists a formula ${\mathrm{\Phi }}_o$ over $I$ such that $o\iff {\mathrm{\Phi }}_o$ is a logical consequence of $\mathrm{\Sigma }$. The existence of ${\mathrm{\Phi }}_o$ given $o$, $I$, and $\mathrm{\Sigma }$ is a coNP-complete problem, and as such, it can be addressed in practice using a SAT solver. From a computational perspective, definability bipartitioning has been shown as a valuable preprocessing technique for model counting, a key task for a number of AI problems involving probabilities. To maximize the benefits offered by such a preprocessing, one is interested in deriving subset-minimal bipartitions in terms of input variables, i.e., definability bipartitions $⟨I,O⟩$ such that for every $i\in I$, $⟨I\setminus \{i\},O\cup \{i\}⟩$ is not a definability bipartition. We show how the computation of subset-minimal bipartitions can be boosted by leveraging not only the decisions furnished by SAT solvers (as done in previous approaches), but also the SAT witnesses (models and cores) justifying those decisions.

In this talk, I briefly outline the theoretical and practical advances that together form the foundation of Owl and Strix, state-of-the-art tools for LTL to automata translation and LTL synthesis, respectively.

This includes a large body of work, a small selection follows:

• $\mathrm{■}$

  Unified translation (JACM): https://doi.org/10.1145/3417995

• $\mathrm{■}$

  One theorem to rule them all (LICS): https://doi.org/10.1145/3209108.3209161

• $\mathrm{■}$

  Owl tool paper: https://doi.org/10.1007/978-3-030-01090-4_34

• $\mathrm{■}$

  Strix tool paper: https://doi.org/10.1007/978-3-319-96145-3_31

The small list above is the culmination of about a dozen papers, see the respective cites within for more details.

In this talk, we will look at the problem of synthesizing both the program and pre-condition, when the post-condition is given as Boolean combination of polynomial inequalities and variables take integral values over a bounded region. The problem does not have a sub-exponential time procedure under Exponential Time Hypothesis. We will discuss an approach that is more efficient than naive enumeration by exploiting results from algebraic geometry.

Attribute grammars allow the association of semantic actions to the production rules in context-free grammars, providing a simple yet effective formalism to define the semantics of a language. However, drafting the semantic actions can be tricky and a large drain on developer time. In this work, we propose a synthesis methodology to automatically infer the semantic actions from a set of examples associating strings to their meanings. We also propose a new coverage metric, derivation coverage. We use it to build a sampler to effectively and automatically draw strings to drive the synthesis engine. We build our ideas into our tool, PĀNINI, and empirically evaluate it on twelve benchmarks, including a forward differentiation engine, an interpreter over a subset of Java bytecode, and a mini-compiler for C language to two-address code. Our results show that PĀNINI scales well with the number of actions to be synthesized and the size of the context-free grammar, significantly outperforming simple baselines.

Temporal logics are powerful tools that are widely used for the synthesis and verification of reactive systems. The recent progress on Large Language Models (LLMs) has the potential to make the process of writing such specifications more accessible. However, writing specifications in temporal logics remains challenging for all but the most expert users. A key question in using LLMs for temporal logic specification engineering is to understand what kind of guidance is most helpful to the LLM and the users to easily produce specifications. Looking specifically at the problem of reactive program synthesis, we explore the impact of providing an LLM with guidance on the separation of control and data–making explicit for the LLM what functionality is relevant for the specification, and treating the remaining functionality as an implementation detail for a series of pre-defined functions and predicates. We present a benchmark set and find that this separation of concerns improves specification generation. Our benchmark provides a test set against which to verify future work in LLM generation of temporal logic specifications.

Inductive functional programming, also called inductive program synthesis, addresses the problem of learning (mostly recursive) functional programs from input/output examples. An related area of research is inductive logic programming (ILP). IP is a type of machine learning because programs (models) are synthesized by inductive generalisation. In contrast to statistical and neural approaches to machine learning, IP approaches typically only need a small number of training examples. Since learned models are represented in form of programs, IP belongs to the group of interpretable machine learning approaches. In the talk, I will give an introduction to inductive functional programming and also present basic concepts of ILP. Furthermore, I will point out how IP can be combined with Deep Learning Architectures for explainability.

More than a decade ago, I described how many problems in formal methods are effectively addressed through reduction to synthesis, including the synthesis of proof artifacts during verification, and synthesis within solvers such as for theory lemmas and quantifier instantiation. Additionally, I observed how an inductive, data-driven approach to synthesis is often very effective. In this talk, I review these ideas, which are also summarized in [1]. I also describe how they enable one to develop learning-theoretic foundations for synthesis, leading to the frameworks of formal inductive synthesis and oracle-guided inductive synthesis (OGIS), with initial theoretical results reported in [2]. Finally, I note how synthesis with large language models (LLMs) is but a special case of oracle-guided synthesis where the LLM forms an untrusted but often effective oracle for searching over large expression (program) spaces. I describe how we can use this oracle-guided synthesis view to formulate an approach to verified code transpilation with LLMs, which beats all conventional approaches to verified code transpilation – initial results are presented in [3].

Motivated by the recent development of scalable approaches to Boolean function synthesis, we study the problem of counting Boolean functions: given a Boolean specification between a set of inputs and outputs, count the number of functions of inputs such that the specification is met. This stands in relation to our problem analogously to the relationship between Boolean satisfiability and the model counting problem. Yet, counting Skolem functions poses considerable new challenges. From the complexity-theoretic standpoint, counting Skolem functions is not only #P-hard; it is quite unlikely to have an FPRAS (Fully Polynomial Randomized Approximation Scheme) as the problem of even synthesizing one Skolem function remains challenging, even given access to an NP oracle. The primary contribution of this work is the first algorithm, SkolemFC, that computes an estimate of the number of Skolem functions. SkolemFC relies on technical connections between counting functions and propositional model counting: our algorithm makes a linear number of calls to an approximate model counter and computes an estimate of the number of Skolem functions with theoretical guarantees. Moreover, we show that Skolem function count can be approximated through a polynomial number of calls to a SAT oracle. Our prototype displays impressive scalability, handling benchmarks comparably to state-of-the-art Skolem function synthesis engines, even though counting all such functions ostensibly poses a greater challenge than synthesizing a single function.

In a Dependency Quantified Boolean Formula (DQBF), each existentially quantified variable is annotated with a dependency set consisting of universally quantified variables. A model of a DQBF consists of functions that correctly assign values to the existentially quantified variables based on the values of the universally quantified variables they depend on. Determining whether a DQBF has a model is NEXP-complete, and DQBFs can naturally express a range of synthesis problems. This talk presents an algorithm for finding a model of a DQBF that iteratively refines a candidate model based on counterexamples. It covers techniques that are crucial to make this approach work well in practice, such as identifying unique Skolem functions by propositional definition extraction, and finding local repairs of invalid functions.

There is an issue we should address related to functional synthesis. Its definition is incomplete. It talks about inputs and outputs only – but many of the variables are in fact don’t cares. It is easily imaginable that many users don’t need the skolem function for a number of internal variables that are not inputs. However, current systems have to create a skolem function for these, too, potentially wasting the end user’s resources. In my opinion, this should to be changed, allowing users to give a dontcare set.

So, if e.g. there are 100 variables, and the user sets 1..50 as inputs, they should be able to say that they are only interested in the skolem function of variable 100 – and if that involves variables 51..99 then of course their skolem functions, too. But if, for example, variable 100 is not connected in any way, shape or form, to variable 66, then there is absolutely no point in creating the skolem function for variable 66. It would be noting but a waste of the end user’s resources. We should focus on what the end users want – and I’m quite sure they only want specific variable(s)’ skolem functions, not everything that isn’t an input.

Let’s discuss. Obviously this new formulation can gracefully simulate the original problem, simply set dontcare = $\mathrm{\varnothing }$. But I am pretty sure that once users start using functional synthesis, their dotcare set will be quite large.

To solve the reactive synthesis problem from LTL specifications or non-deterministic Buchi automata, there are two common approaches: either reduce it to the solving a parity game or solving a Rabin game. We discuss some algorithms to solve these games.

Reactive synthesis emerges as a trustworthy-by-design technique in developing verifiably correct autonomous AI systems. This talk puts a particular focus on reactive synthesis of Linear Temporal Logic on finite traces (LTLf). LTLf, on the one hand, allows for specifying a rich set of temporally extended specifications, and on the other hand, focuses on finite traces, which makes it particularly suitable for specifying tasks of autonomous AI systems. Note that autonomous AI systems will not get stuck accomplishing a task for all their lifetime, but only for a finite (but unbounded) number of steps. In this talk, I will present an overview of key advancements in LTLf synthesis, highlighting its scalability and potential in complex scenarios. These results base on a so-called DFA-technology, which essentially takes the maximal simplicity of reasoning about efficiently constructed deterministic finite word automaton (DFA) of the LTLf objective. The goal of this talk is to engage researchers in automated synthesis, encouraging further advances on the scalability and applicability of LTLf synthesis.