Alignment Monitoring

TL;DR

This paper introduces alignment monitoring techniques to ensure probabilistic models accurately predict system behavior in real-time, enhancing the reliability of formal verification for uncertain systems.

Contribution

It proposes novel runtime alignment monitors, including differential and weighted variants, for real-time assessment of model-system alignment in probabilistic systems.

Findings

Monitors are fast and memory-efficient.

They detect misalignment early.

Experimental validation on PRISM benchmarks.

Abstract

Formal verification provides assurances that a probabilistic system satisfies its specification--conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model's predicted and the system's (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.