Stochastic World Models for Verifying Vision-Based Neural Feedback Systems
作者: I. Samuel Akinwande, Mykel J. Kochenderfer, Clark Barrett
分类: cs.AI, eess.SY
发布日期: 2026-09-29
💡 一句话要点
提出随机世界模型以验证基于视觉的神经反馈系统
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 随机世界模型 生成对抗网络 神经反馈系统 闭环分析 验证技术
📋 核心要点
- 现有的生成对抗网络在复杂场景重现和验证方面存在显著不足，难以满足闭环分析的需求。
- 论文提出使用随机世界模型作为感知替代品，通过物理基础的潜变量训练模型，以提高重现精度和可验证性。
- 实验结果表明，使用世界模型替代品的验证程序能够解决超过80%的状态空间，显著优于现有方法的表现。
📝 摘要（中文）
验证基于视觉的神经反馈系统需要一个模型来描述控制器所依赖的观察数据。该模型必须能够捕捉传感器产生的变化，同时便于闭环分析。尽管生成对抗网络（GAN）曾作为感知替代品，但其体积庞大、对复杂场景的重现能力差且难以验证。本文探索了随机世界模型作为更丰富的感知替代品，训练了一个基于物理的潜变量的世界模型，能够比GAN替代品更真实地重现保留帧，参数量可高达130倍。为验证这些替代品，本文开发了一种结合虚假化、自适应细化、符号分析和反向分析的程序。在使用GAN替代品的紧急制动基准测试中，该程序解决了整个状态空间，其中38%的状态未被现有最先进的验证器解决。在RGB版本的基准测试中，使用世界模型替代品的程序解决了超过80%的状态空间，之前没有报告过验证结果。
🔬 方法详解
问题定义：本文旨在解决基于视觉的神经反馈系统验证中的模型构建问题，现有的生成对抗网络（GAN）在复杂场景的重现和验证上存在局限性。
核心思路：论文提出随机世界模型作为感知替代品，利用物理基础的潜变量进行训练，以更真实地重现观察数据并提高验证的可行性。
技术框架：整体架构包括数据采集、模型训练和验证程序三个主要模块。首先，通过传感器收集数据，然后训练随机世界模型，最后使用结合虚假化和符号分析的验证程序进行验证。
关键创新：最重要的技术创新在于引入随机世界模型，能够在参数量显著增加的情况下，仍然保持对复杂场景的高保真度重现，与传统的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.