用数学方法确保自动驾驶车辆实时安全，减少碰撞风险。
Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates
- 结合屏障证书与碰撞时间指标，构建可验证的安全框架。
- 实测显示碰撞风险降低40%，部分车道冲突完全消除。
- 适合关注自动驾驶安全验证的工程师和研究人员。
现代AI技术使自动驾驶车辆能够感知复杂场景、预测人类行为并实时决策，但这些数据驱动组件常为黑箱，缺乏可解释性与严格安全保证。自动驾驶在动态混合交通环境中运行，与人类驾驶车辆的交互带来不确定性与安全挑战。本文提出一种面向联网自动驾驶车辆（CAVs）的形式化安全框架，将屏障证书（BCs）与可解释的交通冲突度量（特别是时-空安全度量时间到碰撞，TTC）相结合。通过满足模理论（SMT）求解器验证安全条件，并采用自适应控制机制确保车辆实时遵守约束。在真实高速公路数据集上的评估显示，不安全交互显著减少，当TTC低于3秒的事件减少了最多40%，某些车道的冲突完全消除。该方法同时提供可解释与可证明的安全保障，展示了一种实用且可扩展的安全自动驾驶策略。
原文摘要 · Abstract (English)
Modern AI technologies enable autonomous vehicles to perceive complex scenes, predict human behavior, and make real-time driving decisions. However, these data-driven components often operate as black boxes, lacking interpretability and rigorous safety guarantees. Autonomous vehicles operate in dynamic, mixed-traffic environments where interactions with human-driven vehicles introduce uncertainty and safety challenges. This work develops a formally verified safety framework for Connected and Autonomous Vehicles (CAVs) that integrates Barrier Certificates (BCs) with interpretable traffic conflict metrics, specifically Time-to-Collision (TTC) as a spatio-temporal safety metric. Safety conditions are verified using Satisfiability Modulo Theories (SMT) solvers, and an adaptive control mechanism ensures vehicles comply with these constraints in real time. Evaluation on real-world highway datasets shows a significant reduction in unsafe interactions, with up to 40\% fewer events where TTC falls below a 3 seconds threshold, and complete elimination of conflicts in some lanes. This approach provides both interpretable and provable safety guarantees, demonstrating a practical and scalable strategy for safe autonomous driving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。