提出首个概率神经符号系统鲁棒性近似验证方法，解决安全部署难题。
A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification
- 基于松弛法实现概率神经符号系统的近似验证
- 在标准基准上比求解器快数十倍，支持高维输入
- 适合自动驾驶等关键领域安全验证，可扩展性强
神经符号人工智能（NeSy AI）结合了神经网络学习与符号推理，其概率变体中，神经网络从子符号输入提取符号，再由符号组件进行概率推理以回答查询。本文针对此类系统鲁棒性的形式化验证问题，分析其计算复杂度，证明核心计算的决策版本为 $ ext{NP}^{ ext{PP}}$-完全。面对这一困难，我们首次提出基于松弛的近似验证方法。实验表明，该方法在标准 NeSy 基准上相比传统求解器实现指数级加速，并成功应用于真实自动驾驶场景，在高维输入下验证了安全性属性。
原文摘要 · Abstract (English)
Neuro-Symbolic Artificial Intelligence (NeSy AI) has emerged as a promising direction for integrating neural learning with symbolic reasoning. Typically, in the probabilistic variant of such systems, a neural network first extracts a set of symbols from sub-symbolic input, which are then used by a symbolic component to reason in a probabilistic manner towards answering a query. In this work, we address the problem of formally verifying the robustness of such NeSy probabilistic reasoning systems, therefore paving the way for their safe deployment in critical domains. We analyze the complexity of solving this problem exactly, and show that a decision version of the core computation is $\mathrm{NP}^{\mathrm{PP}}$-complete. In the face of this result, we propose the first approach for approximate, relaxation-based verification of probabilistic NeSy systems. We demonstrate experimentally on a standard NeSy benchmark that the proposed method scales exponentially better than solver-based solutions and apply our technique to a real-world autonomous driving domain, where we verify a safety property under large input dimensionalities.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。