Alignment Monitoring
Thomas A. Henzinger, Konstantin Kueffner, Vasu Singh, I Sun

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Software Engineering Methodologies · Software System Performance and Reliability
