Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Verified Artificial Intelligence

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

TL;DR

The paper argues that verifiable AI requires integrating formal methods with AI/ML systems by identifying five core challenges—environment modeling, specification, learning-system modeling, scalable design/verification, and correct-by-construction design—and proposing five corresponding principles. It advocates end-to-end system specifications, hybrid quantitative-Boolean formalisms, introspective and probabilistic environment models, abstractions and semantic feature spaces, and a combination of formal inductive synthesis with run-time assurance. The approach emphasizes data-driven modeling, specification mining, and compositional reasoning to scale verification to complex AI-enabled systems, with practical progress showcased via open-source tools and industrial domains. Overall, it outlines a concrete research agenda to achieve Verified AI by blending design-time guarantees with run-time safeguards.

Abstract

Verified artificial intelligence (AI) is the goal of designing AI-based systems that that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements. This paper considers Verified AI from a formal methods perspective. We describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges.

Towards Verified Artificial Intelligence

TL;DR

The paper argues that verifiable AI requires integrating formal methods with AI/ML systems by identifying five core challenges—environment modeling, specification, learning-system modeling, scalable design/verification, and correct-by-construction design—and proposing five corresponding principles. It advocates end-to-end system specifications, hybrid quantitative-Boolean formalisms, introspective and probabilistic environment models, abstractions and semantic feature spaces, and a combination of formal inductive synthesis with run-time assurance. The approach emphasizes data-driven modeling, specification mining, and compositional reasoning to scale verification to complex AI-enabled systems, with practical progress showcased via open-source tools and industrial domains. Overall, it outlines a concrete research agenda to achieve Verified AI by blending design-time guarantees with run-time safeguards.

Abstract

Verified artificial intelligence (AI) is the goal of designing AI-based systems that that have strong, ideally provable, assurances of correctness with respect to mathematically-specified requirements. This paper considers Verified AI from a formal methods perspective. We describe five challenges for achieving Verified AI, and five corresponding principles for addressing these challenges.

Paper Structure

This paper contains 15 sections, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background and Illustrative Example
  3. Challenges for Verified AI
  4. Environment Modeling
  5. Formal Specification
  6. Modeling Learning Systems
  7. Efficient and Scalable Design and Verification of Models and Data
  8. Correct-by-Construction Intelligent Systems
  9. Principles for Verified AI
  10. Environment Modeling: Introspection, Probabilities, and Data
  11. End-to-End Specifications, Hybrid Specifications, and Specification Mining
  12. System Modeling: Abstractions, Explanations, and Semantic Feature Spaces
  13. Compositional and Quantitative Methods for Design and Verification of Models and Data
  14. Formal Inductive Synthesis, Safe Learning, and Run-Time Assurance
  15. Conclusion

Figures (2)

  • Figure 1: Formal verification procedure.
  • Figure 2: Example of closed-loop cyber-physical system with machine learning components (introduced in dreossi-nfm17).