Towards Verified Artificial Intelligence

1 Introduction

• AI-based systems’ growing societal impact brings risks including software errors, cyber-attacks, and safety concerns, motivating verification and validation.The paper defines Verified AI as the goal of designing such systems with strong, ideally provable, assurances of correctness against mathematically specified requirements.Source: §1 · p. 1
• Formal methods offer a proof-centered starting point: specify requirements, design systems to meet proof obligations, and verify them through algorithmic proof search.The paper notes a spectrum from specification-driven testing and simulation to model checking and theorem proving.Source: §1 · p. 1
• The paper reviews formal methods’ traditional use, analyzes challenges for AI-based systems, and proposes ideas to overcome them, without covering all assurance techniques.Its challenges are intended to apply broadly across AI/ML rather than only to DNNs or RL, and are shaped largely by autonomous and semi-autonomous systems.Source: §1 · pp. 1–2

2 Background and Illustrative Example

• Formal verification checks whether a system model S satisfies property Φ in environment E, returning YES or NO and typically providing a counterexample for NO.Some tools also provide a proof or certificate with YES.Source: §2 · p. 2, Figure 1 · p. 2
• Formal methods broadly include techniques using formal specification, verification, or synthesis, including simulation-based hardware verification and model-based software testing.Source: §2 · p. 2
• Applying formal verification to AI-based systems requires representable system, environment, and property models, ideally with efficient decision procedures, but constructing them and handling complexity are challenging.Source: §2 · p. 2
• The illustrative AEBS is a closed-loop cyber-physical system combining a controller, vehicle plant, camera sensor, and deep-neural-network perception component with the vehicle’s environment.The controller uses ego-vehicle velocity and obstacle distance to regulate acceleration and braking.Source: §2 · pp. 2–3, Figure 2 · p. 3
• Its informal safety requirement is to maintain a safe distance between the moving ego vehicle and other agents or objects on the road, with specification, modeling, and verification nuances.The environment includes other vehicles, pedestrians, road objects, and potentially a driver inside the vehicle.Source: §2 · p. 3

3.1 Environment Modeling

• AI systems operate in complex, uncertain environments, making realistic models difficult to construct for verification or synthesis.Challenges include unknown environment variables, limited knowledge of agent behavior, difficult sensor modeling, and choosing an appropriate fidelity; learned probabilistic and human-behavior models must represent uncertainty and support guarantees about prediction accuracy and convergence.Source: §3.1 · pp. 3–4

3.2 Formal Specification

• AI systems need effective methods to specify desired and undesired properties despite challenges in formalizing tasks, combining quantitative and Boolean requirements, and connecting data to formal requirements.Perception and language tasks may resist precise definitions; requirements can include multiple objectives, tradeoffs, robustness, and fairness, while labeled data is often treated as the specification.Source: §3.2 · pp. 4–5

3.3 Modeling Learning Systems

• Learning systems challenge modeling through high-dimensional hybrid inputs and parameter spaces, online adaptation, and the need to model components in context.The paper notes DNNs with up to 60 million parameters and says verification must either account for future behavioral changes or proceed incrementally and online as systems evolve.Source: §3.3 · p. 5

3.4 Efficient and Scalable Design and Verification of Models and Data

• Scalable AI design and verification requires new computational engines and techniques for data generation, quantitative verification, and compositional reasoning.Data generation must address realism, distributional constraints, size, and diversity; verification must handle hybrid systems, probabilistic agents, and quantitative requirements; compositional methods need contracts and approaches that do not depend on complete component specifications.Source: §3.4 · pp. 5–6

3.5 Correct-by-Construction Intelligent Systems

• Correct-by-construction AI requires specification-driven ML design, theories for composing learning and non-learning components, and effective connections between design-time and run-time resilience.The paper notes that unconditional safe operation may not be provable in every situation, so fault tolerance and error resilience at run time remain crucial.Source: §3.5 · pp. 6–7

4.1 Environment Modeling: Introspection, Probabilities, and Data

• Model environments through introspective assumptions, active data-driven human models, and probabilistic formalisms that represent uncertainty alongside nondeterministic behavior.Introspective methods should identify monitorable assumptions sufficient for specification satisfaction, while human models should capture intent through expert-defined features, offline learning, and runtime updating.Source: §4.1 · pp. 7–8

4.2 End-to-End Specifications, Hybrid Specifications, and Specification Mining

• Specify end-to-end system behavior, combine Boolean and quantitative specifications, and mine specifications from behavior to bridge formal properties and data.System-level constraints can provide partial specifications for perception components; mined properties need not be exact or human-readable.Source: §4.2 · pp. 8–9

4.3 System Modeling: Abstractions, Explanations, and Semantic Feature Spaces

• Develop abstractions, formal-methods-compatible explanations, and semantic feature spaces to make learning systems more tractable to verify and analyze.Semantic spaces represent meaningful environmental factors rather than raw inputs, and a renderer maps them to concrete inputs for goal-directed search.Source: §4.3 · pp. 9–10

4.4 Compositional and Quantitative Methods for Design and Verification of Models and Data

• Create randomized formal methods for constrained data generation, extend quantitative verification over semantic spaces, and develop compositional reasoning for scalable analysis.Control improvisation combines legal-input, realism, and output-distribution constraints; compositional methods can use probabilistic assume-guarantee reasoning, synthesized contracts, and system-derived component constraints.Source: §4.4 · pp. 10–11

4.5 Formal Inductive Synthesis, Safe Learning, and Run-Time Assurance

• Combine formal inductive synthesis and safe learning-by-design with run-time assurance because verification and environment modeling often require restrictive assumptions.Oracle-guided synthesis can use counterexamples; safe learning includes precomputed safety envelopes, while run-time assurance pairs unverified modules with verified backups and mitigation, though monitor synthesis remains largely unsolved.Source: §4.5 · p. 11

• The paper identifies five challenges for applying formal methods to AI-based systems and corresponding design and verification principles.Source: §5 · p. 12
• Since the paper’s original 2016 publication, researchers have developed VerifAI and Scenic, open-source tools implementing the proposed principles.Source: §5 · p. 12
• VerifAI and Scenic have been applied to industrial-scale systems in autonomous driving [33] and aerospace [30], while much remains to be done.Source: §5 · p. 12