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

Understand

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.