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

TL;DR

RepV introduces a neurosymbolic verification method that learns a latent space for plans, enabling scalable, accurate, and probabilistic safety verification of AI plans against natural-language rules, with iterative refinement capabilities.

Contribution

It presents RepV, a novel latent space approach that unifies deep learning and formal verification for scalable, probabilistic plan safety assessment using minimal labeled data.

Findings

Improves compliance prediction accuracy by up to 15%.

Adds fewer than 0.2 million parameters.

Outperforms baseline refinement methods.

Abstract

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/.