日本國立資訊學研究所（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
