SYNT 2019

TBA

An attractive alternative to manual implementation is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). We demonstrate the effectiveness of TSL on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic threepenny-gui library, and to hardware using the Applicative hardware description language ClaSH.

Temporal specifications describe desired long-term behavior. The automated synthesis of programs from temporal specifications has a long and fascinating history, which has generated beautiful mathematics. Much of the attention in practice has been on the synthesis of synchronous hardware circuits. In this talk, I suggest other promising domains, such as the control of IoT (Internet of Things) devices and the coordination of multiple heterogeneous robots. These domains force a reformulation of the basic synthesis framework, by bringing in asynchrony and partial information. Programs for those domains should, ideally, also be robust against noise and failures. I will sketch some initial results on this new framework. Scalability is an immediate challenge: I will also discuss possible ways of ameliorating state explosion.

The design of a coordinator for multiple, independent, reactive agents is a complex task. Coordination synthesis is the automated construction of a coordinator from a specification and behavioral description of the reactive agents. Prior work on coordination synthesis make use of two critical assumptions: (a). all reactive agents are synchronized, (b). the coordinator has complete information about the reactive agents. However, we argue that realistic multi-agent scenarios violate both of these assumptions, rendering existing techniques unsuitable for coordination synthesis. To this end, this work presents an algorithm for coordination synthesis with both asynchrony and partial information. Our synthesis procedure uses high-level languages for specifications and agents, namely we use linear temporal properties for specifications and Communicating Sequential Processes (CSPs) for the reactive agents.

We target the efficient construction of a safety shield for decision making in scenarios that incorporate uncertainties. Markov decision processes (MDPs) are prominent models to capture such planning problems. Reinforcement learning (RL) is a machine learning technique to determine near-optimal policies in MDPs that works even on partially unknown models, and promises superior scalability in comparison to traditional verification techniques. However, during exploration of the MDP, RL lacks safety guarantees, that is, generated policies may induce harmful behavior. We present the concept of a shield that forces decision-making to provably adhere to safety constraints with high probability. In a separation of concerns, we use model checking to efficiently compute the probabilities of critical decisions within a safety-relevant fragment of the MDP. We use model checking results to realize a shield that is applied to an RL algorithm which then optimizes the actual performance objective. We show that we achieve (near-)optimal behavior both for the safety constraints and for the actual learning objective. In our experiments, we demonstrate on the arcade game PAC-MAN that the learning efficiency increases as the learning needs orders of magnitude fewer episodes.

Temporal synthesis is the automated design of a system that interacts with an environment, using a declarative specification of the system's behavior. A popular language for providing such a specification is Linear Temporal Logic, or LTL. LTL synthesis in the general case has remained, however, a hard problem to solve in practice. Because of this, many works have focused on developing synthesis procedures for specific fragments of LTL for which the synthesis problem is easier. Our work focuses on two variants of LTL for which synthesis is significantly simpler algorithmically than the general case. The first, LTL synthesis, is the process of finding a strategy that satisfies a linear temporal specification over finite rather than infinite traces, a problem that has applications in a number of AI planning problems. The second is Safety LTL, which we define to be the Until-free fragment of LTL in Negation Normal Form (NNF), and which expresses safety properties. The intrinsic motivation for this fragment is the observation that in many cases it is not enough to say that something "good" will eventually happen, we need to say by when it will happen. We exploit the fact that the synthesis problem in both of these variants can be reduced to a simpler game than for general infinite-word LTL, by employing a construction based on finite automata, which can be more efficiently constructed, determinized and minimized. We then use symbolic techniques based on BDDs to solve the game, and the mechanism of Boolean synthesis to compute a winning strategy.

We study the reactive synthesis problem of HyperQPTL, which is an extension of linear-time temporal logic with explicit trace and propositional quantification. We identify fragments, containing formulas like promptness, for which the synthesis problem remains decidable. In contrast to the satisfiability problem of HyperQPTL, we show that propositional quantification has an immediate impact on the decidability of the realizability problem.

Despite the practical successes of program synthesis, we still do not have systematic frameworks for understanding when synthesis can be successful. In particular, for a given synthesis algorithm, we would like to answer questions such as: How many examples does my algorithm need to synthesize a program that meets a desired specification? How long does it take for the synthesis algorithm to terminate? Similar questions were raised many years ago in machine learning, giving birth to the field of Computational Learning Theory, which allowed us to understand what functions can be efficiently learned. It is therefore natural to ask whether a similar theory can be developed for program synthesis. In this talk, I will show that developing such a theory is indeed possible. As a concrete example, I will present an algorithm, DIGITS, for synthesizing programs that meet a given probabilistic logical constraint. Unlike many synthesis algorithms that only converge to a correct program "in the limit", DIGITS is guaranteed to terminate in polynomially many rounds. Finally, I'll use DIGITS to present a number of open questions for the new field of "Computational Synthesis Theory".

Studies on program synthesis problems with user-specified search space propel program synthesis to the more practical field. But it is usually not enough to produce any correct solution. In this abstract, we consider the following two questions: 1) how can we find a "good" solution according to certain metric--e.g., produce programs of reasonable size--when there is more than one valid candidate solution in the search space, and 2) how can we provide a certificate of unrealizability when there is no solution in the search space. To answer the questions, we introduce two types of guarantees in program synthesis. Firstly, quantitative objectives that allow users to prefer one solution than others. Secondly, the ability to answer unrealizable when there is no solution. In this abstract, we show two works about introducing guarantees into program synthesis problems and solving program synthesis problems with guarantees. Finally, we present some interesting topic as future directions for each type of guarantee.

Data analysis has the capability to enrich the lives of many, yet it presents a fundamental threat to individual privacy. Formal privacy constraints such as differential privacy serve to protect individual rights while allowing large-scale data analytics to proceed relatively unhindered. However, such privacy constraints present a significant barrier to the access of relevant data. In this abstract, we present a solution that leverages type-directed synthesis and the privacy-aware type system DFuzz to allow users to automatically and efficiently synthesize programs that respect privacy constraints. Furthermore, we introduce a technique for proving randomized privacy mechanisms are sufficiently accurate via reduction to synthesis.

The key to attaining more general artificial intelligence is to develop architectures that are capable of learning complex algorithmic behaviors modeled as programs. The ability to learn programs can allow these architectures to learn to compose high-level abstractions that can in turn lead to many benefits: i) enable neural architectures to perform more complex tasks, ii) learn interpretable representations (programs which can be analyzed, debugged, or modified), and iii) better generalization to new inputs (like algorithms). In this talk, I will present some of our recent work in developing neural architectures for learning programs from examples and natural language.

We define and study the problem of modular concept learning, that is, learning a concept that is a cross product of component concepts. If an element's membership in a concept depends solely on it's membership in the components, learning the concept as a whole can be reduced to learning the components. We analyze this problem with respect to different types of oracle interfaces, defining different sets of queries. If a given oracle interface cannot answer questions about the components, learning can be difficult, even when the components are easy to learn with the same type of oracle queries. While learning from superset queries is easy, learning from membership, equivalence, or subset queries is harder. However, we show that these problems become tractable when oracles are given a positive example and are allowed to ask membership queries.