← 研踪 PaperTrailarXiv:2512.08991 · v4
Action-Guided Reachability for Deterministic World Models of Vision-Based Systems
首次提交 2025-12-08 10:32
版本更新 2026-11-10 10:19
雷达观测 2026-11-11 11:04
摘要
End-to-end vision-based controllers map raw camera images directly to control actions, yet verifying their closed-loop behavior remains challenging: no analytical model maps a physical state to a camera image, and propagating a set of states through high-dimensional images yields loose reachable sets. We address both challenges with two techniques. First, we propose a Deterministic World Model (DWM), a latent-free decoder that generates camera images only from the physical state, trained with a saliency-weighted reconstruction loss and a control-consistency loss. The DWM replaces the camera in the closed loop, so a sound and tight reachable tube of the surrogate closed loop can be computed without bounding any latent variables. Second, we propose an action-guided partition-and-verify scheme that certifies as many initial sets as possible within a fixed computation budget. A Gaussian process learned from cheap simulations orders the cells and splits those that lie across the property boundary, while every other unknown cell is split along the state dimension that most changes the controller's actions along the simulated closed loop, i.e., the one that most reduces the pixel uncertainty reaching the controller. On a CARLA braking system and three Gym benchmarks, the DWM is more accurate to the real camera than a cGAN surrogate and yields 1.9x to 69x narrower robustness intervals. The vision part causes most of the remaining overapproximation, and our splitting reduces the unknown fraction of the four-dimensional CartPole initial set from 21.88% to 8.18% within the budget.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v4 · 2026-11-10 10:19 · 最新观测版本
Action-Guided Reachability for Deterministic World Models of Vision-Based Systems
End-to-end vision-based controllers map raw camera images directly to control actions, yet verifying their closed-loop behavior remains challenging: no analytical model maps a physical state to a camera image, and propagating a set of states through high-dimensional images yields loose reachable sets. We address both challenges with two techniques. First, we propose a Deterministic World Model (DWM), a latent-free decoder that generates camera images only from the physical state, trained with a saliency-weighted reconstruction loss and a control-consistency loss. The DWM replaces the camera in the closed loop, so a sound and tight reachable tube of the surrogate closed loop can be computed without bounding any latent variables. Second, we propose an action-guided partition-and-verify scheme that certifies as many initial sets as possible within a fixed computation budget. A Gaussian process learned from cheap simulations orders the cells and splits those that lie across the property boundary, while every other unknown cell is split along the state dimension that most changes the controller's actions along the simulated closed loop, i.e., the one that most reduces the pixel uncertainty reaching the controller. On a CARLA braking system and three Gym benchmarks, the DWM is more accurate to the real camera than a cGAN surrogate and yields 1.9x to 69x narrower robustness intervals. The vision part causes most of the remaining overapproximation, and our splitting reduces the unknown fraction of the four-dimensional CartPole initial set from 21.88% to 8.18% within the budget.
查看此版本解读 →查看此版本原文 ↗