aiqbench analysis
This research introduces $S^3$, a differentiable objective function designed to optimize discrete abstractions of dynamical systems containing neural network controllers. By enabling gradient-based tuning while maintaining soundness through Taylor model reachability, the method effectively reduces conservatism in safety-critical system verification without sacrificing computational efficiency. The approach represents a significant advancement in applying machine learning techniques to formal methods for verifying hybrid and cyber-physical systems.
$S^3$: A Smooth Simulation Surrogate for Optimizing Discrete Abstractions of Dynamical Systems
arXiv:2608.15920v1 Announce Type: cross Abstract: Intelligent systems are increasingly deployed in safety-critical settings with black-box controllers, including neural networks. The properties and behaviors of these end-to-end systems can be studied with abstraction-based methods that replace them with simpler finite models. Constructing such abstractions requires balancing the soundness of over-approximating the dynamical system against conservatism, which manifests as spurious or excessive nondeterministic behaviors. Bi-simulation theory provides principled metrics for characterizing these relationships, but does not prescribe how to construct sound abstractions with minimal conservatism. We fill this gap with a smooth simulation surrogate ($S^3$) --- a differentiable objective that approximates the reverse simulation metric used to quantify conservatism. Combined with Taylor model-based reachability, $S^3$ enables gradient-based optimization of abstraction parameters while preserving soundness by construction. We evaluate this optimization pipeline on three case studies. Our results show that $S^3$ is strongly correlated with the reverse simulation metric, is computationally faster, and serves as an effective objective for reducing abstraction conservatism.
Abstract:Intelligent systems are increasingly deployed in safety-critical settings with black-box controllers, including neural networks. The properties and behaviors of these end-to-end systems can be studied with abstraction-based methods that replace them with simpler finite models. Constructing such abstractions requires balancing the soundness of over-approximating the dynamical system against conservatism, which manifests as spurious or excessive nondeterministic behaviors. Bi-simulation theory provides principled metrics for characterizing these relationships, but does not prescribe how to construct sound abstractions with minimal conservatism. We fill this gap with a smooth simulation surrogate ($S^3$) --- a differentiable objective that approximates the reverse simulation metric used to quantify conservatism. Combined with Taylor model-based reachability, $S^3$ enables gradient-based optimization of abstraction parameters while preserving soundness by construction. We evaluate this optimization pipeline on three case studies. Our results show that $S^3$ is strongly correlated with the reverse simulation metric, is computationally faster, and serves as an effective objective for reducing abstraction conservatism.
Systems and Control (eess.SY); Machine Learning (cs.LG)
arXiv:2608.15920 [eess.SY]
(or arXiv:2608.15920v1 [eess.SY] for this version)
https://doi.org/10.48550/arXiv.2608.15920 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 252 words
Related coverage
OnlyDense: Reduced-Order Modeling for Lagrangian simulation
arXiv · Jun 9, 2026
Bayesian Optimization for Learning Nonlinear MPC in Autonomous Agent Navigation
arXiv · Jun 16, 2026

[AINews] Reality Checks on AI News (Yegge shuts down Gas Town, Databricks’ +60% Astra cost)
Latent Space · Sep 17, 2026
Fast and Scalable Multi-Agent Distribution Matching via Partitioned Optimal Transport
arXiv · Oct 1, 2026