Joint Verification and Refinement of Language Models for Safety-Constrained Planning

TL;DR

This paper presents a method to verify and refine language model-generated robot programs to ensure safety compliance, significantly improving correctness and training efficiency in robotic applications.

Contribution

It introduces an automaton-based verification approach combined with automated fine-tuning, enabling safer program generation and reducing training complexity.

Findings

30% increase in safe program generation

Training time halved compared to full program fine-tuning

Verification reduces errors in robot task programs

Abstract

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.