Bridging formal methods and machine learning with model checking and global optimisation
Bridging formal methods and machine learning with model checking and global optimisation
复制标题
DOI：
10.1016/j.jlamp.2023.100941
复制
发表时间：
2024-02
期刊：
影响因子：
--
通讯作者：
S. Bensalem;Xiaowei Huang;Wenjie Ruan;Qiyi Tang;Changshun Wu;Xingyu Zhao
中科院分区：
文献类型：
--
作者：
S. Bensalem;Xiaowei Huang;Wenjie Ruan;Qiyi Tang;Changshun Wu;Xingyu Zhao
形式化方法和机器学习是两个基础和理念截然不同的研究领域。形式化方法利用数学上严格的技术来进行软件和硬件系统的规范、开发和验证。机器学习侧重于通过观察训练数据集逐步改进参数化模型的实用方法。虽然历史上这两个领域缺乏交流，但随着对神经网络鲁棒性验证的研究兴趣的爆发，这种趋势在过去几年中发生了变化。本文将简要回顾这些工作，并重点关注两个领域之间迫切需要更广泛、更深入的交流，最终目标是开发具有优异性能和可接受的安全性的学习支持系统。我们提出了一种规范语言 MLS2，并证明它可以表达一组已知的安全属性，包括泛化、不确定性、鲁棒性、数据中毒、后门、模型窃取、成员推理、模型反转、可解释性和公平性。为了验证 MLS2 属性，我们推广了基于全局优化的方法，该方法可以保证收敛到最优解。其中许多对于当前解决方案和最优解决方案之间的差距存在理论界限。
Formal methods and machine learning are two research fields with drastically different foundations and philosophies. Formal methods utilise mathematically rigorous techniques for software and hardware systems' specification, development and verification. Machine learning focuses on pragmatic approaches to gradually improve a parameterised model by observing a training data set. While historically, the two fields lack communication, this trend has changed in the past few years with an outburst of research interest in the robustness verification of neural networks. This paper will briefly review these works, and focus on the urgent need for broader and more in-depth communication between the two fields, with the ultimate goal of developing learning-enabled systems with excellent performance and acceptable safety and security. We present a specification language, MLS2, and show that it can express a set of known safety and security properties, including generalisation, uncertainty, robustness, data poisoning, backdoor, model stealing, membership inference, model inversion, interpretability, and fairness. To verify MLS2properties, we promote the global optimisation-based methods, which have provable guarantees on the convergence to the optimal solution. Many of them have theoretical bounds on the gap between current solutions and the optimal solution.