More Like this

1. Synthesizing Formal Semantics from Executable Interpreters

   https://doi.org/10.1145/3689724  

   Liu, Jiangyi; Murphy, Charlie; Grover, Anvay; Johnson, Keith JC; Reps, Thomas; D’Antoni, Loris (October 2024, Proceedings of the ACM on Programming Languages)

   Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be a daunting and error-prone task, this requirement stands in the way of such frameworks being adopted by non-expert users. We present an algorithm that can automatically synthesize inductively defined syntax-directed semantics when given (i) a grammar describing the syntax of a language and (ii) an executable (closed-box) interpreter for computing the semantics of programs in the language of the grammar. Our algorithm synthesizes the semantics in the form of Constrained-Horn Clauses (CHCs), a natural, extensible, and formal logical framework for specifying inductively defined relations that has recently received widespread adoption in program verification and synthesis. The key innovation of our synthesis algorithm is a Counterexample-Guided Synthesis (CEGIS) approach that breaks the hard problem of synthesizing a set of constrained Horn clauses into small, tractable expression-synthesis problems that can be dispatched to existing SyGuS synthesizers. Our tool Synantic synthesized inductively-defined formal semantics from 14 interpreters for languages used in program-synthesis applications. When synthesizing formal semantics for one of our benchmarks, Synantic unveiled an inconsistency in the semantics computed by the interpreter for a language of regular expressions; fixing the inconsistency resulted in a more efficient semantics and, for some cases, in a 1.2x speedup for a synthesizer solving synthesis problems over such a language. 

   more » « less
2. Combining Functional and Automata Synthesis to Discover Causal Reactive Programs

   https://doi.org/10.1145/3571249  

   Das, Ria; Tenenbaum, Joshua B.; Solar-Lezama, Armando; Tavares, Zenna (January 2023, Proceedings of the ACM on Programming Languages)

   We present a new algorithm that synthesizes functional reactive programs from observation data. The key novelty is to iterate between a functional synthesis step, which attempts to generate a transition function over observed states, and an automata synthesis step, which adds any additional latent state necessary to fully account for the observations. We develop a functional reactive DSL called Autumn that can express a rich variety of causal dynamics in time-varying, Atari-style grid worlds, and apply our method to synthesize Autumn programs from data. We evaluate our algorithm on a benchmark suite of 30 Autumn programs as well as a third-party corpus of grid-world-style video games. We find that our algorithm synthesizes 27 out of 30 programs in our benchmark suite and 21 out of 27 programs from the third-party corpus, including several programs describing complex latent state transformations, and from input traces containing hundreds of observations. We expect that our approach will provide a template for how to integrate functional and automata synthesis in other induction domains. 

   more » « less
3. Inductive Program Synthesis Guided by Observational Program Similarity

   https://doi.org/10.1145/3622830  

   Feser, Jack; Dillig, Işıl; Solar-Lezama, Armando (October 2023, Proceedings of the ACM on Programming Languages)

   We present a new general-purpose synthesis technique for generating programs from input-output examples. Our method, called metric program synthesis, relaxes the observational equivalence idea (used widely in bottom-up enumerative synthesis) into a weaker notion of observational similarity, with the goal of reducing the search space that the synthesizer needs to explore. Our method clusters programs into equivalence classes based on an expert-provided distance metric and constructs a version space that compactly represents “approximately correct” programs. Then, given a “close enough” program sampled from this version space, our approach uses a distance-guided repair algorithm to find a program that exactly matches the given input-output examples. We have implemented our proposed metric program synthesis technique in a tool called SyMetric and evaluate it in three different domains considered in prior work. Our evaluation shows that SyMetric outperforms other domain-agnostic synthesizers that use observational equivalence and that it achieves results competitive with domain-specific synthesizers that are either designed for or trained on those domains. 

   more » « less
4. MoVer: Motion Verification for Motion Graphics Animations

   https://doi.org/10.1145/3731209  

   Ma, Jiaju; Agrawala, Maneesh (August 2025, ACM Transactions on Graphics)

   While large vision-language models can generate motion graphics animations from text prompts, they regularly fail to include all spatio-temporal properties described in the prompt. We introduce MoVer, a motion verification DSL based on first-order logic that can check spatio-temporal properties of a motion graphics animation. We identify a general set of such properties that people commonly use to describe animations (e.g., the direction and timing of motions, the relative positioning of objects, etc.). We implement these properties as predicates in MoVer and provide an execution engine that can apply a MoVer program to any input SVG-based motion graphics animation. We then demonstrate how MoVer can be used in an LLM-based synthesis and verification pipeline for iteratively refining motion graphics animations. Given a text prompt, our pipeline synthesizes a motion graphics animation and a corresponding MoVer program. Executing the verification program on the animation yields a report of the predicates that failed and the report can be automatically fed back to LLM to iteratively correct the animation. To evaluate our pipeline, we build a synthetic dataset of 5600 text prompts paired with ground truth MoVer verification programs. We find that while our LLM-based pipeline is able to automatically generate a correct motion graphics animation for 58.8% of the test prompts without any iteration, this number raises to 93.6% with up to 50 correction iterations. Our code and dataset are at https://mover-dsl.github.io. 

   more » « less
5. utomating Mechanism Design with Program Synthesis

   Narayanasamy, Sai Kiran (May 2022, Proc. Automated Learning Agents Workshop)

   This paper presents a new approach to the automated design of mechanisms that incentivize self-interested agents to maximize a global objective (such as revenue or social welfare) in equilibrium. Prior work on automated design has either been restricted to relatively simple mechanisms, or represented mechanisms as neural networks that are hard to interpret and cannot easily incorporate prior knowledge. In this paper, we propose program synthesis as a way around these issues. Concretely, we formalize the problem of designing mechanisms in the form of multiagent environments whose transition and reward functions are programs in a domainspecific language (DSL), in order to maximize an outcome such as revenue or social welfare under given assumptions on how agents act in these environments. We present an initial algorithm, based on a combination of stochastic search over programs and Bayesian optimization, for this problem. We empirically evaluate the algorithm in two domains with different characteristics. Our experiments suggest that the approach can synthesize programmatic mechanisms that are human-interpretable and also perform well. 

   more » « less