Vehicle：为神经网络注入形式化验证能力的开源工具包

Vehicle 是一个开源工具包，旨在将逻辑规约嵌入神经网络，弥合深度学习与形式化验证之间的鸿沟。其核心是高阶函数式规约语言，支持将同一规约编译为训练损失函数、验证器查询，并导出到交互式定理证明器，实现神经网络的形式化验证。该项目由 vehicle-lang 团队维护，源码托管于 GitHub（链接：https://github.com/vehicle-lang/vehicle），发布时间为2026-05-23。它针对神经网络的"黑盒"困境，为安全关键领域（如自动驾驶、医疗诊断）的AI系统提供可信度保障。

深度学习模型在图像识别、NLP、自动驾驶等领域取得突破，但决策过程难以解释和验证。传统测试无法覆盖所有输入场景，在安全关键领域风险极高。形式化验证通过数学证明确保系统满足规约，但神经网络的非线性特性使其难以用传统逻辑框架描述，应用面临巨大挑战。

Vehicle的核心设计理念是同一规约可在神经网络生命周期多阶段复用：编译为训练损失函数引导学习、编译为验证器查询进行部署前验证、导出到定理证明器做系统级验证。其规约语言采用高阶函数式范式，支持依赖类型，能简洁表达复杂性质（如单调性约束：forall x y. x <= y => network(x) <= network(y)）。强大的类型系统可在编译期捕获错误，确保规约与网络架构兼容，相关研究发表于CPP'23会议。

Vehicle的技术实现包括三部分：1. 将规约编译为可微分损失函数，实现"规约引导学习"；2. 集成Marabou（基于SMT的神经网络验证器），可证明规约对所有输入成立或生成反例；3. 支持导出验证结果到Agda、Rocq、Isabelle等交互式定理证明器，确保神经网络作为系统组件的正确性。若网络权重变化，证明检查会失败，防止未经验证的模型部署。

Vehicle提供多个应用案例：1. ACAS Xu无人机防撞系统：复现Reluplex论文中的规约，描述复杂安全性质；2. 汽车控制器：证明在传感器噪声和侧风干扰下，控制器能保持汽车在道路行驶；3. MNIST鲁棒性验证：证明分类器在图像邻域内对微小扰动鲁棒，对抗样本攻击下分类结果不变。

Vehicle与现有深度学习生态无缝集成：模型格式支持ONNX（兼容PyTorch、TensorFlow）；数据格式支持IDX（MNIST标准格式）；验证后端采用Marabou（SMT-based验证器）；证明器接口支持Agda、Rocq、Isabelle等。

Vehicle有坚实学术基础：工具论文发表于EPTCS/FSCD 2025，类型检查器设计发表于CPP'23，编译到验证器查询的研究为arXiv 2024预印本。项目正积极开发，欢迎社区通过GitHub Issue Tracker贡献（如添加新模型格式、验证器或定理证明器支持）。未来，Vehicle将成为AI安全领域确保系统可信度的关键技术，推动可靠、可解释AI的发展。