Source-linked AI summary
Towards Verified Artificial Intelligence
Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry
TL;DR
AI-based systems increasingly affect society while raising concerns about software errors, cyber-attacks, and safety, motivating Verified AI. The paper examines this goal through formal methods, identifies five challenges, and proposes corresponding principles, supported by authors’ experience applying them.
Problem
AI-based systems have broad societal impact and associated risks, but achieving strong, ideally provable assurances against mathematically specified requirements remains challenging.
Method
The paper reviews formal-methods practice for AI-based systems, analyzes five challenges, and proposes principles including abstraction, inductive synthesis, safe learning, and run-time assurance.
Results
The authors report that their principles have been successfully applied and provide a good starting point for applying formal methods to AI-based systems.
Takeaways & Limitations
The proposed principles point a way toward the goal of Verified AI while complementing other perspectives on the problem.
Takeaways & Limitations
The discussion focuses on formal methods and is shaped largely by autonomous and semi-autonomous systems, rather than covering all assurance techniques or AI settings.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper frames Verified AI as achieving strong, ideally provable assurances that AI-based systems satisfy mathematically specified requirements. It examines this goal through formal methods, emphasizing broad applicability beyond particular AI technologies.
- Verified AI seeks strong, ideally provable assurances that AI-based systems satisfy mathematically specified requirements.
- The paper reviews traditional formal-methods applications, analyzes their challenges for AI-based systems, and proposes ideas to address them.
- Its discussion focuses on formal methods rather than the broader set of techniques that could improve assurance in AI-based systems.
- The identified challenges target a broad range of AI and machine-learning systems, not only deep neural networks or reinforcement-learning systems.
2 Background and Illustrative Example
Formal verification takes system, environment, and property models as inputs and returns whether the system satisfies the property, often with explanatory evidence. The paper illustrates these ideas using a semi-autonomous driving system.
- A formal verification procedure takes a system model S, an environment model E, and a property Φ as inputs.
- The verifier returns YES or NO on whether S satisfies Φ in E; NO may include a counterexample, while YES may include a correctness certificate.
- The paper adopts a broad view of formal methods that includes formal specification, verification, synthesis, and specification-guided simulation or testing.
- Applying formal verification requires representing S, E, and Φ in formalisms with ideally efficient decision procedures, but constructing these representations is difficult.
- The illustrative example is a closed-loop cyber-physical system for semi-autonomous driving, centered on an automated emergency braking system with machine-learning perception.
- The example’s safety requirement concerns maintaining a safe distance between the moving ego vehicle and other road agents or objects.
3 Challenges for Verified AI
The paper identifies five challenges for formally verifying AI-based systems: modeling uncertain environments, specifying desired behavior, modeling learning systems, scaling computational methods, and supporting compositional and correct-by-construction design.
- 3.1 Environment Modeling: AI-based systems operate in complex, uncertain environments where agents, variables, intentions, and behaviors may be difficult to model precisely.
- 3.1 Environment Modeling: Environment models must provide useful fidelity: purely nondeterministic over-approximations can create too many spurious bug reports, while some systems require probabilistic assumptions.
- 3.2 Formal Specification: Formal specifications are difficult for perception and other AI tasks, and must address Boolean, quantitative, robustness, fairness, and data-based requirements.
- 3.3 Modeling Learning Systems: Learning systems create verification challenges through very high-dimensional inputs and parameter or state spaces, plus online adaptation and evolution.
- 3.4 Efficient and Scalable Design and Verification of Models and Data: AI/ML verification requires advances in computational engines for efficient and scalable training, testing, design, and verification.
- 3.4 Efficient and Scalable Design and Verification of Models and Data: Formal data generation must produce realistic, distributionally constrained, selective ensembles that support dataset size, diversity, training, and generalization objectives.
- 3.4 Efficient and Scalable Design and Verification of Models and Data: Compositional reasoning is difficult when perception components lack complete formal specifications, motivating techniques that do not depend on them.
- 3.4 Efficient and Scalable Design and Verification of Models and Data: Correct-by-construction AI design spans dataset creation, model-structure synthesis, feature generation, hyper-parameter selection, debugging, and overall compositional design.
4 Principles for Verified AI
The paper proposes five principles for addressing Verified AI challenges through formal-methods-based design and verification. These principles span environment modeling, specifications, ML abstractions, randomized quantitative methods, and correct-by-construction learning systems.
- The five principles correspond to five Verified AI challenges and guide the design and verification process.Table 1 summarizes these challenge–principle pairings.
- Environment modeling: Environment modeling should be introspective, data-driven, and probabilistic, identifying monitorable assumptions sufficient to guarantee specifications.The assumptions should ideally be weakest, efficiently generated and monitored, and potentially translatable into human-understandable explanations.
- Specifications: AI-based systems should combine end-to-end specifications with hybrid Boolean-quantitative formalisms and specification mining to bridge data and properties.Boolean formalisms aid composition, while quantitative semantics support optimization and finer-grained satisfaction.
- ML components: ML components require automated abstractions, explanations, and semantic analysis techniques to make formal reasoning more tractable.Searching lower-dimensional semantic feature spaces can simplify analysis when suitable renderers map semantic points to concrete features.
- Data, testing, and verification: Formal methods for data generation, testing, and verification should be compositional, randomized, and quantitative.Control improvisation generates examples satisfying hard legality constraints, soft similarity constraints, and output-distribution requirements.
- Correct-by-construction design: AI-based systems should use formal inductive synthesis and safe-learning design supported by run-time assurance.Formal inductive synthesis generates models or classifiers from examples while requiring them to satisfy formal specifications.
- The authors report that applying these principles provides a good starting point for formal methods in AI-based systems.They characterize the principles as promising rather than a complete solution, noting that substantial further work remains.
5 Conclusion
The paper analyzes Verified AI from a formal methods perspective, identifies five challenges, and proposes corresponding design and verification principles. Subsequent work produced VerifAI and Scenic, which were applied to industrial-scale autonomous-driving and aerospace systems, while the authors emphasize that much remains to be done.
- The paper identifies five main challenges for applying formal methods to AI-based systems and proposes corresponding principles for design and verification.The authors summarize these challenges and principles in Table 1.
- Open-source tools VerifAI and Scenic implement techniques based on the proposed principles and have been applied to industrial-scale autonomous-driving and aerospace systems.
- The reported results are an initial step, and much more work remains for Verified AI.