# RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verification

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 38 references that are in the map.
- First posted on arXiv 30 Oct 2025.

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

- [Refusal in Language Models Is Mediated by a Single Direction](https://mlsanity.com/paper/2406.11717/) (2024)
- [Deliberative Alignment: Reasoning Enables Safer Language Models](https://mlsanity.com/paper/2412.16339/) (2024)
- [LLMs Know More Than They Show: On the Intrinsic Representation of LLM Hallucinations](https://mlsanity.com/paper/2410.02707/) (2024)
- [Do I Know This Entity? Knowledge Awareness and Hallucinations in Language Models](https://mlsanity.com/paper/2411.14257/) (2024)
- [SEAL: Steerable Reasoning Calibration of Large Language Models for Free](https://mlsanity.com/paper/2504.07986/) (2025)
- [Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents](https://mlsanity.com/paper/2402.00798/) (2024)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning](https://mlsanity.com/paper/2409.17270/) (2024)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Know Where You're Uncertain When Planning with Multimodal Foundation Models: A Formal Framework](https://mlsanity.com/paper/2411.01639/) (2024)
- [Automaton-Based Representations of Task Knowledge from Generative Language Models](https://mlsanity.com/paper/2212.01944/) (2022)
- [Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planning](https://mlsanity.com/paper/2510.21302/) (2025)
- [Enhancing Legal Compliance and Regulation Analysis with Large Language Models](https://mlsanity.com/paper/2404.17522/) (2024)
- [Preemptive Detection and Steering of LLM Misalignment via Latent Reachability](https://mlsanity.com/paper/2509.21528/) (2025)
- [The Challenges and Opportunities of Human-Centered AI for Trustworthy Robots and Autonomous Systems](https://mlsanity.com/paper/2105.04408/) (2021)
- [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)
- [Neuro-Symbolic AI for Compliance Checking of Electrical Control Panels](https://mlsanity.com/paper/2305.10113/) (2023)
- [Joint Verification and Refinement of Language Models for Safety-Constrained Planning](https://mlsanity.com/paper/2410.14865/) (2024)
- [Reasoning, Memorization, and Fine-Tuning Language Models for Non-Cooperative Games](https://mlsanity.com/paper/2410.14890/) (2024)
- [UNCAP: Uncertainty-Guided Neurosymbolic Planning Using Natural Language Communication for Cooperative Autonomous Vehicles](https://mlsanity.com/paper/2510.12992/) (2025)

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

- [Safe Embodied AI for Long-horizon Tasks: A Cross-layer Analysis of Robotic Manipulation](https://mlsanity.com/paper/2606.05660/) (2026)
- [Regime-Conditional Verification: Correctness Estimation for Adapting and Monitoring Safety Classifiers](https://mlsanity.com/paper/2608.14089/) (2026)

## Abstract (arXiv)

As AI systems migrate to safety-critical domains, verifying that their actions comply with well-defined rules remains a challenge. Formal methods provide provable guarantees but demand hand-crafted temporal-logic specifications, offering limited expressiveness and accessibility. Deep learning approaches enable evaluation of plans against natural-language constraints, yet their opaque decision process invites misclassifications with potentially severe consequences. We introduce RepV, a neurosymbolic verifier that unifies both views by learning a latent space where safe and unsafe plans are linearly separable. Starting from a modest seed set of plans labeled by an off-the-shelf model checker, RepV trains a lightweight projector that embeds each plan, together with a language model-generated rationale, into a low-dimensional space; a frozen linear boundary then verifies compliance for unseen natural-language rules in a single forward pass. Beyond binary classification, RepV provides a probabilistic guarantee on the likelihood of correct verification based on its position in the latent space. This guarantee enables a guarantee-driven refinement of the planner, improving rule compliance without human annotations. Empirical evaluations show that RepV improves compliance prediction accuracy by up to 15% compared to baseline methods while adding fewer than 0.2M parameters. Furthermore, our refinement framework outperforms ordinary fine-tuning baselines across various planning domains. These results show that safety-separable latent spaces offer a scalable, plug-and-play primitive for reliable neurosymbolic plan verification. Code and data are available at: https://repv-project.github.io/.