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. 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, 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.

翻译：形式化验证神经符号化的网络-物理系统（如无人机、医疗设备和机器人）具有复杂性。神经网络组件必须针对可用数据和安全性规范进行优化训练，并通过专用求解器进行验证；系统“网络”和“物理”行为的符号模型需在交互式定理证明器中构建与验证，这通常需要依赖成熟的数学库来推理离散与连续动力学的相互作用，并尽可能获取无限时域安全保证。最终，需要将这两项具有挑战性的验证任务以连贯一致的方式整合为单一证明，同时保持所生成模型的可部署性。本文提出一种用于构建此类证明的组合式方法论。Vehicle框架提供了一种用于描述、训练和验证神经网络组件的函数式领域特定语言。我们扩展了Vehicle以支持以最小工作量与任意交互式定理证明器集成。首先，我们描述如何重用Vehicle的标准双向类型检查器，将神经规范转译为目标多个定理证明器的中间表示。其次，我们将Vehicle与Rocq、Isabelle/HOL、Agda及工业级证明器Imandra集成，并在每个交互式定理证明器中展示了带神经网络控制器的离散网络-物理系统的通用无限时域安全证明。最后，我们利用Rocq中的数学组件库验证了带神经控制器的连续网络-物理系统（医疗设备模型）的无限时域安全性。据我们所知，这是通用型交互式定理证明器中首次实现此类结果，且该成果的可行性完全得益于Vehicle函数式接口所提供的组合性。