AwesomeREA.org

2023 · 期刊论文

结合函数合成与自动机合成以发现因果反应式程序

Combining Functional and Automata Synthesis to Discover Causal Reactive Programs

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

AutumnSynth 根据观察到的画面帧及用户动作（如点击和方向键）构成的轨迹，合成 Autumn 程序；Autumn 是面向 Atari 风格网格世界的函数式反应式语言。基于启发式的感知步骤将每帧解析为带类型的对象，跟踪步骤再将对象跨时间步关联起来。随后，合成器为每个观察到的变化寻找更新函数，并搜索触发该变化的事件。当基于可观察状态的事件都无法解释某次更新时，自动机合成会借助基于 SAT 的 Sketch 编码或更快的启发式方法，引入计数器、模式等潜在状态。作者提出了含 30 个程序的 Causal Inductive Synthesis Corpus（CISC），启发式版本在其中合成出 27 个程序；经少量修改的版本在第三方 EMPA 网格世界语料库的 27 个游戏中合成出 21 个。

研究范围与局限

目标是可用 Autumn 表达、完全可观察的小型网格世界，而非具有连续物理、复杂图形或已编译代码的游戏。感知与跟踪基于启发式；由于 Autumn 将对象渲染为部分透明，感知步骤不处理遮挡。CISC 的输入轨迹由人工构造，以覆盖各模型的动态；“成功”指合成程序能复现给定轨迹，而非与真实程序语义等价。启发式版本的运行时间从约两分钟到 9–13 小时不等；Sketch 版本在若干基准上 24 小时后超时，部分 EMPA 游戏也在 40 小时后超时。EMPA 需要针对随机事件做领域特定修改；由于多数 EMPA 游戏具有非确定性，其结果通过人工检查确认，且每个游戏只使用第一关。在新的 CISC 测试轨迹上，有四个合成程序因训练轨迹未展示全部动态而偏离真实程序，对其中三个重新测试时，拼接多条轨迹后恢复出了真实程序。对于随机事件，AutumnSynth 只检测非确定性，并不推断其背后的概率分布。该方法属于符号程序合成，并未使用大语言模型。

与本合集的关联

补充一种从观察到的游玩过程中合成游戏程序（包括潜在状态）的符号方法，与本节基于大语言模型的代码世界模型及游戏重建研究互补。

发表与复核详情

发表载体
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

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，因此不记录代码链接。本次未运行代码或实验。

来源复核于

本合集仅做来源复核，未重新运行论文实验。请通过原始论文或 BibTeX 引用原作者。

报告条目过时 建议修正翻译

一手来源

  1. https://dl.acm.org/doi/10.1145/3571249
  2. https://web.archive.org/web/20240416064933/https://dl.acm.org/doi/10.1145/3571249
  3. https://api.crossref.org/works/10.1145/3571249
  4. https://dl.acm.org/doi/pdf/10.1145/3571249
  5. https://web.archive.org/web/20240416110317/https://dl.acm.org/doi/pdf/10.1145/3571249
  6. https://github.com/riadas/AutumnSynth.jl/tree/e62edb9368c95c2271008ecb4e547afa4d2e393b
  7. https://riadas.github.io/