Joint Verification and Refinement of Language Models for Safety-Constrained Planning
This addresses the reliability issue for deploying language models in real-world robotic systems, offering a method to ensure safety and improve efficiency, though it is incremental as it builds on existing verification and fine-tuning approaches.
The paper tackles the problem of language models generating error-prone robot programs that violate safety specifications by developing a verification method that converts programs into automata and proves safety for arbitrary combinations, and an automated fine-tuning procedure that uses verification outcomes for supervision. Empirical results show a 30% increase in specification-compliant program generation and a 50% reduction in training time.
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.