在数据稀疏时,如何可靠验证控制计划的可达性?
Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data
- 基于模型误差的有界光滑性,推导出可达管宽度的理论下界
- 提出可拒绝不支持序列的认证机制,避免虚假保证
- 适合关注安全控制验证的机器人与自动化研究者
从仿真到现实的策略通常基于理想动力学设计,但实际系统试验仅能提供少量孤立的一步转移。我们研究固定控制序列的预执行认证问题,如由学习策略生成的动作块。若该序列进入未观测的状态-输入区域,其观测结果可能与轨迹在该处分离任意大的目标系统一致。任何对所有此类系统均有效的确定性认证器,必须拒绝认证或返回投影宽度任意大的可达管。对于有界光滑的目标-名义模型误差类,我们推导出依赖于计划的投影宽度下界。这些结果揭示了统一轨迹包含、有限投影宽度与不受限模型误差行为之间的三难困境。ForeReach需要提供模型误差的分量式利普希茨边界;观测到的转移对可以否定此声明,但无法在观测区域外建立它。在有效声明的前提下,我们的方法构建模型误差的集合隶属包络,传播以区间的可达管,并仅当传播保持在认证域内且每个投影截面避开危险集时才进行认证。在两个基准系统中,校准基线在数据支持外失去轨迹包含后仍可能保持窄区间,而我们的方法会拒绝认证无支持的序列,并在相关目标数据和足够障碍物间隙可用时恢复认证。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。