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.

翻译：本文作为一项非正式贡献，介绍了一个正在进行的研究方向，该方向致力于为动态系统、反应式程序以及更广泛的网络物理系统模型的复杂随机模型，构建一种新的可靠证明方法以实现形式化验证与控制。神经证明由两个关键组成部分构成：1）证明规则编码了确保对目标模型进行通用时序规约验证所需的条件；2）用于解除这些规则的证书，即通过归纳（即循环、重复）方法从所述证明规则构建而成；这种归纳方法包括：2a）从模型动态中获取样本并据此训练神经网络，同时2b）通过可满足性模理论（SMT）查询来泛化这些网络，该查询充分利用了模型的完整知识。在复杂随机模型上的序贯决策问题背景下，该方法还能额外生成可证明正确的策略/控制器，即状态反馈函数，这些函数与神经证书相结合，能够形式化地实现针对目标模型的给定规约。