Bensalem, Saddek, Huang, Xiaowei 
ORCID: 0000-0001-6267-0366, Ruan, Wenjie, Tang, Qiyi, Wu, Changshun and Zhao, Xingyu ORCID: 0000-0002-3474-349X
(2024)
Bridging formal methods and machine learning with model checking and global optimisation.
Journal of Logical and Algebraic Methods in Programming, 137.
p. 100941.
Abstract
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 MLS2 properties, 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.
| Item Type: | Article |
|---|---|
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 19 Jan 2024 11:32 |
| Last Modified: | 30 Jan 2024 10:57 |
| DOI: | 10.1016/j.jlamp.2023.100941 |
| Open Access URL: | https://doi.org/10.1016/j.jlamp.2023.100941 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3177914 |
Dimensions
Dimensions
