arXiv:2603.02235cs.LGcs.AI2026-03

让AI验证器理解自然语言需求,自动转成可验证的正式规范

Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

  • 用户用自然语言描述需求,系统自动转为形式化验证查询
  • 在结构化与非结构化数据上成功验证复杂语义规格
  • 保持用户意图准确性且计算开销低,适合实际应用

当前神经网络验证工具仅支持有限类别的规格,通常以原始输入输出的低层约束表达。这一局限严重阻碍其在多样化应用场景中的采纳与实用。根本原因在于深度神经网络学习的内部表示缺乏与人类可理解特征的显式映射。为此,我们向验证流程引入新组件,使现有验证工具能适用于更广泛领域和规格风格。我们的框架允许用户以自然语言表述规格,系统自动分析并转换为与前沿神经网络验证器兼容的形式化查询。我们在结构化与非结构化数据集上评估该方法,证明其成功验证了此前无法处理的复杂语义规格。结果表明,该转换过程在保持用户意图高保真度的同时,计算开销极低,显著拓展了形式化DNN验证在真实世界高层次需求中的适用性。

原文摘要 · Abstract (English)

Neural network verification tools currently support only a narrow class of specifications, typically expressed as low-level constraints over raw inputs and outputs. This limitation significantly hinders their adoption and practical applicability across diverse application domains where correctness requirements are naturally expressed at a higher semantic level. This challenge is rooted in the inherent nature of deep neural networks, which learn internal representations that lack an explicit mapping to human-understandable features. To address this, we bridge this gap by introducing a novel component to the verification pipeline, making existing verification tools applicable to a broader range of domains and specification styles. Our framework enables users to formulate specifications in natural language, which are then automatically analyzed and translated into formal verification queries compatible with state-of-the-art neural network verifiers. We evaluate our approach on both structured and unstructured datasets, demonstrating that it successfully verifies complex semantic specifications that were previously inaccessible. Our results show that this translation process maintains high fidelity to user intent while incurring low computational overhead, thereby substantially extending the applicability of formal DNN verification to real-world, high-level requirements.

神经网络验证自然语言形式化方法AI可解释性

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。