2023 · Journal article

Combining Functional and Automata Synthesis to Discover Causal Reactive Programs

Ria Das; Joshua B. Tenenbaum; Armando Solar-Lezama; Zenna Tavares

AutumnSynth synthesizes a program in Autumn, a functional reactive language for Atari-style grid worlds, from a trace of observed frames and user actions such as clicks and arrow keys. Heuristic perception parses each frame into typed objects and tracking links them across time steps. The synthesizer then finds an update function for each observed change and searches for the event that triggers it. When no event over the observed state explains an update, automata synthesis invents latent state, such as counters or modes, using a SAT-based Sketch encoding or a faster heuristic. The authors introduce the 30-program Causal Inductive Synthesis Corpus (CISC), on which the heuristic variant synthesizes 27 programs. A slightly modified version synthesizes 21 of 27 games from the third-party EMPA grid-world corpus.

Scope and limitations

Targets are small, fully observed grid worlds expressible in Autumn, not games with continuous physics, rich graphics or compiled code. Perception and tracking are heuristic, and because Autumn renders objects partially transparent, perception does not address occlusion. CISC input traces were constructed manually to exercise each model’s dynamics, and success means the synthesized program reproduces the given trace, not semantic equivalence to the ground truth. Heuristic runtimes range from about two minutes to 9–13 hours; the Sketch variants time out after 24 hours on several benchmarks, and EMPA runs time out after 40 hours on some games. EMPA required domain-specific changes for random events. Because most EMPA games are nondeterministic, their results were checked by manual inspection, and only the first level of each game was used. On new CISC test traces, four synthesized programs diverged from the ground truth because their training traces did not show all dynamics, and concatenating several traces recovered the ground-truth program for the three that were retested. For random events AutumnSynth detects nondeterminism but does not infer the underlying probability distributions. The method is symbolic program synthesis and does not use an LLM.

Why it fits this collection

Adds symbolic synthesis of game programs, including latent state, from observed play, complementing the section’s LLM-based code world-model and game-reconstruction research.

Publication and review details

Venue: Proceedings of the ACM on Programming Languages (POPL 2023)
Status: Journal article
Publication / posting date: January 9, 2023
Date source: ACM’s Crossref deposit records print publication on 2023-01-09; the online-publication date of 2023-01-11, also shown on the ACM article page, is recorded separately in metadata notes. The POPL meeting dates are not substituted.
DOI: 10.1145/3571249

Crossref, the archived ACM page and the 31-page article give the four authors, Proceedings of the ACM on Programming Languages volume 7, issue POPL, Article 56, pages 1628–1658. Crossref records print publication on 2023-01-09 and online publication on 2023-01-11, and the article footer gives January 2023. The ACM article is open access under CC BY 4.0. The paper says the Autumn language and AutumnSynth were implemented in Julia but links no code or artifact. The author’s publication page links only papers. The riadas/AutumnSynth.jl repository under the first author’s account contained only a one-line README at its single 2023-03-15 commit, so no code link is recorded. No code or experiments were run.

Sources reviewed 2026-10-19

Source review only; experiments were not rerun for this collection. Cite the original authors using the linked paper or BibTeX.

Report an outdated entry Suggest a translation fix

Scope and limitations

Why it fits this collection

Publication and review details

Primary sources