让AI计划的安全部分与危险部分在空间中可线性分离,实现高效可靠验证。
RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verification
- 构建可安全分离的低维潜在空间,用线性边界判断计划是否合规。
- 相比基线方法,合规预测准确率提升最高15%,参数增量少于0.2M。
- 无需人工标注即可自适应优化规划器,适合高安全性场景应用。
随着AI系统进入安全关键领域,确保其行为符合明确规则仍是一大挑战。形式化方法虽能提供可证明的保障,但需手工编写时序逻辑规范,表达能力有限且难普及。深度学习方法可评估计划对自然语言规则的符合性,但决策过程不透明,易导致严重误判。本文提出RepV,一种神经符号验证框架,通过学习一个潜在空间,使安全与不安全计划在其中线性可分。从少量由现成模型检查器标记的计划种子集出发,RepV训练一个轻量级投影器,将每个计划及其语言模型生成的解释理由嵌入低维空间;随后通过固定线性边界,在一次前向传播中验证未见自然语言规则的合规性。除二分类外,RepV还基于潜在空间中的位置提供正确验证的概率保证,支持保障驱动的规划器优化,提升规则符合性而无需人工标注。实验表明,与基线方法相比,RepV在合规预测准确率上提升最高达15%,新增参数少于0.2M;其优化框架在多个规划领域均优于普通微调基线。结果表明,安全可分离的潜在空间为可靠的神经符号计划验证提供了可扩展、即插即用的通用范式。代码与数据见:https://repv-project.github.io/。
原文摘要 · Abstract (English)
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/.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。