ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont
TL;DR
The paper tackles the challenge of verifying learning-enabled CPS where black-box components interact with complex real-world environments, which makes monolithic formal proofs intractable. It proposes ScenicProver, a framework built on the Scenic probabilistic programming language that supports: (i) compositional system descriptions with clear component interfaces, (ii) assume-guarantee contracts expressed as $C=(\mathcal{A},\mathcal{G})$ in an extension of Linear Temporal Logic $LTLfMT$, (iii) evidence generation from testing, Lean 4 proofs, and external assumptions, (iv) contract-evidence combination via operators, and (v) automatic generation of assurance cases showing provenance. In a case study on autonomous emergency braking with sensor fusion, leveraging manufacturer guarantees for radar and laser sensors and testing under uncertain conditions yields stronger probabilistic guarantees than monolithic testing for the same computational budget. The work demonstrates improved verification efficiency and traceable, scalable assurance for LE-CPS, with potential to inform standards in automotive safety and related domains.
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.