日本国立信息学研究所（NII）架构科学研究领域的莲尾一郎教授等人组成的研究团队，在JST战略性创造研究推进事业ERATO莲尾元数理系统设计项目（ERATO MMSD）中，开发出了为汽车自动驾驶系统的安全性提供强有力的数学保障的技术及基础理论。该研究成果已于7月5日在IIEEE Transactions on Intelligent Vehicles的网络版上公开。
研究团队提出的 “GA-RSS” 方法和RSS通用的自动驾驶安全性的数学证明方法（供图：国立信息学研究所（NII））
对于汽车自动驾驶技术的普及，仅仅提高自动驾驶汽车的安全性是不够的，还需要向社会保证自动驾驶汽车的高安全性，并对此进行解释，从而让人们接受自动驾驶汽车上路行驶。然而，以往的经验论和统计方法伴随着诸如“为什么可以说它足够安全”以及“能否给出一个让社会接受的解释”等问题，亟需创建一种能以更容易理解的方式解释安全性的逻辑方法。
对此，英特尔公司提出的RSS（responsibility-sensitive safety：责任敏感安全模型）方法论受到了人们的关注。它的目标是通过将交通安全规则写成明确的数学公式并证明公式的合理性来为自动驾驶汽车的安全性提供数学证明。
虽然通常很难用数学证明诸如自动驾驶等复杂系统的安全性，但RSS通过将证明对象缩小到自动驾驶汽车应该遵循的“逻辑安全规则”上，使之成为可能。然而，尽管RSS在产业界和学术界引起了相当大的兴趣，但制定和证明逻辑安全规则的技术基础尚未取得发展，应用范围仅限于在没有岔道的路上跟随前车行驶等简单的驾驶场景。
此次，NII的研究团队为克服RSS的这一弱点，利用形式逻辑学方面的专业知识新确立了RSS的技术基础，并在此基础上提出了RSS的扩展版“GA-RSS”。
以往的RSS仅用来避免单纯驾驶场景下的碰撞，而GA-RSS的特点是，对于需要实现“在避免与其他车辆碰撞的同时在安全地点紧急停车”等目标的复杂驾驶场景，也能制定逻辑安全规则并证明其正确性。
该方法是一种提出严密的数学逻辑安全规则，并将“只要遵守这些逻辑安全规则就不会发生事故”的事实作为“安全性定理”在数学上进行证明的方法。作为可以扩展的技术基础，研究团队新提出了名为dFHL（differential Floyd-Hoare logic：微分弗洛伊德·霍尔逻辑）的形式逻辑系统，并在此基础上设计和实现了逻辑安全规则推导工作流及软件支持。
通过将RSS与dFHL相结合，实现了向GA-RSS的扩展，由此可以应用于不同的自动驾驶场景。以紧急停车为例，以往的RSS安全规则会强制执行短视的防撞行为，会因其他车辆的阻挡而无法执行变道，也无法实现紧急停车的目标。而在GA-RSS安全规则下，可以把通过加速和刹车来绕过其他车辆的全局行动计划纳入安全规则，能够实现紧急停车的目标。
这种逻辑安全规则需要针对各种驾驶场景单独制定和证明。利用此次的成果——规则推导工作流程和软件支持，即使是复杂的驾驶场景，也能在约几周的现实时间内制定逻辑安全规则。
以这种方式创建的逻辑安全规则是不依赖于车企和车型等的通用规则，可以作为整个社会的资产长期使用。
今后，研究团队将在ERATO MMSD项目中利用此次提出的工作流和软件支持，制定针对更多驾驶场景的逻辑安全规则，同时，为进一步提高逻辑安全规则制定的效率并节省人力，还将推进理论研究和软件开发。
原文：《科学新闻》
翻译编辑：JST客观日本编辑部
【论文信息】
期刊：IEEE Transactions on Intelligent Vehicles
论文：Goal-Aware RSS for Complex Scenarios via Program Logic
URL：arxiv.org/abs/2207.02387
