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

arXiv: https://arxiv.org/abs/2410.14865 · HTML: https://mlsanity.com/paper/2410.14865/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 37 references that are in the map.
- First posted on arXiv 18 Oct 2024.

## Builds on (most cited first, 21 of 21)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [GPT Understands, Too](https://mlsanity.com/paper/2103.10385/) (2021)
- [ProgPrompt: Generating Situated Robot Task Plans using Large Language Models](https://mlsanity.com/paper/2209.11302/) (2022)
- [InCoder: A Generative Model for Code Infilling and Synthesis](https://mlsanity.com/paper/2204.05999/) (2022)
- [Fine-Tuning Pretrained Language Models: Weight Initializations, Data Orders, and Early Stopping](https://mlsanity.com/paper/2002.06305/) (2020)
- [Unified Pre-training for Program Understanding and Generation](https://mlsanity.com/paper/2103.06333/) (2021)
- [CodeT5+: Open Code Large Language Models for Code Understanding and Generation](https://mlsanity.com/paper/2305.07922/) (2023)
- [LEVER: Learning to Verify Language-to-Code Generation with Execution](https://mlsanity.com/paper/2302.08468/) (2023)
- [IntelliCode Compose: Code Generation Using Transformer](https://mlsanity.com/paper/2005.08025/) (2020)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Deploying and Evaluating LLMs to Program Service Mobile Robots](https://mlsanity.com/paper/2311.11183/) (2023)
- [Fine-Tuning Language Models Using Formal Methods Feedback](https://mlsanity.com/paper/2310.18239/) (2023)
- [Multimodal Pretrained Models for Verifiable Sequential Decision-Making: Planning, Grounding, and Perception](https://mlsanity.com/paper/2308.05295/) (2023)
- [Robo-Instruct: Simulator-Augmented Instruction Alignment For Finetuning Code LLMs](https://mlsanity.com/paper/2405.20179/) (2024)
- [ESBMC-Python: A Bounded Model Checker for Python Programs](https://mlsanity.com/paper/2407.03472/) (2024)

## Built on by (most cited first, 6 of 6)

- [Safety Guardrails for LLM-Enabled Robots](https://mlsanity.com/paper/2503.07885/) (2025)
- [VLN-Zero: Rapid Exploration and Cache-Enabled Neurosymbolic Vision-Language Planning for Zero-Shot Transfer in Robot Navigation](https://mlsanity.com/paper/2509.18592/) (2025)
- [A Survey of Foundation Models for IoT: Taxonomy and Criteria-Based Analysis](https://mlsanity.com/paper/2506.12263/) (2025)
- [RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verification](https://mlsanity.com/paper/2510.26935/) (2025)
- [CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action](https://mlsanity.com/paper/2608.27797/) (2026)
- [Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions](https://mlsanity.com/paper/2610.02662/) (2026)

## Abstract (arXiv)

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.