Toward Verified Artificial Intelligence

2 min read

A position paper on what formal verification of AI-based systems would take. The authors frame verification as checking a system model S in an environment model E against a property Φ, then name five challenges (modelling the environment, writing formal specifications, modelling learned components, scaling design and verification over data and models, correct-by-construction design) and one principle for each. The CACM article is the 2022 version of an arXiv paper first posted in 2016; I read the arXiv version from 2020.

Findings

  • Environment modelling is the hardest part: in an urban traffic scene even the number of agents is unknown. Their answer is introspective environment modelling, where the design process extracts the weakest assumptions about the environment that guarantee Φ and monitors them at run time.
  • Specifications should start at the system level and use hybrid Boolean and quantitative formalisms (they point to STL robustness) because perception components rarely have crisp specs.
  • Because verification is undecidable in most cases and environments cannot be fully modelled, design-time proofs must be paired with run-time assurance. Simplex and SOTER-style wrappers are their examples.
  • The authors call extracting environment assumptions into monitors, and choosing what to do when a monitor fires, “a largely unsolved problem”.
  • Tools that came out of this agenda: VerifAI and the Scenic scenario language, applied in autonomous driving and aerospace.

Limits

  • A roadmap, with no new theorem or experiment. Progress claims point to the authors’ own tools.
  • Little on adversaries. A component that lies on purpose is a different environment model from one that is noisy.

Relevance

Seshia et al. give the reason runtime monitors exist: you cannot prove the robot correct in a world you cannot model, so you monitor the assumptions instead. The open part, deciding what to do after the monitor fires, is the failure recovery problem. See runtime monitoring, foundation models for robotics and robust robotics.