ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
This addresses the problem of verifying complex learning-enabled systems for researchers and engineers in cyber-physical systems, offering a novel framework but with incremental improvements over existing tools.
The paper tackles the intractable verification of learning-enabled cyber-physical systems by introducing ScenicProver, a framework for compositional probabilistic verification, and demonstrates its effectiveness in a case study on an autonomous vehicle's emergency braking system, enabling stronger probabilistic guarantees than monolithic testing with the same computational budget.
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.