一句话：提出 Vehicle 的组合式方法，将神经网络验证与符号证明集成到任意交互式定理证明器中。
神经符号信息物理系统（无人机、医疗设备、机器人）的形式验证十分困难：神经组件需在数据与安全规范下训练并用专用求解器验证；符号的“信息”与“物理”行为需在交互式定理证明器（ITP）中建模验证，常依赖成熟数学库处理离散与连续动态，并希望获得无限时间范围保证；两类结果还需一致整合且保持可部署。本文提出组合式方法：Vehicle 是用于指定、训练和验证神经组件的函数式 DSL，作者扩展它以极小代价与任意 ITP 集成。通过复用其标准双向类型检查器，将神经规范转译为面向多证明器的中间表示，集成 Rocq、Isabelle/HOL、Agda 和 Imandra，展示带神经网络控制器的离散 CPS 的通用无限时间范围安全证明。最后在 Rocq 中用 Mathematical Components 库验证了建模为连续 CPS 的神经控制器医疗设备的无限时间范围安全性。据作者所知，这是通用 ITP 中首个此类结果。
Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the "cyber" and "physical" behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model. In this paper we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort, thereby bridging the gap between the neural and symbolic proofs. First, we describe how Vehicle’s standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, to put the idea of compositional neural-cyber-physical system verification to the test, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle's functional interface.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2605-02790,
title = {Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice},
author = {Matthew L. Daggitt and Ekaterina Komendantskaya and Alistair Sirman and Alessandro Bruni and Samuel Teuber and Josh Smart and Grant Passmore},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828680}
}