ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems

TL;DR

ScenicProver is a comprehensive framework for the compositional probabilistic verification of learning-enabled cyber-physical systems, integrating formal proofs, testing, and assurance case generation to handle complex real-world environments.

Contribution

It introduces a novel framework that combines compositional system description, assume-guarantee contracts, evidence generation, and assurance case creation for verifying learning-enabled CPS.

Findings

Stronger probabilistic guarantees achieved compared to monolithic testing.

Effective verification demonstrated on autonomous vehicle emergency braking system.

Leverages manufacturer sensor guarantees to focus testing on uncertain conditions.

Abstract

Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces ScenicProver, a verification framework that aims to fill this gap. Built upon the Scenic probabilistic programming language, the framework supports: (1) compositional system description with clear component interfaces, ranging from interpretable code to black boxes; (2) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (3) evidence generation through testing, formal proofs via Lean 4 integration, and importing external assumptions; (4) systematic combination of generated evidence using contract operators; and (5) automatic generation of assurance cases tracking the provenance of system-level guarantees. We demonstrate the framework's effectiveness through a case study on an autonomous vehicle's automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for radar and laser sensors and focusing testing efforts on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.