用可微代理优化动态系统抽象，减少误报行为。
$S^3$: A Smooth Simulation Surrogate for Optimizing Discrete Abstractions of Dynamical Systems
- 提出可微的 $S^3$ 代理，逼近反向模拟度量
- 在三个案例中显著降低抽象保守性
- 适合安全关键系统中的控制器验证
智能系统越来越多地部署于安全关键场景，使用黑箱控制器（如神经网络）。通过抽象方法可将这些端到端系统替换为更简单的有限模型以研究其性质。构建此类抽象需在保真性与保守性之间权衡，后者表现为虚假或过度的非确定性行为。双模拟理论提供了刻画此类关系的严谨度量，但未给出如何构造最小保守性的保真抽象的方法。本文提出平滑模拟代理（$S^3$）——一种可微目标函数，用于近似反向模拟度量以量化保守性。结合泰勒模型可达性分析，$S^3$ 实现了对抽象参数的梯度优化，同时保证保真性。我们在三个案例研究中评估该优化流程，结果表明 $S^3$ 与反向模拟度量高度相关，计算更快，并能有效减少抽象保守性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。