让大模型生成的机器人程序自动通过安全验证并高效优化。
Joint Verification and Refinement of Language Models for Safety-Constrained Planning
- 将程序转为状态机形式，按安全规范逐层验证
- 验证后程序组合仍安全，降低复杂度30%
- 用验证结果指导微调，训练效率提升50%
大型语言模型能从自然语言描述生成用于执行机器人任务的程序（如Python），但这些程序常违反外部任务规范。缺乏有效验证方法使得模型在真实系统中难以可靠部署。本文提出一种将生成的机器人程序转化为基于自动机的表示，并据此验证其是否符合任务相关的安全规范。我们证明了任意经验证程序的组合仍满足安全规范，从而无需对由多个简单程序构成的复杂程序单独验证，显著降低计算复杂度。随后，我们引入一种自动化微调流程，利用验证结果作为监督信号。基于该定理，只需训练模型生成安全的子组件，即可实现整体程序的安全性，提升训练效率。在机器人应用中的实证结果显示，生成符合规范程序的概率提升了30%，训练时间相比直接微调完整程序减少一半。
原文摘要 · Abstract (English)
Large language models possess impressive capabilities in generating programs (e.g., Python) from natural language descriptions to execute robotic tasks. However, these generated programs often contain errors that violate externally given task specifications. Without an effective method to verify their correctness, the reliable deployment of language models in real-world systems is practically infeasible. We develop a method that converts generated robot programs into an automaton-based representation and verifies them against task-relevant safety specifications. We establish a theorem that any arbitrary combination of the verified programs will also satisfy the safety specifications. Hence, the method eliminates the need to verify complex programs composed of multiple simpler ones, reducing computation complexity. We then introduce an automated fine-tuning procedure that leverages verification outcomes for supervision. By applying the theorem, this procedure only requires training the model to generate safe sub-components, thereby improving training efficiency. Empirical results on robot applications show a 30 percent increase in the probability of generating specification-compliant programs, with training time reduced by half compared to fine-tuning on generating full programs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。