CARVE：面向互動駕駛的基於包絡之被否决機動可認證低成本修正

摘要

互動式駕駛揭露了一種在基於規則的自動駕駛系統中容易被忽略的失效模式：即便非優先權主體進行小幅度的合法讓步即可恢復可行性，但自車候選方案仍可能具有負值的硬性規則邊界。現有的規則手冊、防護機制及可達域濾波器擅長否決不安全行為，而基於預測的規劃器則建模可能的回應。然而，二者均無法在運行時提供一個證明物件，用以說明：哪些有界多主體編輯能修復該操控行為、編輯的歸屬方、該請求是否在路權容許範圍內，以及若請求未被遵循時自車的備用方案為何。我們將此遺失的物件定義為「互動修復認證」，並提出 **CARVE**——一個無需預測的認證層，建構於自車歸屬與他車歸屬的戰術算子所構成的有限格之上。他車歸屬的請求僅在 \(B_j(s) = β(π_j)α_j^{\max}(s)\) 的「合作包絡」內允許，該包絡將運動學可達性與規範性優先權予以區分。最終的認證記錄了：約束規則、修復類別、修復集合、責任加權成本分攤及備用方案。在 589 個基於 Lanelet2 幾何的 INTERACTION 重播情境中，CARVE-Greedy 接受了最初被否決的 98.64% 操控行為，並恢復了 370/378 個人類判定為誤否決的案例，同時維持 589/589 的路權尊重、零優先權主體假陽性、以及 400/400 的壓力情境否決。我們證明了認證的正確性、結構性路權尊重、有限格精確最小性、備用應變能力及歸責一致性條件。CARVE 不預測也不要求其他駕駛者配合；它僅認證所提議的互動是否在宣告假設下為有界、可歸因且符合規範允許。

English

Interactive driving exposes a failure mode that is easy to miss in rule-aware autonomous-driving stacks: a hard-rule margin can be negative for an ego candidate even though a small lawful accommodation by a non-priority agent would restore feasibility. Existing rulebooks, shields, and reachability filters are strong at vetoing unsafe actions, while prediction-based planners model likely responses. Neither returns a runtime proof object that states which bounded multi-agent edit repairs the maneuver, who owns the edit, whether the request is right-of-way affordable, and what ego fallback remains if the request is not observed. We formulate this missing object as *interactive repair certification* and introduce *CARVE*, a prediction-free certificate layer over a finite lattice of ego-owned and agent-owned tactical operators. Agent-owned requests are admissible only inside \(B_j(s) = β(π_j)α_j^{\max}(s)\), a cooperation envelope that separates kinematic reachability from normative priority. The resulting certificate records the binding rule, repair category, repair set, responsibility-weighted cost split, and fallback. On 589 Lanelet2-geometry-grounded INTERACTION replay episodes, CARVE-Greedy accepts 98.64% of initially vetoed maneuvers and recovers 370/378 human-resolved false vetoes, while preserving 589/589 right-of-way respect, zero priority-agent false positives, and 400/400 negative-stress vetoes. We prove certificate soundness, structural right-of-way respect, exact finite-lattice minimality, fallback contingency, and blame-consistency conditions. CARVE does not predict or require another driver's compliance; it certifies whether a proposed interaction is bounded, attributable, and normatively admissible under declared assumptions.