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

• URL: http://arxiv.org/abs/2511.02164v1
• Date: Tue, 04 Nov 2025 01:09:08 GMT
• Title: ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
• Authors: Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont,
• Abstract summary: This paper introduces ScenicProver, a verification framework for learning-enabled cyber-physical systems.<n>It supports compositional system description with clear component interfaces, ranging from interpretable code to black boxes.<n>We demonstrate the framework's effectiveness through a case study on an autonomous vehicle's emergency braking system with sensor fusion.
• Score: 3.4880795442123733
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Composable Attestation: A Generalized Framework for Continuous and Incremental Trust in AI-Driven Distributed Systems [4.2822349607372265]
  This paper presents composable attestation as a generalized cryptographic framework for Continuous and Incremental Trust in Distributed Systems.<n>We establish a rigorous mathematical foundation which is defining core properties of such attestation systems.<n>The framework's utility extends to applications such as secure AI model integrity verification, federated learning, and runtime trust assurance.
  arXiv  Detail & Related papers  (2026-03-02T22:45:26Z)
• LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [0.8574682463936006]
  Traditional formal verification tools fall short when faced with systems that embed both opaque black-box AI components and complex dynamics.<n>We introduce LUCID, a verification engine for certifying safety of black-box embedding dynamical systems.<n> LUCID is the first known tool capable of establishing quantified safety guarantees for such systems.
  arXiv  Detail & Related papers  (2025-12-12T17:46:50Z)
• Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis [49.31947916567367]
  Hamilton-Jacobi (J) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable under worst-case uncertainties.<n>This work is the first HJ-based reachability-based system verification framework for the Robust Verification Controllers via HJ rover.<n>Within Ro-CoRe, we propose novel methods for safety verification and controller design.
  arXiv  Detail & Related papers  (2025-11-18T18:55:20Z)
• BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
  We introduce an LLM-based agentic framework for barrier certificate synthesis.<n>The framework uses natural language reasoning to propose, refine, and validate candidate certificates.<n> BarrierBench is a benchmark of 100 dynamical systems spanning linear, nonlinear, discrete-time, and continuous-time settings.
  arXiv  Detail & Related papers  (2025-11-12T14:23:49Z)
• DSperse: A Framework for Targeted Verification in Zero-Knowledge Machine Learning [0.0]
  DSperse is a framework for distributed machine learning inference with cryptographic verification.<n>We evaluate DSperse using multiple proving systems and report empirical results on memory usage, runtime, and circuit behavior.
  arXiv  Detail & Related papers  (2025-08-09T12:38:18Z)
• BlueGlass: A Framework for Composite AI Safety [0.2999888908665658]
  This paper introduces BlueGlass, a framework designed to facilitate AI safety by providing a unified infrastructure.<n>To demonstrate the utility of this framework, we present three safety-oriented analyses on vision-language evaluation.<n>More broadly, this work contributes infrastructure and findings for building more robust and reliable AI systems.
  arXiv  Detail & Related papers  (2025-07-14T09:45:34Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• A Hybrid Framework for Statistical Feature Selection and Image-Based Noise-Defect Detection [55.2480439325792]
  This paper presents a hybrid framework that integrates both statistical feature selection and classification techniques to improve defect detection accuracy.<n>We present around 55 distinguished features that are extracted from industrial images, which are then analyzed using statistical methods.<n>By integrating these methods with flexible machine learning applications, the proposed framework improves detection accuracy and reduces false positives and misclassifications.
  arXiv  Detail & Related papers  (2024-12-11T22:12:21Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• A Verification Framework for Certifying Learning-Based Safety-Critical Aviation Systems [6.168537302126847]
  We present a safety verification framework for design-time and run-time assurance of learning-based components in aviation systems. From the design-time assurance perspective, we propose offline mixed-fidelity verification tools that incorporate knowledge from different levels of granularity in simulated environments. From the run-time assurance perspective, we propose reachability- and statistics-based online monitoring and safety guards for a learning-based decision-making model.
  arXiv  Detail & Related papers  (2022-05-09T22:56:00Z)
• Learning Hybrid Control Barrier Functions from Data [66.37785052099423]
  Motivated by the lack of systematic tools to obtain safe control laws for hybrid systems, we propose an optimization-based framework for learning certifiably safe control laws from data. In particular, we assume a setting in which the system dynamics are known and in which data exhibiting safe system behavior is available.
  arXiv  Detail & Related papers  (2020-11-08T23:55:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.