用于验证基于视觉的神经反馈系统的随机世界模型

中文摘要 AI 辅助

验证基于视觉的神经反馈系统需要对其控制器所依据的观测进行建模。这样的模型必须捕捉传感器产生的变化，同时保持对闭环分析的可处理性。生成对抗网络（GAN）已被用作感知替代模型，但它们规模庞大，难以再现复杂场景，且难以验证。我们探索随机世界模型作为更丰富的感知替代模型类别。我们训练了一个具有物理基础潜在变量的世界模型，其构建基于标准验证器可界定的操作。该模型在再现保留帧方面比参数多达130倍的GAN替代模型更忠实。为了验证这些替代模型，我们开发了一种结合了反证、自适应细化、符号和反向分析的程序。在带有GAN替代模型的紧急制动基准上，我们的程序解决了整个状态空间，其中38%的状态空间是最先进的验证器未解决的。在基准的RGB版本上，此前没有报告过验证结果，我们的程序使用世界模型替代模型解决了超过80%的状态空间。

英文摘要

Verifying a vision-based neural feedback system requires a model of the observations its controller acts upon. Such a model must capture the variation the sensor produces, while remaining tractable for closed-loop analysis. Generative adversarial networks (GANs) have served as perception surrogates, but they are large, reproduce complex scenes poorly, and are hard to verify. We explore stochastic world models as a richer class of perception surrogates. We train a world model with physically grounded latents, built from operations that standard verifiers bound. It reproduces held-out frames more faithfully than GAN surrogates with up to 130 times as many parameters. To verify these surrogates, we develop a procedure that combines falsification, adaptive refinement, symbolic, and backward analyses. On an emergency braking benchmark with a GAN surrogate, our procedure resolves the entire state space, 38% of which the state-of-the-art verifier left unresolved. On the RGB version of the benchmark, where no verification results have previously been reported, our procedure resolves over 80% of the state space with a world model surrogate.

发表机构

• Stanford University（斯坦福大学）

机构由 AI 辅助整理，请以论文原文为准。