用神经网络生成可证明的验证证书，确保复杂系统控制的安全性。
Neural Proofs for Sound Verification and Control of Complex Systems
- 通过神经网络与SMT结合，递归生成可验证的控制证书。
- 在随机动力系统中，可生成满足时序规范的正确策略。
- 适合需要形式化安全保证的自动驾驶、工业控制场景。
本文介绍一项持续研究，旨在为复杂随机动力系统、反应式程序及更一般的网络物理系统模型，构建可靠的正式验证与控制方法。神经证明由两个核心部分构成：1）证明规则编码了需验证的通用时序规范；2）证书用于释放这些规则，即通过从模型动态中采样并训练神经网络，再利用SMT求解器结合模型知识进行泛化。在复杂随机模型的顺序决策问题中，可进一步生成可证明正确的策略/控制律（即状态反馈函数），与神经证书协同，形式化满足目标模型的指定规范。
原文摘要 · Abstract (English)
This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。