发表机构
University of Florida（佛罗里达大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出平滑仿真代理$S^3$，结合泰勒模型可达性实现动力系统离散抽象的梯度优化，经案例验证其可有效降低抽象保守性且计算高效。
AI 中文摘要
智能系统越来越多地部署在包含神经网络等黑箱控制器的安全关键场景中，可基于抽象方法将这些端到端系统替换为更简单的有限模型，以研究其属性与行为。构建此类抽象需平衡动力系统过近似的正确性与保守性，保守性表现为虚假或过度的非确定性行为。双仿真理论为表征这些关系提供了原则性度量，但未规定如何构造保守性最小的正确抽象。我们提出平滑仿真代理（$S^3$），它是近似用于量化保守性的反向仿真度量的可微目标函数。结合基于泰勒模型的可达性，$S^3$可对抽象参数进行基于梯度的优化，且通过构造保持正确性。我们在三个案例研究中评估该优化流程，结果显示$S^3$与反向仿真度量强相关、计算速度更快，且是减少抽象保守性的有效目标函数。
英文摘要
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.
