# 结合函数合成与自动机合成以发现因果反应式程序 > AutumnSynth 根据观察到的画面帧及用户动作（如点击和方向键）构成的轨迹，合成 Autumn 程序；Autumn 是面向 Atari 风格网格世界的函数式反应式语言。基于启发式的感知步骤将每帧解析为带类型的对象，跟踪步骤再将对象跨时间步关联起来。随后，合成器为每个观察到的变化寻找更新函数，并搜索触发该变化的事件。当基于可观察状态的事件都无法解释某次更新时，自动机合成会借助基于 SAT 的 Sketch 编码或更快的启发式方法，引入计数器、模式等潜在状态。作者提出了含 30 个程序的 Causal Inductive Synthesis Corpus（CISC），启发式版本在其中合成出 27 个程序；经少量修改的版本在第三方 EMPA 网格世界语料库的 27 个游戏中合成出 21 个。 - 作者：Ria Das; Joshua B. Tenenbaum; Armando Solar-Lezama; Zenna Tavares - 原标题：Combining Functional and Automata Synthesis to Discover Causal Reactive Programs - 发表载体：Proceedings of the ACM on Programming Languages (POPL 2023) - 发表状态：期刊论文 - 出版／提交日期：2023 年 1 月 9 日 - 日期依据：ACM 提交的 Crossref 元数据将印刷出版日期记为 2023-01-09；ACM 论文页面同样显示的 2023-01-11 在线出版日期在元数据说明中单独记录。本条目不以 POPL 会议日期替代。 - DOI：10.1145/3571249 - 来源复核于：2026-10-19 - 收录于：2026-10-31 - 原始论文： - PDF： - BibTeX： - 目录页面： - 记录 JSON： - 英文版：[English](https://awesomerea.org/papers/paper-autumnsynth/index.md) ## 研究范围与局限 目标是可用 Autumn 表达、完全可观察的小型网格世界，而非具有连续物理、复杂图形或已编译代码的游戏。感知与跟踪基于启发式；由于 Autumn 将对象渲染为部分透明，感知步骤不处理遮挡。CISC 的输入轨迹由人工构造，以覆盖各模型的动态；“成功”指合成程序能复现给定轨迹，而非与真实程序语义等价。启发式版本的运行时间从约两分钟到 9–13 小时不等；Sketch 版本在若干基准上 24 小时后超时，部分 EMPA 游戏也在 40 小时后超时。EMPA 需要针对随机事件做领域特定修改；由于多数 EMPA 游戏具有非确定性，其结果通过人工检查确认，且每个游戏只使用第一关。在新的 CISC 测试轨迹上，有四个合成程序因训练轨迹未展示全部动态而偏离真实程序，对其中三个重新测试时，拼接多条轨迹后恢复出了真实程序。对于随机事件，AutumnSynth 只检测非确定性，并不推断其背后的概率分布。该方法属于符号程序合成，并未使用大语言模型。 ## 与本合集的关联 补充一种从观察到的游玩过程中合成游戏程序（包括潜在状态）的符号方法，与本节基于大语言模型的代码世界模型及游戏重建研究互补。 ## 发表与复核说明 Crossref、ACM 页面存档与 31 页的论文给出四位作者，以及 Proceedings of the ACM on Programming Languages 第 7 卷 POPL 期 Article 56、第 1628–1658 页。Crossref 记载印刷出版于 2023-01-09、在线出版于 2023-01-11，论文页脚标为 2023 年 1 月。ACM 论文以 CC BY 4.0 开放获取。论文称 Autumn 语言与 AutumnSynth 以 Julia 实现，但未链接代码或产物；作者的出版物页面也只链接论文。第一作者账户下的 riadas/AutumnSynth.jl 仓库在其唯一一次 2023-03-15 提交中只有一行 README。 ## 一手来源 1. 2. 3. 4. 5. 6. 7. ## 关于此条目 已依据论文及一手来源复核。请通过原始论文或 BibTeX 引用原作者。 原创说明采用 MIT 许可；外部项目、论文与素材保留各自的权利和许可。