Value Functions as Supermartingale Certificates

Can We Turn an AI's Score Into a Mathematical Guarantee?

In autonomous systems, we face a tension between performance and safety. We use Reinforcement Learning (RL) to train agents. These agents optimize for a score called a value function (the expected total discounted reward). However, they lack inherent logical guarantees. Researchers have found a way to bridge this gap. They turn the "score" an AI uses to learn into a formal mathematical proof. This allows us to guarantee that an agent satisfies specific safety rules. This works even in complex or infinite environments.

The Question

The authors investigate a disconnect in formal methods. On one side, we have certification methods for stochastic systems (systems with inherent randomness). These methods use "supermartingale certificates." These are real-valued functions that act as mathematical proof rules. They ensure a system satisfies $\omega$-regular properties (logic specifications describing infinite sequences of events). On the other side, we have Reinforcement Learning. RL excels at finding policies (strategies for choosing actions) for these tasks. But RL lacks formal guarantees that a trained policy adheres to logic.

The central question is: Can the value function actually serve as a formal proof certificate? Specifically, can it encode a Streett supermartingale (a certificate for $\omega$-regular properties)?

Why The Old Answer Was Incomplete

These two fields historically operated in separate silos. If you wanted formal guarantees, you used constrained optimization to synthesize certificates. This approach is mathematically rigorous. However, it scales poorly. It struggles as state spaces grow or become continuous (represented by real numbers).

Conversely, RL for Linear Temporal Logic (LTL) tasks typically synchronizes the agent's state with an automaton (a state machine representing logic). This helps the agent learn. But it does not provide a certificate. Even if the agent finds an optimal policy, we cannot formally prove it satisfies the specification. This is true except in very restricted finite state spaces. We can optimize for the probability of success, but we cannot certify absolute satisfaction.

What They Did

The researchers propose two distinct reward designs. These designs force the value function to take on the properties of a certificate.

The first is the "Absorbing Set Reward Design." This requires knowing the absorbing sets (regions where the agent stays indefinitely) induced by the policy. The second is the "Specification-Only Reward Design." This is more practical for deployment. It requires only knowledge of the LTL specification. This second method uses a "state-dependent discount factor." This means the agent's sense of time only decays when interacting with reward-bearing regions.

The authors tested these theories on a stochastic grid-world MDP (a discrete environment with probabilistic movement). They evaluated LTL specifications across the Manna-Pnueli hierarchy (a classification of logic complexity). They compared synthesized certificates against the PRISM model checker. PRISM is a standard tool for probabilistic verification.

What They Found

The authors report that the theoretical connection holds. Under the proposed reward designs, the value function $V^\pi$ transforms into a Streett supermartingale $W$. This uses the relation $W(s) := C - V^\pi(s)$. Here, $C$ is a constant related to the discount factor.

In their experiments, the results were decisive. For policies that satisfied the LTL specifications, the synthesized certificates were valid [Table 1]. For policies that failed the task, the certificates were invalid [Table 1]. As shown in, the certificate for the task $F b \wedge G \neg h$ behaves as expected.

The certificate values strictly decrease in expectation as the agent moves toward the target. This satisfies the mathematical requirements for a proof. The authors confirmed that for satisfying policies, the satisfaction probability was $1.0$. This matched the PRISM model checker results.

What This Changes

This work shifts formal verification from constrained optimization to policy evaluation. Policy evaluation is a much more scalable process.

If this generalizes to high-dimensional spaces, the implications are significant. It suggests a "principled route" to certified RL. Instead of baking safety into the training loop via constraints, we can train an agent and then extract a certificate. It also provides a diagnostic tool. If a neural network's value function fails the supermartingale proof rules, it indicates approximation error.

However, the paper does not yet address the "noise" of deep learning. In practice, we use neural networks to approximate value functions. These approximations are never perfect. The authors note that investigating how estimation error impacts certificate validity is a critical next step. A researcher should attempt to synthesize a certificate using a Deep Q-Network (DQN) in a continuous environment. This would test if the "proof" survives the transition from exact math to neural approximation.

Figures from the paper