paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Programming-by-Demonstration for Long-Horizon Robot Tasks

面向长时程机器人任务的示教编程
POPL 8(POPL)2024匹配度 4/10 · 论文将 LLM 引导搜索用于程序合成并包含不可实现性证明,属于 AI→PL 的邻近方向;但其核心是机器人长时程任务的编程示教,并非静态分析/形式化验证,也不涉及浮点、贝叶斯程序分析或 Agentic/ML 系统程序分析。引用 11 inbox
Noah Patton, Kia Rahmani, Meghana Missula, Joydeep Biswas, Işıl Dillig
crossref: 2026-09-10

AI 速览

一句话:提出面向长时程机器人任务的程序化示教学习算法,先学程序草图,再用 LLM 引导搜索补全并判定不可实现性。

本文研究程序化示教学习(LfD),目标是从用户演示中学习可控制机器人行为的程序,尤其针对需要嵌套循环与多条件分支等复杂控制流的长时程任务。方法分两步:先从演示中学习刻画目标控制流的程序草图,再通过 LLM 引导的搜索补全草图,并引入证明示教编程问题不可实现的新技术以剪枝。作者实现工具 prolex,在 120 个复杂任务与环境中评测:120 秒限制下 80% 可找到与演示一致的程序;返回解的任务中 81% 仅需一次演示即可恢复真实程序。对比 CVC5 仅解决 25%,GPT-Synth 因环境复杂无一解决。

问题
如何从用户演示中为长时程机器人任务合成具有复杂控制流结构的程序。
方法
先学习捕获目标控制流的程序草图,再用 LLM 引导的搜索补全草图,并利用新的不可实现性证明技术进行剪枝。
评估
实现工具 prolex,在 120 个复杂任务与环境中评测,并与 CVC5、GPT-Synth 对比成功率及恢复真实程序的能力。
原文摘要(Abstract)

The goal of programmatic Learning from Demonstration (LfD) is to learn a policy in a programming language that can be used to control a robot’s behavior from a set of user demonstrations. This paper presents a new programmatic LfD algorithm that targets long-horizon robot tasks which require synthesizing programs with complex control flow structures, including nested loops with multiple conditionals. Our proposed method first learns a program sketch that captures the target program’s control flow and then completes this sketch using an LLM-guided search procedure that incorporates a novel technique for proving unrealizability of programming-by-demonstration problems. We have implemented our approach in a new tool called prolex and present the results of a comprehensive experimental evaluation on 120 benchmarks involving complex tasks and environments. We show that, given a 120 second time limit, prolex can find a program consistent with the demonstrations in 80% of the cases. Furthermore, for 81% of the tasks for which a solution is returned, prolex is able to find the ground truth program with just one demonstration. In comparison, CVC5, a syntaxguided synthesis tool, is only able to solve 25% of the cases even when given the ground truth program sketch , and an LLM-based approach, GPT-Synth, is unable to solve any of the tasks due to the environment complexity.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2580,
  title = {Programming-by-Demonstration for Long-Horizon Robot Tasks},
  author = {Noah Patton and Kia Rahmani and Meghana Missula and Joydeep Biswas and Işıl Dillig},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632860}
}