基于 KeYmaera X 的自主神经汽车控制的验证
系统与控制
2026-01-28 v1 人工智能
机器学习
计算机科学中的逻辑
系统与控制
摘要
本文提出了一种形式化模型和形式化安全证明，用于微分动态逻辑(dL)中的 ABZ'25 案例研究。该案例研究涉及一辆在高速公路上行驶的自动驾驶汽车，需避免与相邻车辆的碰撞。利用 KeYmaera X 的 dL 实现，我们在无限时间范围内证明了不存在碰撞，从而确保安全性独立于行程长度。安全保证适用于时变反应时间和刹车力。我们的 dL 模型考虑了车辆前后方的单车道场景。我们展示了 dL 及其工具是运行时监控、屏蔽和神经网络验证的严格基础。通过这一工作，我们揭示了 ABZ'25 研究中提供的规范与模拟环境 highway-env 之间的不一致性。我们尝试修复这些不一致性，并发现诱发了诸多反例，这些反例还指示了所提供的强化学习环境中的问题。
关键词
引用
@article{arxiv.2504.03272,
title = {Verification of Autonomous Neural Car Control with KeYmaera X},
author = {Enguerrand Prebet and Samuel Teuber and André Platzer},
journal= {arXiv preprint arXiv:2504.03272},
year = {2026}
}
备注
21 pages, 6 figures; Accepted at the 11th International Conference on Rigorous State Based Methods (ABZ'25)