Options
Advanced Learning and Conformal Methods for Verification and Prediction of Stochastic Systems
Cairoli, Francesca
2025
Loading...
e-ISBN
978-88-5511-663-3
Abstract
This research summary synthesises findings from recent papers at the intersection of formal methods, stochastic systems, and machine learning. The reviewed literature reveals a strong trend towards leveraging deep generative models (e.g., Diffusion models, VAEs, GANs) for tasks such as model abstraction, forecasting, and planning. A critical parallel trend is the integration of these data-driven methods with rigorous statistical guarantees, primarily through Conformal Prediction (CP) and Bayesian inference, to ensure reliability and safety. The papers are organized into four macro-topics: 1) Conformal Prediction for Runtime Verification and Monitoring, which focuses on providing efficient, statistically guaranteed predictions for temporal logic properties; 2) Scalable Bayesian Verification and Uncertainty Quantification, which addresses the challenge of scaling parametric verification to high dimensions; 3) Neuro-Symbolic and Generative Model Discovery, which explores methods to automatically learn interpretable, mechanistic models from data; and 4) Generative Abstractions and Guided Sampling, which uses generative models to create fast simulators and to steer outputs towards satisfying complex constraints. The collective findings indicate a paradigm shift from purely simulation-based analysis to a hybrid, data-driven approach that does not sacrifice formal guarantees, enabling the application of formal verification to larger, more complex systems.
Questa sintesi di ricerca sintetizza i risultati di recenti articoli sull'intersezione tra modelli formali, sistemi stocastici e modelli di apprendimento automatico. La letteratura esaminata rivela una forte tendenza a sfruttare modelli generativi profondi (ad esempio, modelli di diffusione, VAE, GAN) per attività quali l'astrazione, la previsione e la pianificazione di modelli. Una tendenza parallela critica è l'integrazione di questi metodi basati sui dati con rigorose garanzie statistiche, principalmente attraverso la previsione conforme (CP) e l'inferenza bayesiana, per garantire affidabilità e sicurezza. Gli articoli sono organizzati in quattro macro-argomenti: 1) Previsione conforme per la verifica e il monitoraggio in fase di esecuzione, che si concentra sulla fornitura di previsioni efficienti e statisticamente garantite per le proprietà logiche temporali; 2) Verifica bayesiana scalabile e quantificazione dell'incertezza, che affronta la sfida di scalare la verifica parametrica ad alte dimensioni; 3) Scoperta di modelli neurosimbolici e generativi, che esplora metodi per apprendere automaticamente modelli interpretabili e meccanicistici dai dati; e 4) Astrazioni Generative e Campionamento Guidato, che utilizza modelli generativi per creare simulatori rapidi e orientare gli output verso il soddisfacimento di vincoli complessi. I risultati complessivi indicano un cambiamento di paradigma da un'analisi basata puramente sulla simulazione a un approccio ibrido basato sui dati che non sacrifica le garanzie formali, consentendo l'applicazione della verifica formale a sistemi più ampi e complessi.
Publisher
EUT Edizioni Università di Trieste
Source
Francesca Cairoli, "Advanced Learning and Conformal Methods for Verification and Prediction of Stochastic Systems" in: "Pierluigi Barbieri, "iNEST – Interconnected Nord-Est Innovation Ecosystem: General frame of the project and Activities of Young Researcher at the University of Trieste", Trieste, EUT Edizioni Università di Trieste, 2025, pp.
Languages
en
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International