Source-linked AI summary
Testing Between the Test Cases: Proving End-to-End Steering in Conditions You Never Drove
Menuka Ghalan, Charles Rodgers, Zachary D. Asher
TL;DR
Automated-driving tests can miss failures between sampled conditions, while formal verification can reason over untested disturbance settings. The paper trains camera-only steering networks in CARLA and uses bound propagation between captured clear and degraded frames; it finds untested potential failures and concludes that formal verification can complement simulation for validation.
Problem
Finite testing can miss long-tail disturbances, and safety standards remain difficult to apply to high-performing E2E policies whose failure modes are not easily enumerated.
Method
The study trains small camera-only steering models in CARLA and applies CROWN bound propagation to frames captured at identical poses, without further simulation.
Results
Formal verification identified conditions that broke the clear-trained policy without closed-loop testing and found potential failure points between tested cases.
Takeaways & Limitations
Formal verification is presented as a viable complement to simulation for automated-driving verification and validation.
Takeaways & Limitations
The study’s evidence is preliminary, and intermediate disturbance-level failures require a further closed-loop testing campaign.
Abstract
from arXiv · showhide
AI-based automated vehicle testing is challenging because a model that passes every test condition can still fail in the real world. Formal verification offers a way to directly address this gap. On a simulated highway and an arterial road we trained two small end-to-end steering networks each in CARLA, one on clear conditions alone and one on clear, fog, night and low sun. All four models were driven against a 2.19 ft lane-departure budget. Without driving again, we used bound propagation, a formal method that reads the trained weights, to compute how far steering can drift at every disturbance strength between two captured images. One calculation covers more than a campaign could drive: on the arterial it spans 133 poses, where ten intensities each would be 10^133 combinations, in minutes on one GPU. Not only did formal verification find conditions that broke the clear-trained policy without simulation testing, it provided some preliminary evidence for potential failures between the test cases. Our overall conclusion is that formal verification is a viable complement to simulation, and could be adopted as a part of verification and validation for automated driving.
1 Introduction
End-to-end driving policies are difficult to reconcile with safety standards and finite testing campaigns because unanticipated disturbances can fall outside both enumerated failure modes and sampled inputs. The paper presents formal verification through bound propagation as a way to guarantee neural-network behavior over mathematically described disturbance sets, including conditions never physically driven.
- Safety-compliance challenge: E2E policies map camera pixels directly to driving commands, but their strong performance makes failure-mode enumeration assumed by safety standards difficult.Relevant standards address functional safety, intended-functionality hazards, AI components, and autonomous products, yet the shared enumeration premise remains difficult for E2E policies.
- Testing gap: Simulation remains central to empirical safety cases, but its finite captured inputs cannot establish behavior over all possible disturbance manifestations.Dedicated adverse-condition datasets, generated inputs, and transferable adversarial examples expand coverage without eliminating the uncountable disturbance space.
- Testing gap: Finite test campaigns cannot enumerate the uncountably many settings of continuously varying disturbances, leaving long-tail physical conditions outside sampled evidence.Changing one disturbance parameter can require rerunning the campaign, while data-driven policies can generalize poorly outside their training distribution.
- Formal verification: Formal verification computes an output range for every input in a mathematically described set, guaranteeing safety when that range remains within the limit.Bound propagation reads trained weights, propagates an input range through the network, and produces a range the output cannot leave.
- Paper contribution: The paper applies formal verification to CARLA-based E2E steering and maps physical disturbances to verifier-bounded input sets, targeting safety-case evidence for conditions nobody drove.The study uses two roads, camera-only sensing, and steering as the learned command, while reconciling per-frame bounds with closed-loop vehicle dynamics.
2 Related Work
Related work places formal verification within efforts to strengthen safety assurance for automated driving beyond vehicle-level testing. It emphasizes that disturbance modeling, rather than solver capability alone, determines whether verification applies to realistic driving conditions.
- Safety assurance: Vehicle-level testing alone cannot provide the confidence required for deployment, motivating formal methods as part of automated-driving assurance.Prior work also estimates that demonstrating a rare-event safety reduction can require billions of test kilometers.
- Formal-methods background: Formal methods have successfully certified deterministic software such as CompCert and seL4, but deep-learning controllers require a different verification paradigm.Interactive theorem provers target explicit rule-based logic, unlike neural-network policies.
- Disturbance modeling: Disturbance modeling limits automated-driving formal methods because standard image-space balls may include images no camera can produce.The related work contrasts imperceptible image modifications and probabilistic guarantees with open macroscopic physical deviations such as global illumination changes.
- Positioning: The paper uses CROWN with input-space branch and bound, requiring trained parameters, architecture, and a renderer for pose-paired simulator disturbances.The method complements abstract interpretation, control reachability, and uncertainty-aware analyses while avoiding high-dimensional ℓ2-ball assumptions in its current one-parameter set.
3 Methodology
The methodology combines CARLA closed-loop driving with formal verification of compact, distilled steering networks across two distinct road environments. It models degraded visibility as bounded image families between matched simulator renders and evaluates sustained steering deviation using subdivided bound propagation.
- 3.1 Simulator, Vehicle, and ODD: Two distinct CARLA operational design domains are evaluated: a grade-separated highway loop and an urban arterial with tighter corners.The highway is Town04 and the arterial is Town06; intersections are excluded from the measurements.
- 3.2 AI Model Development: Teacher–student distillation makes formal verification tractable by verifying only compact ReLU students rather than the larger PilotNet-class teachers.The student uses three strided convolutions and two fully connected layers, while the teacher is used only as a distillation source.
- 3.2 AI Model Development: Four small student steering networks are verified, with one clear-only model and one mixed-condition model trained for each road.The students share a convolutional architecture, while widths and input sizes vary by road; each is distilled from a larger PilotNet-class teacher.
- 3.3 Disturbance Modeling: Each disturbance family interpolates between clear and degraded frames captured at the same simulator pose, with strength s ranging from 0 to 1.The study considers clear, fog, night, and low-sun conditions; captured frames are rendered before cropping and downsampling so they match the network inputs.
- 3.3 Disturbance Modeling: Analytic and dataset-based disturbance models were rejected because they failed to isolate or reproduce the condition-dependent steering response required by the verification family.The evaluated alternatives included a photometric fog model, ACDC paired images from separate drives, and temporally random CARLA rain.
- 3.5 Formal Verification: CROWN bounds each of 16 strength sub-intervals per pose, and the resulting steering bounds are aggregated using the average sustained deviation across the route.Subdividing the one-parameter family tightens the one-sided bounds; the road-average criterion discounts short-lived sign-reversing spikes while retaining persistent bias.
4 Results
Closed-loop testing established baseline behavior, after which CROWN verification compared every disturbance family against the lane-keeping criterion without further simulation. Verification matched observed outcomes and exposed intermediate-strength failures and broader pose-wise risks that endpoint drives could miss.
- 4.1 Closed-Loop Driving: The clear-trained model stayed near zero CTE in clear conditions, while mixed-trained models stayed near zero across mixed conditions; Town06 was more challenging overall.In mixed conditions, the clear-only model failed faster on Town06, while the mixed model had slightly higher CTE there.
- 4.2 Verification: 13×: the arterial clear-trained night case exceeded the tolerance corridor by thirteen times, while refused highway cases escaped it by up to 4×.Certified cases remained well inside the corridor, and both clear-trained models left their lane on every night run.
- 4.2 Verification: 10^133: ten disturbance intensities across 133 arterial poses would create 10^133 combinations, whereas one bound costs a few minutes of GPU time.The bound covers the whole disturbance family, unlike a closed-loop test that evaluates one disturbance value.
- 4.3 Between the Test Cases: Intermediate disturbance strengths revealed arterial failures missed by endpoint testing: fog peaked at 1.01 bias at s⋆=0.41 and low sun at 1.87 at s⋆=0.60.At the rendered condition, the corresponding biases were only 0.69 and 0.37, inside the corridor, although both cases left the lane on every lap.
- 4.3 Between the Test Cases: Pose-wise disturbance profiles also exceeded the corridor for mixed-trained fog and night cases, reaching 1.179 and −1.210 despite both single-strength drives remaining inside it.These profiles assign disturbance strength separately by pose, so they represent a larger question than any one fixed-strength drive.
- 4.3 Between the Test Cases: The study’s evidence remains preliminary: failures at intermediate strengths warrant a dedicated closed-loop campaign to further evaluate and improve formal verification.The authors report that formal verification may identify failures not captured by closed-loop testing.
- 4.4 The Difference Is the ODD: Town06’s greater difficulty was not explained by network capacity, input projection, or random seed, leaving road type and geometry as the remaining variable.The arterial is straighter overall but has tighter minimum-radius corners than the highway, and fog was harder to certify across measured capacities and resolutions.
5 Conclusion
The study applies formal verification to camera-only steering models in CARLA and finds that it predicted highway outcomes while identifying potential failures absent from closed-loop testing. The authors conclude that this approach is viable for a narrow aspect of automated-driving verification, but broader disturbance families remain future work.
- The study trained clear-only and mixed-condition camera-only steering models for Town04 and Town06, then verified disturbance strengths between captured frames.
- Formal verification correctly predicted every highway outcome and identified potential failure points never tested in closed loop.
- The authors provide evidence that formal verification is viable for a narrow aspect of automated-driving verification.
- Future work must widen the mathematical disturbance set to rain, snow, glare, dust, and combinations, while testing verification-predicted failures.
Data Availability
The paper releases its reproducibility artifacts as a versioned software record and separately publishes the captured frames used for bound computation.
- The pipeline, instruments, checkpoints, and artifacts behind the paper’s numbers are released as a versioned software record.
- The captured frames used to compute the bounds are published separately.
Abbreviations
This section defines abbreviations used throughout the paper, including terms for the vehicle, simulator, model architecture, safety concepts, and verification methods.
- AV means autonomous vehicle, CARLA means Car Learning to Act, and E2E means end-to-end.
- CNN, FC, ReLU, RGB, and FOV denote convolutional neural network, fully connected, rectified linear unit, red-green-blue, and field of view.
- CTE, ODD, MSE, and PPC denote cross-track error, operational design domain, mean squared error, and pure-pursuit controller.
- SDP and SMT denote semidefinite programming and satisfiability modulo theories, while SOTIF denotes safety of the intended functionality.