PI Mary Sheeran (10%) ms@chalmers.se
Postdoc to be hired (2 yrs at 80%, + 20% teaching)
Collaborators Alexey Voronov (RiSE Viktoria), Koen Claessen, Carl Seger, John Hughes (Chalmers)
External Advisors Erik Meijer (Facebook, Menlo Park), Dimitrios Vytiniotis (DeepMind, London)
Project start expected April-June 2019 Project end Dec 2021
It has long been known that our ability to develop and deploy machine learning (ML) algorithms outpaces our ability to make clear guarantees about their behaviour. Szegedy et al, in 2013, revealed how neural networks are susceptible to adversarial examples [SZS13]. Later, Goodfellow (an author of that paper) coauthored a series of blog posts beginning with “Breaking things is easy” [PG16], which points out that we know much more about attacking machine learning models than about defending them. In “The challenge of verification and testing of machine learning” [PG17], the authors conclude that “The verification of machine learning models is still in its infancy, because methods make assumptions that prevent them from providing absolute guarantees of the absence of adversarial examples.”
This situation is unacceptable, as ML algorithms will increasingly be deployed in safety critical systems, for example in autonomous vehicles. In addition, machine learning will increasingly be used to develop the software that is part of the infrastructure on which we rely (for communication, shopping, banking etc.).
This project aims to develop new methods of testing and verifying machine learning algorithms and to kickstart our group’s application of its expertise in testing and formal verification in the area of AI/ML.
There is promising work on which we can build. For example, Bastani et al showed how to formulate, efficiently estimate and improve the robustness of neural nets, using an encoding of the robustness property as a constraint system [BIL16]. (One of the coauthors of this paper, Dimitrios Vytiniotis, now at DeepMind, has agreed to act as an external advisor to the project.) Katz et al have taken promising first steps towards formally verifying properties of neural networks, at scale, without having to make any simplifying assumptions [KBD17]. However, much remains to be done to enable both testing and verification of the safety of machine learning algorithms. A recent survey done by RiSE Viktoria of the state of the art of testing of self-driving vehicles confirms that this project is timely, and targets the early stage of a vital research field. We plan to collaborate with Voronov, who contributed to the survey.
Investigate if new methods of testing of cyber-physical systems being developed in our VR Research Environment [SyTec,CSE18] can be adapted to work on neural networks.
Study applications in ML based Natural language translation (where errors are everywhere, and grouping them is what is needed).
Study testing and formal verification of ML based autonomous driving in collaboration with RiSE Viktoria.
Study testing in the context of machine learning based software development (see Erik Meijer’s recent talk at Chalmers; Meijer has agreed to be an advisor on the project).
The postdoc will likely concentrate on one of these application domains, depending on their background.
Concrete first steps might include
The long term goal is to develop methods to design neural networks and machine learning based software with guaranteed properties.
[SZS13] Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., & Fergus, R. (2013). Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199.
[PG16] Papernot N., & Goodfellow, I. (2016). Breaking things is easy. Blog post, Dec. 16, 2016. http://www.cleverhans.io/security/privacy/ml/2016/12/16/breaking-things-is-easy.html
[PG17] Papernot N., & Goodfellow, I (2017). The challenge of verification and testing of machine learning. Blog post, June 14 2017.
http://www.cleverhans.io/security/privacy/ml/2017/06/14/verification.html
[KBD17] Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv preprint arXiv:1702.01135.
[BIL16] O. Bastani, Y. Ioannou, L. Lampropoulos, D. Vytiniotis, A. V. Nori, A. Criminisi (2016). Measuring Neural Net Robustness with Constraints. 30th Conf. on Neural Information Processing Systems (NIPS).
[SyTec] Systematic Testing of Cyber Physical Systems, http://systematictesting.org/
Funded by Vetenskapsrådet, VR 2016-06204
[CSE18] K. Claessen, N. Smallbone, J. Eddeland, Z. Ramezani, K. Åkesson (2018). Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems.
14th IFAC Workshop on Discrete Event Systems (WODES).