Technical Summary: Safety-Constrained Reinforcement Learning with Post-Training Reachability Verification for Robot Navigation

1. Problem Formulation

The paper addresses the critical challenge of deploying autonomous mobile robots in cluttered environments where perception uncertainty (e.g., sensor noise) can lead to catastrophic failures. The authors argue that standard Reinforcement Learning (RL) safety metrics, which rely on average cumulative cost, are insufficient because they mask "tail-risk" behaviors—rare but high-consequence events where a policy might collide despite having a low average cost.

The problem is formalized as a Constrained Markov Decision Process (CMDP). Unlike traditional CMDPs that constrain the expected cumulative cost $E[C_\pi] \leq b$, this work seeks a policy $\pi$ that maximizes expected reward while satisfying a Conditional Value-at-Risk (CVaR) constraint:
$$\max_{\pi} J_R(\pi) \quad \text{s.t.} \quad \text{CVaR}_\alpha(C_\pi) \leq b$$
Here, $\text{CVaR}_\alpha$ represents the expected cost in the worst $(1-\alpha)$ fraction of episodes, explicitly targeting the tail of the cost distribution rather than the mean.

Furthermore, the paper identifies a gap between statistical training guarantees and formal safety verification. A policy with favorable CVaR statistics may still produce unsafe actions under bounded observation uncertainty. Therefore, the goal is to unify risk-sensitive training with post-training neural network reachability verification to ensure that the policy's action outputs remain within safety margins even when inputs are perturbed.

2. Methodology: The VIA Framework

The proposed framework, VIA (Verification-Informed safe reinforcement learning for Autonomous navigation), operates in two distinct phases:

Phase I: CVaR-Constrained Off-Policy Training

The authors adapt the TD3 (Twin Delayed DDPG) off-policy algorithm to optimize for CVaR constraints. Key technical components include:

• State Augmentation: To estimate CVaR in an off-policy setting, the state space is augmented with a dynamic cost budget variable $e_t$. The augmented state is $\bar{s}_t = (s_t, e_t)$, where $e_t$ tracks the accumulated cost history, allowing the critic to distinguish between states reached under different cost histories.
• Distributional Cost Critic: Instead of estimating a single expected cost value, the cost critic $Q^C_\phi$ outputs $M$ quantiles of the cumulative cost distribution. To prevent the "crossing problem" (where predicted quantiles violate monotonicity), a noncrossing quantile logit network is employed using a specific parameterization involving cumulative softmax summation.
• Adaptive VaR Update: A critical challenge in off-policy CVaR optimization is tracking the Value-at-Risk (VaR) quantile threshold without on-policy evaluations. The authors introduce a gradient-free update rule for the VaR parameter $u$ based on the empirical exceedance probability of costs in the replay buffer, ensuring stable convergence toward the target quantile.
• Lagrangian Optimization: The policy is optimized using a Lagrangian relaxation of the CVaR-constrained objective. The actor loss combines the task reward critic and the estimated CVaR cost, weighted by a Lagrange multiplier $\lambda$ that is updated based on the empirical constraint slack.

Phase II: Post-Training Reachability Verification

After training, the framework performs a formal safety assessment using POLAR (Polynomial Arithmetic for Reachability), a tool that combines Taylor Model (TM) arithmetic with Bernstein polynomial interpolation.

• Reachability Analysis: Given bounded observation uncertainty $\epsilon$, the method propagates TMs through the trained neural network to compute a guaranteed action reachable set $A(s, \epsilon)$. This set represents all possible actions the policy could output given the input uncertainty.
• Safety Rate Metric: The authors define a Safety Rate metric. For a given state, they sample actions from the bounds of the reachable set (including endpoints and midpoints) and simulate the robot's motion. A state is "verified safe" if all sampled actions result in collision-free trajectories. The Safety Rate is the proportion of evaluated states that satisfy this criterion.
• Integration: The paper posits that CVaR-constrained training naturally shapes the policy toward conservative, tightly bounded action distributions, making the resulting reachable sets smaller and more amenable to formal verification compared to expectation-based baselines.

3. Key Contributions

1. CVaR-Constrained TD3 Framework: The design of an off-policy CVaR optimization framework featuring a distributional cost critic with noncrossing quantile regression and an adaptive VaR update mechanism to stabilize quantile convergence.
2. Verification-Informed Safety Metric: The development of a safety verification framework combining POLAR reachability analysis with layered safety boundaries, introducing the Safety Rate metric to quantify policy robustness under bounded observation uncertainty.
3. Empirical Validation: Comprehensive validation in simulation across ten navigation scenarios and six baselines, as well as successful sim-to-real transfer on a physical Clearpath Jackal robot.

4. Experimental Results

Experiments were conducted in a Gazebo simulation (10m $\times$ 10m arena with obstacles) and on a physical robot.

• Performance vs. Baselines: VIA achieved the highest Success Rate (98.3%) and the lowest Collision Rate (1.7%) among all compared methods (including TD3, SAC-Lagrangian, RCPO, WCSAC, and CVaR-CPO).
• Divergence of Metrics: A key finding is the divergence between average cost rankings and reachability-based safety rankings. For instance, RCPO achieved the lowest average cost (1.17) but a lower Safety Rate (98.5% for successful episodes) compared to VIA (99.6%). This demonstrates that average cost metrics can miss latent risks that formal verification captures.
• Impact of $\alpha$: Ablation studies showed that increasing the CVaR confidence level $\alpha$ (focusing on more extreme tails) improved both success rates and safety metrics, with $\alpha=0.9$ yielding the most conservative and robust performance.
• Sim-to-Real Transfer: When deployed on a Clearpath Jackal robot, the success rate dropped to 90.0% due to physical noise and delays, but the Overall Safety Rate remained nearly identical to simulation (99.2% vs. 99.1%), confirming that the policy maintains verified safety margins in the real world.

5. Significance and Claims

The paper claims that reachability verification captures risks missed by empirical cost metrics alone. By combining risk-sensitive training (CVaR) with formal post-training verification, the authors demonstrate that policies can be trained not just to be safe on average, but to maintain safety margins under uncertainty.

The authors state that this work is the first to integrate CVaR-constrained policy optimization with neural network reachability verification specifically for robot navigation. They emphasize that while formal verification is computationally expensive and typically limited to low-dimensional or small networks, their approach uses lightweight architectures to enable this integration.

The paper concludes modestly, acknowledging that the reliance on Taylor Model arithmetic restricts the complexity of the verifiable policy networks. Future work is identified as exploring GPU-accelerated reachability methods and integrating verification signals directly into the training loop for closed-loop safety optimization.