Pith. sign in

REVIEW 3 major objections 5 minor 46 references

A rule hierarchy matches human driving preferences 80.9 percent of the time

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 22:41 UTC pith:XV4WS465

load-bearing objection A genuinely useful AV benchmark with solid external validation, but the 80.9% alignment headline is softer than it looks once you read Table V, and the in-sample priority tuning should be relabeled. the 3 major comments →

arxiv 2602.16073 v2 pith:XV4WS465 submitted 2026-02-17 cs.RO cs.AIcs.LOcs.SYeess.SY

ScenicRules: An Autonomous Driving Benchmark with Multi-Objective Specifications and Abstract Scenarios

Kevin Kai-Chun Chang , Ekin Beyazit , Alberto Sangiovanni-Vincentelli , Tichakorn Wongpiromsarn , Sanjit A. Seshia This is my paper
classification cs.RO cs.AIcs.LOcs.SYeess.SY
keywords autonomous drivingrulebookmulti-objective specificationscenario generationScenicfalsificationformal verificationSTL
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper introduces ScenicRules, a benchmark for autonomous driving that evaluates an agent against a prioritized set of formalized driving objectives rather than a single weighted score. It formalizes 19 driving rules as temporal-logic formulas with quantitative violation scores, groups them into a Hierarchical Rulebook in which whole classes of rules inherit priority relations, and pairs this specification layer with formal, stochastic scenarios written in the Scenic language. The paper claims this combination is the first of its kind and shows that the rulebook's induced trajectory preferences agree with human judgments on 80.9±1.8% of pairwise comparisons, on par with learned baselines. It also shows the benchmark exposes diverse failure modes under falsification, including cases where an agent avoids a collision only by violating road-compliance rules. A sympathetic reader would take away that prioritized, interpretable specifications can serve as a practical evaluation instrument for autonomous driving systems.

Core claim

The paper's central claim is that combining a Hierarchical Rulebook — a set of rule groups with explicit pairwise priorities, where each rule carries a temporal-logic formula and a violation score — with Scenic programs as abstract scenario models yields a benchmark that is both interpretable and aligned with real driving behavior. On a public dataset of human trajectory preferences, the base rulebook achieves 80.9±1.8% agreement; scenario-specific priority tuning reaches 85.97%, matching brute-force permutation search. Under simulation-based falsification, the benchmark produces hundreds of distinct combinations of violated rules across common and near-accident scenarios, demonstrating that

What carries the argument

The central machinery is the Hierarchical Rulebook: rules are grouped by function (safety-critical, road compliance, safety-enhancing, precautionary, social interpretability, progress, comfort), and priorities are assigned between groups rather than among individual rules, which would otherwise require navigating more than 10^35 possible orderings. Each rule's violation is quantified by a violation score, and the error value of a trajectory is a priority-weighted sum of violated rules. Around this sits the scenario layer: a k-center greedy selector picks a compact set of representative Scenic programs (encoded as Hamming vectors) from more than a million possible combinations, and a falsifie

Load-bearing premise

The benchmark's agreement with human judgments rests on the authors' specific choices of rule formalizations, group priority orderings, and threshold parameters; the paper's own results show that a different equally reasonable encoding can drop agreement from 80.9% to as low as 70.8%.

What would settle it

Re-run the human-preference evaluation with the sum-based vehicle-clearance formalization in place of the default max-based one, using an independent set of preference labels not involved in tuning. If agreement holds near 80%, the formalization choice is not load-bearing; if it falls toward the paper's reported 70.8%, the benchmark's headline alignment is sensitive to that encoding.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Agents can be compared by which prioritized rule they violate first, revealing qualitatively different failure modes in the same scenario.
  • The rule set and violation scores are extensible: users can add custom rules or swap formalizations, and the paper shows such swaps change evaluation outcomes.
  • The scenario-selection procedure guarantees that every maneuver/spatial-relation combination in the covered space is within Hamming distance 2 of a selected scenario, so a small suite covers a large space.
  • Context-specific priorities can be learned from human preference data, converging in two greedy iterations to the same accuracy as exhaustive search.
  • The benchmark exercises every collected rule: falsification found at least one violation of each objective across the scenario suite.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Because the paper's Table V shows roughly a ten-point swing in human agreement when clearance is formalized as a sum rather than a maximum, the benchmark's headline number is tied to a specific encoding; a standardized 'formalization card' would make results portable across implementations.
  • The near-accident scenarios are generated from collision reports through an LLM-assisted pipeline, so the suite's realism inherits the quality of those reports and prompts; an obvious test is whether independently reconstructed programs produce similar falsification findings.
  • The roughly 80% agreement ceiling is close to the dataset's reported inter-annotator agreement, suggesting a single static rulebook may already be near saturation; modeling a distribution over rulebooks, or per-scenario attribution of responsibility, could push alignment higher.
  • The evaluation machinery could be reused beyond driving — for robot navigation or human-robot interaction — wherever objectives conflict and priorities need to be explicit.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces ScenicRules, a benchmark for autonomous driving that pairs a multi-objective, priority-based specification framework (Hierarchical Rulebook, extending the prior Rulebook structure) with formal scenario models written in the Scenic language. It contributes a collection of 19 formalized driving objectives, a group-based hierarchical priority structure, a curated set of common and near-accident Scenic scenarios (the latter generated from natural-language collision reports via an LLM-assisted pipeline), and experimental results on the Reasonable Crowd dataset showing 80.9±1.8% agreement between the rulebook-induced preferences and human preferences, comparable to published RF/LR baselines. It also demonstrates falsification-based failure discovery on the scenario suite.

Significance. If the reported alignment is robust, ScenicRules would be a valuable and extensible evaluation instrument: it combines explicit priority relations among objectives with an expressive, formally grounded scenario language, and it is validated against external human judgments. The paper ships a repository and reports the base human-agreement result with cross-validated error bars, explicitly acknowledging the ~84% human-human agreement ceiling. The coreset-based scenario selection and the demonstration of diverse joint failure modes are also useful contributions. However, the central alignment claim depends on specific rule formalizations and priority choices, and the sensitivity evidence in the paper itself substantially tempers the contribution's strength.

major comments (3)
  1. [Sec. V-A(d), Table V] The headline claim that the formalized objectives and Hierarchical Rulebooks 'align well' with human judgments is not robust to equally defensible formalization choices. Table V shows that changing clearance aggregation from max to sum lowers accuracy from 80.97% to 70.80%, heading-based classification gives 78.35%, and centroid-based correct-side gives 79.07%. The default choices are not given an independent, principled justification; they appear to be the ones yielding the highest number. Since the paper's central external-validation claim rests on this encoding, the authors should either provide a rule-based or behavioral argument for the defaults, or report the accuracy as a range and soften the claim. A 10-point swing across plausible formalizations means the current claim of 'alignment' is overstated.
  2. [Sec. V-A(c), Table IV] The context-aware priority tuning experiment is performed in-sample. Table IV reports 85.97% accuracy after greedy priority permutation search, matching brute force, but this optimization is conducted on the same evaluation dataset used to compute the accuracy. Consequently, the result does not provide evidence that human preferences are genuinely context-dependent in a generalizable sense; it demonstrates overfitting to the Reasonable Crowd scenarios. To support the claim of validation, the authors should use held-out trajectories or nested cross-validation when optimizing priorities and report the resulting out-of-sample accuracy.
  3. [Sec. V-A(a), Table III] The statement that 'our rulebook is designed independently of the dataset and generalizes to arbitrary scenarios' is not fully supported. While the base rulebook itself is not trained on the labels, its formalization choices (e.g., the priority ordering in Fig. 4 and the threshold values in Table I) were selected by the authors, and the 'w/ parameter' variant is explicitly tuned on the same 5-fold splits. At minimum, the independence claim should be restricted to the base rulebook and should acknowledge that the rule set and priorities are still a human-authored encoding rather than a purely principled or learned one. Please clarify the exact status of the base versus optimized results.
minor comments (5)
  1. [Table I, Rule 7] The VS formula for Rule 7 appears to be a copy-paste error from Rule 6: it reads 'max_{t,k,i}(a0,i(t)-Aack)', which uses an acceleration threshold, whereas the rule is about vehicle time-to-collision and should involve T_vehicle,ttc. Please correct the formula and verify the implementation matches the intended semantics.
  2. [Definition 2] The example '23+20=9' is missing superscript formatting; it should read 2^3 + 2^0 = 9. Please fix the typesetting.
  3. [Abstract / Sec. I] The claim of being 'the first benchmark' to combine rulebooks with Scenic is strong given the authors' prior work [4] and other Scenic-driven falsification tools. Consider qualifying the novelty (e.g., 'first comprehensive benchmark' or 'first benchmark that additionally...') to avoid overclaim.
  4. [Sec. V-Ba, Table VI] The coverage claim would be more informative if the authors reported the distribution of Hamming distances (e.g., how many scenarios are at distance 0, 1, 2) instead of only the maximum distance. The current table shows full categorical coverage, but the 'max distance 2' is the only quantitative summary.
  5. [Appendix E] The appendix notes that LLM-generated programs contain minor syntax errors requiring manual refinement. Please state how many of the 27 near-accident programs required human correction and whether the reported falsification results are based on the corrected versions. This is relevant for reproducibility.

Circularity Check

1 steps flagged

Central 80.9% alignment is externally grounded, but the 85.97% context-dependent accuracy is an in-sample fit of the same optimization objective.

specific steps
  1. fitted input called prediction [Sec. V-Ac / Table IV / Algorithm 1 (Appendix B)]
    "The algorithm employs an iterative greedy strategy. First, it calculates the baseline agreement rate between the initial rulebook and the human-labeled dataset (Line 2) using the evaluateAgreement function. ... If a swap yields a rate higher than the current best ... the configuration is updated. ... As shown in T able IV, scenario-specific rulebooks achieve higher accuracy than a monolithic rulebook, validating that human preferences are context-dependent."

    Algorithm 1 returns B*_M only when no group swap can increase evaluateAgreement(B*_M, L) on the labeled dataset L. Table IV's reported 'Accuracy (%)' for scenario-specific rulebooks is exactly this same evaluateAgreement objective on L. Therefore the 85.97% figure is the maximized value of the function used to select the rulebook, so reporting it as evidence that human preferences are context-dependent is not an independent validation: the rulebook was chosen to produce that number. This is in-sample fitting presented as confirming evidence, though it is peripheral to the base 80.9% result.

full rationale

The paper's main alignment claim, 80.9±1.8% agreement with human trajectory preferences on the Reasonable Crowd dataset, is grounded in an external dataset and is claimed to come from a rulebook designed independently of the dataset. That is genuine external evidence and not circular. Algorithm 2's parameter tuning is evaluated with 5-fold cross-validation, so it is not itself a direct self-fit. The paper's self-citations to prior Rulebook, Scenic, and VerifAI work are used as definitions and tools, not as the proof of the benchmark's validity, so they are not load-bearing circularity. The formalization-sensitivity results in Table V are a robustness concern for the headline claim, but they are not a definitional collapse because the alternative formalizations are not fit to the same objective; they show the result is choice-dependent rather than that the derivation reduces to its inputs. The clearest circular step is the context-aware priority optimization in Table IV / Algorithm 1, where the reported accuracy is the very objective being maximized on the same labels. This overstates the evidence for context-dependence, but it does not invalidate the externally grounded base result.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 1 invented entities

The central claim rests on: standard STL robustness semantics; the rulebook error-weight aggregation inherited from the authors' prior work [4]; external human-preference labels as ground truth (with known ~84% annotator ceiling); the expressiveness of the hierarchical-rulebook class itself; MetaDrive's fidelity to the encoded scenarios; and the adequacy of the discrete attribute encoding for scenario diversity. Free parameters include all rule thresholds (greedily tuned on the evaluation data in Algorithm 2, values unreported), the hand-specified baseline priority ordering, the k=100 scenario budget, and the per-scenario priority permutations of Table IV, which are fitted on the same labels they are scored against.

free parameters (4)
  • Rule thresholds (TTC limits, clearance distances, acknowledgment thresholds, speed-limit V_limit) = Greedily tuned via Algorithm 2 on Reasonable Crowd labels; tuned values not reported in text
    These thresholds define what counts as a violation and its severity. The paper reports the improvement from tuning (80.9→81.8%) but never reports the fitted values, so the benchmark's behavior is not fully specified without the repo.
  • Baseline hierarchical priority ordering of rule groups (Fig. 4) = Hand-specified: safety-critical before road-compliance before safety-enhancing before social-interpretability before pre
    Drives all RQ1 results. The paper labels it a 'reference baseline' and shows context-specific re-orderings change accuracy by about 5 points (Table IV), making it a chosen-by-hand structural parameter rather than a derived one.
  • Scenario budget k=100 for k-center coreset selection (per configuration) = 100
    Hand-chosen budget. The coverage guarantee (max Hamming distance 2 out of 3,232 encodings) holds only at this budget; the paper does not justify the number or report how coverage degrades with smaller k.
  • Per-scenario optimized priority ordering (Table IV) = 85.08% (adjacent swaps) / 85.97% (arbitrary swaps), matching brute-force search
    Fit per scenario on the same Reasonable Crowd labels used for scoring. This is an in-sample fit ceiling of the hierarchical-rulebook class, not a predictive validation.
axioms (6)
  • standard math STL semantics and quantitative robustness (Appendix A) correctly quantify violation severity
    Underlies all rule formalizations (Table I); standard Maler-Nickovic/Donze-Maler theory, not derived in the paper.
  • domain assumption Rulebook error value with exponential weights 2^(m_r) (Def. 2, from [4]) is the right aggregation of priority-weighted violations
    Inherited from the authors' prior work; the exponential weighting is a design choice and no alternative aggregations are compared.
  • domain assumption Reasonable Crowd dataset [3], aggregated via Bradley-Terry, provides ground-truth human driving preference
    External evidence, but the paper itself notes annotator agreement is only about 84%, capping achievable rulebook alignment; the dataset's co-authors overlap with this paper's authors.
  • domain assumption Human driving preferences are representable by a preorder over rule groups (the hierarchical-rulebook class)
    The greedy/brute-force optimization in Table IV searches only this restricted class; the 85.97% ceiling equals the best fit inside the class, so the class's expressiveness bounds the claimed context-dependence result.
  • domain assumption MetaDrive faithfully realizes the Scenic scenarios and agent behaviors as specified
    All falsification results (Table VII) are simulator runs; no validation against real-world outcomes is offered.
  • domain assumption Scenario diversity is captured by the discrete attribute encoding (ego/adversary maneuver + spatial relation) with Hamming distance
    The coverage claims in Table VI hold only within this encoding; continuous semantic parameters (speeds, braking, offsets) and map variability are not part of the diversity measure.
invented entities (1)
  • Hierarchical Rulebook B_M (rule groups with inter-group and intra-group priorities) independent evidence
    purpose: Reduces the huge number of possible rule orderings to interpretable group-level priorities and enables context-specific and data-driven priority adaptation
    Not a physical entity, but a new conceptual framework element carrying falsifiable predictions (trajectory-preference rankings) that are checked against the external Reasonable Crowd labels and sensitivity tables, so it has an independent handle.

pith-pipeline@v1.3.0-alltime-deepseek · 5202 in / 5973 out tokens · 253495 ms · 2026-08-02T22:41:45.225861+00:00 · methodology

0 comments
read the original abstract

Developing autonomous driving systems for complex traffic environments requires balancing multiple objectives, such as avoiding collisions, obeying traffic rules, and making efficient progress. In many situations, these objectives cannot be satisfied simultaneously, and explicit priority relations naturally arise. Also, driving rules require context, so it is important to formally model the environment scenarios within which such rules apply. Existing benchmarks for evaluating autonomous vehicles lack such combinations of multi-objective prioritized rules and formal environment models. In this work, we introduce ScenicRules, a benchmark for evaluating autonomous driving systems in stochastic environments under prioritized multi-objective specifications. We first formalize a diverse set of objectives to serve as quantitative evaluation metrics. Next, we design a Hierarchical Rulebook framework that encodes multiple objectives and their priority relations in an interpretable and adaptable manner. We then construct a compact yet representative collection of scenarios spanning diverse driving contexts and near-accident situations, formally modeled in the Scenic language. Experimental results show that our formalized objectives and Hierarchical Rulebooks align well with human driving judgments and that our benchmark effectively exposes agent failures with respect to the prioritized objectives. Our benchmark can be accessed at https://github.com/BerkeleyLearnVerify/ScenicRules/.

Figures

Figures reproduced from arXiv: 2602.16073 by Alberto Sangiovanni-Vincentelli, Ekin Beyazit, Kevin Kai-Chun Chang, Sanjit A. Seshia, Tichakorn Wongpiromsarn.

Figure 1
Figure 1. Figure 1: Real-world autonomous driving examples with multiple conflicting objectives. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: An example of a Rulebook. III. PRELIMINARIES A. Signal Temporal Logic (STL) Signal temporal logic (STL) [33] extends Linear Temporal Logic (LTL) by introducing real-time and real-valued constraints. In this section, we focus on the two STL operators used in this paper: the eventually operator F and the globally operator G. Their semantics are defined as follows: (x,t)|=FIφ ⇐⇒ ∃t ′∈t+I· [PITH_FULL_IMAGE:fi… view at source ↗
Figure 3
Figure 3. Figure 3: An example Scenic program. to an objective, and each directed edge (v1,v2)∈EB indicates that v1 has a higher priority than v2 [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Our automated Scenic program generator. TABLE II: Supported attributes in the Scenic generator. Attribute Supported Options agent type car, pedestrian vehicle maneuver going straight, left turn, right turn, lane change, lane following spatial relation to ego ahead of, behind, faster lane, slower lane, opposing lanes, conflicting lanes pedestrian maneuver crossing street, walking along sidewalk maneuver, an… view at source ↗
Figure 6
Figure 6. Figure 6: The falsification flow. dataset. Using the greedy algorithm from Sec. IV-B, and with the safety-critical group fixed at the highest priority, we optimize the priority relations among the remaining groups. We evaluate two settings: swapping only adjacent groups and swapping arbitrary pairs. As shown in Table IV, scenario-specific rulebooks achieve higher accuracy than a monolithic rulebook, validating that … view at source ↗
Figure 7
Figure 7. Figure 7: Different failure modes identified under the same driving [PITH_FULL_IMAGE:figures/full_fig_p008_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Example from the Reasonable Crowd dataset [3]. Each sce [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Evaluation flow for comparing hierarchical Rulebook [PITH_FULL_IMAGE:figures/full_fig_p011_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: An example common scenario specification. [PITH_FULL_IMAGE:figures/full_fig_p012_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The corresponding Scenic program of the specification in Fig. 10 (Part I). [PITH_FULL_IMAGE:figures/full_fig_p013_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: The corresponding Scenic program of the specification in Fig. 10 (Part II). [PITH_FULL_IMAGE:figures/full_fig_p014_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: The prompt used for LLM-assisted Scenic program generation (Part I). [PITH_FULL_IMAGE:figures/full_fig_p015_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: The prompt used for LLM-assisted Scenic program generation (Part II). [PITH_FULL_IMAGE:figures/full_fig_p016_14.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 8 linked inside Pith

  1. [1]

    How W aymo’s driverless technology avoided scooter rider who fell into Austin road,

    KXAN Austin, “How W aymo’s driverless technology avoided scooter rider who fell into Austin road,” 2024. [Online]. A vailable: https: //youtu.be/h7PGrAlPELc?si=ZkURWsldNjSi3OKQ

    2024

  2. [2]

    Tesla’s approach to autonomy,

    A. Elluswamy, “Tesla’s approach to autonomy,” 2025. [Online]. A vailable: https://x.com/aelluswamy/status/1981644831790379245

    arXiv 2025

  3. [3]

    The Reasonable Crowd: T owards evidence-based and interpretable models of driving behavior,

    B. Helou, A. Dusi, A. Collin, N. Mehdipour, Z. Chen, C. Lizarazo, C. Belta, T . W ongpiromsarn, R. D. T ebbens, and O. Beijbom, “The Reasonable Crowd: T owards evidence-based and interpretable models of driving behavior,” in IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2021, pp. 6708–6715

    2021

  4. [4]

    Dynamic, multi-objective specification and falsification of autonomous CPS,

    K. K.-C. Chang, K. Xu, E. Kim, A. Sangiovanni-Vincentelli, and S. A. Seshia, “Dynamic, multi-objective specification and falsification of autonomous CPS, ” inInternational Conference on Runtime V erification (RV). Springer, 2024, pp. 40–58

    2024

  5. [5]

    Addressing the IEEE A V test challenge with Scenic and V erifAI,

    K. Viswanadha, F . Indaheng, J. W ong, E. Kim, E. Kalvan, Y . Pant, D. J. Fremont, and S. A. Seshia, “ Addressing the IEEE A V test challenge with Scenic and V erifAI,” inIEEE International Conference on Artificial Intelligence T esting (AIT est). IEEE, 2021, pp. 136–142

    2021

  6. [6]

    On a formal model of safe and scalable self-driving cars,

    S. Shalev-Shwartz, S. Shammah, and A. Shashua, “On a formal model of safe and scalable self-driving cars, ”arXiv preprint arXiv:1708.06374, 2017

    Pith/arXiv arXiv 2017

  7. [7]

    Objective metrics of comfort: Developing a driving style for highly automated vehicles,

    H. Bellem, T . Schönenberg, J. F . Krems, and M. Schrauf, “Objective metrics of comfort: Developing a driving style for highly automated vehicles,” Transportation Research P art F: Traffic Psychology and Behaviour, vol. 41, pp. 45–54, 2016

    2016

  8. [8]

    Formalization of intersection traffic rules in temporal logic,

    S. Maierhofer, P . Moosbrugger, and M. Althoff, “Formalization of intersection traffic rules in temporal logic,” inIEEE Intelligent V ehicles Symposium (IV). IEEE, 2022, pp. 1135–1144

    2022

  9. [9]

    Large scale interactive motion forecasting for autonomous driving: The W aymo Open Motion Dataset,

    S. Ettinger, S. Cheng, B. Caine, C. Liu, H. Zhao, S. Pradhan, Y . Chai, B. Sapp, C. R. Qi, Y . Zhouet al., “Large scale interactive motion forecasting for autonomous driving: The W aymo Open Motion Dataset,” inIEEE/CVF International Conference on Computer V ision (ICCV), 2021, pp. 9710–9719

    2021

  10. [10]

    Argoverse 2: Next genera- tion datasets for self-driving perception and forecasting,

    B. Wilson, W . Qi, T . Agarwal, J. Lambert, J. Singh, S. Khandelwal, B. Pan, R. Kumar, A. Hartnett, J. K. Ponteset al., “ Argoverse 2: Next genera- tion datasets for self-driving perception and forecasting,”arXiv preprint arXiv:2301.00493, 2023

    Pith/arXiv arXiv 2023

  11. [11]

    nuScenes: A multimodal dataset for autonomous driving,

    H. Caesar, V . Bankiti, A. H. Lang, S. V ora, V . E. Liong, Q. Xu, A. Krishnan, Y . Pan, G. Baldan, and O. Beijbom, “nuScenes: A multimodal dataset for autonomous driving,” inIEEE/CVF Conference on Computer V ision and P attern Recognition (CVPR), 2020, pp. 11 621–11 631

    2020

  12. [12]

    One thousand and one hours: Self-driving motion prediction dataset,

    J. Houston, G. Zuidhof, L. Bergamini, Y . Y e, L. Chen, A. Jain, S. Omari, V . Iglovikov, and P . Ondruska, “One thousand and one hours: Self-driving motion prediction dataset, ” inConference on Robot Learning (CoRL). PMLR, 2021, pp. 409–418

    2021

  13. [13]

    T owards learning- based planning: The nuPlan benchmark for real-world autonomous driving,

    N. Karnchanachari, D. Geromichalos, K. S. T an, N. Li, C. Eriksen, S. Y aghoubi, N. Mehdipour, G. Bernasconi, W . K. Fong, Y . Guoet al., “T owards learning- based planning: The nuPlan benchmark for real-world autonomous driving, ” in IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2024, pp. 629–636

    2024

  14. [14]

    nuPlan: A closed-loop ML-based planning benchmark for autonomous vehicles,

    H. Caesar, J. Kabzan, K. S. T an, W . K. Fong, E. W olff, A. Lang, L. Fletcher, O. Beijbom, and S. Omari, “nuPlan: A closed-loop ML-based planning benchmark for autonomous vehicles, ”arXiv preprint arXiv:2106.11810, 2021

    Pith/arXiv arXiv 2021

  15. [15]

    CommonRoad: Composable benchmarks for motion planning on roads,

    M. Althoff, M. Koschi, and S. Manzinger, “CommonRoad: Composable benchmarks for motion planning on roads,” inIEEE Intelligent V ehicles Symposium (IV). IEEE, 2017, pp. 719–726

    2017

  16. [16]

    NA VSIM: Data-driven non- reactive autonomous vehicle simulation and benchmarking,

    D. Dauner, M. Hallgarten, T . Li, X. W eng, Z. Huang, Z. Y ang, H. Li, I. Gilitschenski, B. Ivanovic, M. Pavoneet al., “NA VSIM: Data-driven non- reactive autonomous vehicle simulation and benchmarking,”Advances in Neural Information Processing Systems, vol. 37, pp. 28 706–28 719, 2024

    2024

  17. [17]

    M3CAD: T owards generic cooperative autonomous driving benchmark,

    M. Zhu, Y . Zhu, Y . Zhu, Q. Chen, D. Qu, S. Fu, and Q. Y ang, “M3CAD: T owards generic cooperative autonomous driving benchmark, ”arXiv preprint arXiv:2505.06746, 2025

    arXiv 2025

  18. [18]

    Liability, ethics, and culture-aware behavior specification using rulebooks,

    A. Censi, K. Slutsky, T . W ongpiromsarn, D. Y ershov, S. Pendleton, J. Fu, and E. Frazzoli, “Liability, ethics, and culture-aware behavior specification using rulebooks, ” inInternational Conference on Robotics and Automation (ICRA). IEEE, 2019, pp. 8536–8542

    2019

  19. [19]

    INTERACTION dataset: An international, adversarial and cooperative motion dataset in interactive driving scenarios with semantic maps,

    W . Zhan, L. Sun, D. W ang, H. Shi, A. Clausse, M. Naumann, J. Kummerle, H. Konigshof, C. Stiller, A. de La Fortelleet al., “INTERACTION dataset: An international, adversarial and cooperative motion dataset in interactive driving scenarios with semantic maps, ”arXiv preprint arXiv:1910.03088, 2019

    Pith/arXiv arXiv 1910

  20. [20]

    SceNDD: A scenario-based naturalistic driving dataset,

    A. Prabu, N. Ranjan, L. Li, R. Tian, S. Chien, Y . Chen, and R. Sherony, “SceNDD: A scenario-based naturalistic driving dataset,” inIEEE 25th International Conference on Intelligent Transportation Systems (ITSC). IEEE, 2022, p. 4363–4368

    2022

  21. [21]

    scenario.center: Methods from real-world data to a scenario database,

    M. Schuldes, C. Glasmacher, and L. Eckstein, “scenario.center: Methods from real-world data to a scenario database, ” inIEEE Intelligent V ehicles Symposium (IV). IEEE, 2024, pp. 1119–1126

    2024

  22. [22]

    A coreset selection of coreset selection literature: Introduction and recent advances,

    B. B. Moser, A. S. Shanbhag, S. Frolov, F . Raue, J. Folz, and A. Dengel, “ A coreset selection of coreset selection literature: Introduction and recent advances, ”arXiv preprint arXiv:2505.17799, 2025

    arXiv 2025

  23. [23]

    Active learning for convolutional neural networks: A core-set approach,

    O. Sener and S. Savarese, “ Active learning for convolutional neural networks: A core-set approach, ”arXiv preprint arXiv:1708.00489, 2017

    Pith/arXiv arXiv 2017

  24. [24]

    Scenic: A language for scenario specification and data generation,

    D. J. Fremont, E. Kim, T . Dreossi, S. Ghosh, X. Y ue, A. L. Sangiovanni- Vincentelli, and S. A. Seshia, “Scenic: A language for scenario specification and data generation,”Machine Learning, vol. 112, no. 10, pp. 3805–3849, 2023

    2023

  25. [25]

    Scenic: A language for scenario specification and scene generation,

    D. J. Fremont, T . Dreossi, S. Ghosh, X. Y ue, A. L. Sangiovanni-Vincentelli, and S. A. Seshia, “Scenic: A language for scenario specification and scene generation, ” inACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2019

    2019

  26. [26]

    A survey on autonomous driving datasets: Statistics, annotation 8 quality, and a future outlook,

    M. Liu, E. Y urtsever, J. Fossaert, X. Zhou, W . Zimmer, Y . Cui, B. L. Zagar, and A. C. Knoll, “ A survey on autonomous driving datasets: Statistics, annotation 8 quality, and a future outlook, ”IEEE Transactions on Intelligent V ehicles (T -IV), 2024

    2024

  27. [27]

    Carla autonomous driving challenge

    CARLA, “Carla autonomous driving challenge.” [Online]. A vailable: https://leaderboard.carla.org/challenge/

  28. [28]

    Pseudo-simulation for autonomous driving,

    W . Cao, M. Hallgarten, T . Li, D. Dauner, X. Gu, C. W ang, Y . Miron, M. Aiello, H. Li, I. Gilitschenski, B. Ivanovic, M. Pavone, A. Geiger, and K. Chitta, “Pseudo-simulation for autonomous driving, ” inConference on Robot Learning (CoRL), 2025

    2025

  29. [29]

    Example applications of IEEE std 2846-2022 to formal safety-related models,

    “Example applications of IEEE std 2846-2022 to formal safety-related models, ”

    2022

  30. [30]

    Safety of the intended driving behavior using rulebooks,

    A. Collin, A. Bilka, S. Pendleton, and R. D. Tebbens, “Safety of the intended driving behavior using rulebooks,” inIEEE Intelligent V ehicles Symposium (IV), 2020, pp. 136–143

    2020

  31. [31]

    Parallel and multi-objective falsification with Scenic and V erifAI,

    K. Viswanadha, E. Kim, F . Indaheng, D. J. Fremont, and S. A. Seshia, “Parallel and multi-objective falsification with Scenic and V erifAI,” inInternational Conference on Runtime V erification (RV). Springer, 2021, pp. 265–276

    2021

  32. [32]

    T oward verified artificial intelligence,

    S. A. Seshia, D. Sadigh, and S. S. Sastry, “T oward verified artificial intelligence, ” Communications of the ACM, vol. 65, no. 7, pp. 46–55, 2022

    2022

  33. [33]

    Monitoring temporal properties of continuous signals,

    O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals, ” inInternational Symposium on F ormal T echniques in Real-Time and F ault-T olerant Systems (FTRTFT). Springer, 2004, pp. 152–166

    2004

  34. [34]

    Robust satisfaction of temporal logic over real-valued signals,

    A. Donzé and O. Maler, “Robust satisfaction of temporal logic over real-valued signals,” inInternational Conference on F ormal Modeling and Analysis of Timed Systems (FORMATS). Springer, 2010, pp. 92–106

    2010

  35. [35]

    Robustness of temporal logic specifications for continuous-time signals,

    G. E. Fainekos and G. J. Pappas, “Robustness of temporal logic specifications for continuous-time signals, ”Theoretical Computer Science, vol. 410, no. 42, pp. 4262–4291, 2009

    2009

  36. [36]

    CARLA: An open urban driving simulator,

    A. Dosovitskiy, G. Ros, F . Codevilla, A. Lopez, and V . Koltun, “CARLA: An open urban driving simulator, ” inConference on Robot Learning (CoRL), 2017, pp. 1–16

    2017

  37. [37]

    MetaDrive: Composing diverse driving scenarios for generalizable reinforcement learning,

    Q. Li, Z. Peng, Z. Xue, Q. Zhang, and B. Zhou, “MetaDrive: Composing diverse driving scenarios for generalizable reinforcement learning,”arXiv preprint arXiv:2109.12674, 2021

    Pith/arXiv arXiv 2021

  38. [38]

    A001035: Number of partially ordered sets (“posets

    N. J. A. Sloane, “ A001035: Number of partially ordered sets (“posets”) with n labeled elements. ” [Online]. A vailable: https://oeis.org/A001035

  39. [39]

    Error detecting and error correcting codes,

    R. W . Hamming, “Error detecting and error correcting codes, ”The Bell System T echnical Journal, vol. 29, no. 2, pp. 147–160, 1950

    1950

  40. [40]

    Autonomous vehicle collision reports

    California Department of Motor V ehicles, “ Autonomous vehicle collision reports. ” [Online]. A vailable: https://www.dmv.ca.gov/portal/vehicle-industry- services/autonomous-vehicles/autonomous-vehicle-collision-reports/

  41. [41]

    ScenicNL: Generating probabilistic scenario programs from natural language,

    K. Elmaaroufi, D. Shanker, A. Cismaru, M. V azquez-Chanlatte, A. Sangiovanni- Vincentelli, M. Zaharia, and S. A. Seshia, “ScenicNL: Generating probabilistic scenario programs from natural language,” in1st Conference on Language Modeling (COLM), 2024

    2024

  42. [42]

    Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities,

    G. Comanici, E. Bieber, M. Schaekermann, I. Pasupat, N. Sachdeva, I. Dhillon, M. Blistein, O. Ram, D. Zhang, E. Rosenet al., “Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities, ”arXiv preprint arXiv:2507.06261, 2025

    Pith/arXiv arXiv 2025

  43. [43]

    Proximal policy optimization algorithms,

    J. Schulman, F . W olski, P . Dhariwal, A. Radford, and O. Klimov, “Proximal policy optimization algorithms, ”arXiv preprint arXiv:1707.06347, 2017

    Pith/arXiv arXiv 2017

  44. [44]

    V erifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems,

    T . Dreossi, D. J. Fremont, S. Ghosh, E. Kim, H. Ravanbakhsh, M. V azquez- Chanlatte, and S. A. Seshia, “V erifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems,” inInternational Conference on Computer Aided V erification (CA V). Springer, 2019, pp. 432–442

    2019

  45. [45]

    Rank analysis of incomplete block designs: I. the method of paired comparisons,

    R. A. Bradley and M. E. T erry, “Rank analysis of incomplete block designs: I. the method of paired comparisons, ”Biometrika, vol. 39, no. 3/4, pp. 324–345, 1952. APPENDIXA DETAILEDDEFINITIONS OFSIGNALTEMPORALLOGIC(STL) In this section, we provide the formal definitions of Signal Temporal Logic (STL) [33]: LetT denote the time domain, and x:T→R n be a sig...

    1952

  46. [2023]

    A vailable: https://ieeexplore.ieee.org/document/10051644

    [Online]. A vailable: https://ieeexplore.ieee.org/document/10051644

    arXiv