An Attention Mechanism for Probabilistic Zero-Shot Monitoring of Formal Languages

The deployment of autonomous systems raises the question of how safety-relevant properties can be assured at runtime. This is a challenging task for vision-based systems, in which safety-relevant quantities must be inferred from raw sensor data; the need for suitable solutions to this problem is reinforced by the increasing use of end-to-end policies, such as VLAs. We seek a monitor that a user can prompt with any property expressed in a formal language (a machine-interpretable specification language) and that predicts its satisfaction probability from the observation history zero-shot, i.e., without training on the specific property. We cast monitoring as attention over potential futures: the property acts as a mask over candidate futures in the chosen language, whilst a predictive state representation captures the probabilities of a fixed set of short candidate futures given the observation history. Via a linear decoder, attention over these short futures collapses into one fixed weight vector compiled from the property's syntax. Hence, one learned representation serves any property without property-specific data or training. Whilst the number of potential futures grows exponentially in the time horizon of the property, our monitor only evaluates an inner product at runtime at a cost independent of the horizon. Lastly, we compute calibrated error bounds for learned predictive state representations; a new property needs no new data or model training, only recalibration on stored calibration labels. We validate the zero-shot capabilities of our monitor on driving data spanning agent tracks, rendered bird's-eye views, and raw camera frames. We attain $91$ to $93$% of the predictive skill of reference monitors which are trained separately for each property, answering each frame as it arrives at $9$ to $150$ times lower cost than a sampled autoregressive baseline.