Towards Verified AI

 Considerable, complex piece. .... 

Toward Verified Artificial Intelligence   By Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry

Communications of the ACM, July 2022, Vol. 65 No. 7, Pages 46-55      10.1145/3503914

Artificial intelligence (AI) is a term used for computational systems that attempt to mimic aspects of human intelligence, including functions we intuitively associate with intelligence, such as learning, problem solving, and thinking and acting rationally—for example, see Russell and Norvig.26 We interpret the term AI broadly to include closely related areas such as machine learning (ML). Systems that heavily use AI, henceforth referred to as AI systems, have had a significant societal impact in domains that include healthcare, transportation, finance, social networking, e-commerce, and education.

CONTRIBUTED ARTICLES

Toward Verified Artificial Intelligence

By Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry

Communications of the ACM, July 2022, Vol. 65 No. 7, Pages 46-55    10.1145/3503914

This growing societal-scale impact has brought with it a set of risks and concerns, including errors in AI software, cyber-attacks, and AI system safety.4 Therefore, the question of verification and validation of AI systems, and, more broadly, of achieving trustworthy AI,39 has begun to demand the attention of the research community. We define "verified AI" as the goal of designing AI systems that have strong, ideally provable, assurances of correctness with respect to mathematically specified requirements. How can we achieve this goal?

In this article, we consider the challenge of verified AI from the perspective of formal methods, a field of computer science and engineering concerned with the rigorous mathematical specification, design, and verification of systems.38 At its core, formal methods is about proof: formulating specifications that form proof obligations; designing systems to meet those obligations; and verifying, via algorithmic proof search, that the systems indeed meet their specifications. A spectrum of formal methods, from specification-driven testing and simulation to model checking and theorem proving, are routinely used in the computer-aided design of integrated circuits (ICs) and have been widely applied to find bugs in software, analyze cyber-physical systems (CPS), and find security vulnerabilities. We review the way formal methods has traditionally been applied, identify the unique challenges arising in AI systems, and present ideas and recent advances towards overcoming these challenges.   .... '