面向视觉自主系统的统一概率化验证与验证

精确和全面的情境感知是现代自主系统的关键能力。从丰富的感信号中感知任务关键细节的深度神经网络已广泛普及；然而，其黑箱行为和对环境不确定性及分布迁移的敏感性，使得其形式化验证颇具挑战性。基于抽象的视觉自主系统验证技术产生的安全保证依赖于刚性假设，如界限误差或已知唯一分布。此类过于严格和不灵活的假设限制了保证的有效性，尤其是在多样化和不确定的测试时环境中。我们提出了一种方法，统一感知的验证模型与其离线验证。该方法利用区间马尔可夫决策过程（interval MDP），提供一种灵活的端到端保证，直接适应于测试时条件下的分布外情况。我们在具有明确状态估计分布的合成感知马尔可夫链和山坡车基准上评估了该方法。我们的发现表明，我们可以保证整体系统安全性的紧致且严格的界限。