Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data
2026-08-03 • Robotics
Robotics
AI summaryⓘ
The authors study how to check if a fixed sequence of control actions will work safely on a real system when only limited data is available. They show that if the planned actions reach parts of the system’s behavior that haven’t been observed, any method that guarantees safety either cannot certify the plan or must allow very large uncertainty. To address this, the authors propose ForeReach, which depends on a known bound for how much the real system can differ from the model and uses observed data to build safety guarantees. Their method avoids false safety claims when data is lacking and can certify plans reliably when enough data and safety margins are present.
sim-to-real transfermodel errorcontrol sequencesafety certificationreachable setszonotopesLipschitz boundset-membershiptrajectory containmentaction chunk
Authors
Yanliang Huang, Zhen Zhang, Ahmad Hafez, Wenyuan Wu, Peng Xie, Zhuoqi Zeng, Amr Alanwar
Abstract
Sim-to-real policies are designed under nominal dynamics, but target-system trials may yield only a few isolated one-step transitions. We study pre-execution certification of a fixed control sequence, such as an action chunk produced by a learned policy. If the sequence reaches an unobserved state-input region, the observations remain consistent with target systems whose trajectories separate along it by an arbitrarily large amount. Any deterministic certifier sound for all of them must then decline to certify or return a reachable tube with arbitrarily large projected width. For bounded smooth classes of the target-nominal model error, we derive a finite plan-dependent projected-width lower bound. These results expose a trilemma among uniform trajectory containment, finite projected width, and unrestricted model-error behavior beyond the observations. ForeReach requires a supplied componentwise Lipschitz bound on the model error. Observed transition pairs can refute this declaration but cannot establish it outside the observed locations. Conditional on a valid declaration, our method constructs a set-membership envelope for the model error, propagates a zonotopic reachable tube, and certifies only when propagation remains within the certification domain and every projected tube slice avoids the unsafe set. In two benchmark systems, calibration baselines may remain narrow after losing trajectory containment outside data support, whereas our method declines to certify unsupported sequences and recovers certification when relevant target data and sufficient obstacle clearance are available.