复杂系统的神经证明：声音验证与控制
系统与控制
2025-12-23 v1 人工智能
机器学习
计算机科学中的逻辑
系统与控制
摘要
本篇非正式论文呈现正在进行的研究线索，致力于构建针对复杂随机动力系统模型、响应式程序以及更广泛的Cyber-物理系统模型的形式化验证与控制的新方法。神经证明由两个关键组件构成：1）证明规则编码验证一般时序规范的要求；2）证书用于 discharge 这些规则，即通过归纳（循环、重复）方法从证明规则中构建；这种归纳方法涉及：2a）访问模型动力学的样本并据此训练神经网络，同时2b）通过SAT-模theory（SMT）查询对网络进行泛化，充分利用模型的知识。在复杂随机模型上的序列决策问题中，可以额外生成 provably-correct 的策略/策略/控制器，即状态反馈函数，与神经证书共同正式达到模型感兴趣的规范。
关键词
引用
@article{arxiv.2512.18389,
title = {Neural Proofs for Sound Verification and Control of Complex Systems},
author = {Alessandro Abate},
journal= {arXiv preprint arXiv:2512.18389},
year = {2025}
}