Backward-Reachability Distance Head

(1) Add a small r-dimensional distance head to the shared encoder of an actor-critic model. The main actor and critic remain unchanged; the new head receives observation x and predicts one modal distance per requirement. The environment wrapper maintains q and exposes it only for producing training labels, not as an input, so the experiment tests whether the observation contains enough information. (2) Construct W_i and d_i offline using the same reverse graph traversal as the shield. During rollout store x_t, q_t, x_{t+1}, q_{t+1}, and the action. In each minibatch compute a Huber regression loss against clip(d_i(q_t),0,D), with D such as 20 for unreachable states. For each mode with finite d_i(q_t)>0, add the progress term [h_i(x_{t+1})-h_i(x_t)+1]_+. Mask this term at marked states and for transitions leaving M_i. Optimize the standard PPO or SAC loss plus lambda_d times distance loss and lambda_p times progress loss; start with lambda_d=0.1 and lambda_p=0.05, then anneal if policy learning degrades. (3) Distances are computed exactly from the finite monitor; model uncertainty and observation aliasing are measured by distance prediction error. If observations are partially observed, replace the head with a GRU head and compare. (4) First experiment on procedurally generated MiniGrid layouts with sparse rewards, hazards, and two simultaneous goals. Compare PPO with no auxiliary task, distance supervision only, and distance plus progress loss using equal rollout budgets. Success signals are faster first-goal and final-goal attainment, lower critic loss variance, fewer blocking states, and better held-out-layout performance.