一句话：提出闭环反例引导合成框架，融合LLM规划、SMT验证与可微行为树合成，实现长时程机器人神经符号策略学习。
该文针对机器人程序化强化学习中长时程、稀疏奖励任务里自然语言、形式规约与可执行代码之间语义难以对齐的问题，提出闭环、反例引导的神经符号合成框架。方法首先将自然语言任务描述转为PDDL，通过Guess-Check-Critique循环交替进行LLM规划生成与SMT验证，得到可信高层规划；随后把已验证规划中的符号抽象自动编译为参数化终止条件，与低层策略联合优化以保证语义一致，并将子策略组合为行为树进行微调，同时利用验证与学习反馈闭环迭代抽象与编译，增量构建可复用技能库。在有挑战的长时程机器人任务上，该方法优于现有最优方法，并具备可解释性与泛化能力。
Recent advances in foundation models have motivated hybrid programming that integrates natural language descriptions, formal specifications, and executable code. A critical challenge in such systems lies in achieving semantic alignment across heterogeneous representations at different abstraction levels. This challenge is particularly pressing in programmatic reinforcement learning (PRL) for robotics, where long-horizon, sparse-reward tasks demand tight coordination between symbolic reasoning and continuous control. Existing approaches either rely on manually engineered symbolic representations or on LLM-generated plans that might be untrustworthy or infeasible to execute, leaving such fundamental gaps unaddressed. We present a closed-loop, counterexample-guided synthesis framework that unifies LLM-based planning, formal verification, and differentiable behavior tree (BT) synthesis for neuro-symbolic policy learning. The framework first converts natural language task descriptions into PDDL, then generates valid high-level plans via a Guess-Check-Critique loop that interleaves LLM generation with SMT-based verification. We automatically compile symbolic abstractions in verified plans into parameterized termination conditions, and co-optimize them with low-level policies to enforce semantic consistency. The learned sub-policies are composed into an integrated BT and fine‑tuned to ensure task-level executability. Furthermore, we perform closed-loop iterations of abstractions and compilations using feedback from verification and learning, while incrementally building a reusable skill library for efficient knowledge transfer. Experiments on challenging long-horizon robotic tasks show that our method exceeds state-of-the-art methods while providing interpretability and generalization.
@article{HuangWMMW26,
title = {Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks},
author = {Yu Huang and Ziji Wu and Zhengyi Ma and Kexin Ma and Ji Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808338}
}