用形式化方法证明自动驾驶车辆无限时长下不碰撞，确保安全可靠。
Verification of Autonomous Neural Car Control with KeYmaera X
- 基于微分动态逻辑构建车辆避撞形式模型
- 证明在任意时长内均无碰撞，支持变反应时间与制动强度
- 揭示强化学习环境漏洞，适合安全验证研究者参考
本文针对ABZ'25案例研究，在微分动态逻辑（dL）框架下构建了自动驾驶汽车在高速公路上避撞的形式化模型，并使用KeYmaera X工具完成形式化安全证明。证明表明，在无限时间范围内不会发生碰撞，且该安全性独立于行程长度。模型考虑单车道场景中前后车辆情况，支持时变反应时间和制动力度。研究结果证实dL及其工具可作为运行时监控、防护机制和神经网络验证的严格基础。同时，文中揭示了原规范与仿真环境highway-env之间的不一致，修复后发现多个反例，暴露出强化学习训练环境中的潜在问题。
原文摘要 · Abstract (English)
This article presents a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a highway avoiding collisions with neighbouring cars. Using KeYmaera X's dL implementation, we prove absence of collision on an infinite time horizon which ensures that safety is preserved independently of trip length. The safety guarantees hold for time-varying reaction time and brake force. Our dL model considers the single lane scenario with cars ahead or behind. We demonstrate that dL with its tools is a rigorous foundation for runtime monitoring, shielding, and neural network verification. Doing so sheds light on inconsistencies between the provided specification and simulation environment highway-env of the ABZ'25 study. We attempt to fix these inconsistencies and uncover numerous counterexamples which also indicate issues in the provided reinforcement learning environment.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。