Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Constrained MDPs and policy safety — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A small expected cost can coexist with frequent finite-horizon violations

Example

Consider a one-state CMDP with actions safe and risky, deterministic self-transition, zero reward, discount $γ = 1 / 10$ , cost $0$ for safe, cost $1$ for risky, and cost threshold $b = 1 / 8$ . The stationary policy chooses risky with probability $1 / 10$ at every decision, with independent action draws in the first seven decisions. Its expected discounted cost is $1 / 9 < 1 / 8$ , so it is feasible, while the probability of at least one cost during those seven decisions is $5,217,031 / 10,000,000 > 1 / 2$ .

Example references

The finite transition model, bounded cost signal, and stationary randomized policy.

Expected discounted-cost feasibility constraint: Expected discounted-cost feasibility is defined by $J_{c}^{π} (μ) \leq b$ .

Facts & Assumptions

Given: One state $s$ , two actions, deterministic self-transition, $γ = 1 / 10$ , cost $c (s, safe, 0, s) = 0$ , cost $c (s, risky, 0, s) = 1$ , threshold $b = 1 / 8$ , and policy probability $1 / 10$ for risky at each step.

[F1]

Finite discounted constrained Markov decision process: a finite CMDP's transition/reward masses and bounded transition-cost signals determine finite-time state and transition masses.

[F2]

Expected discounted-cost feasibility constraint: $J_{c}^{π} (μ)$ is the discounted sum of the finite-time expected costs, and feasibility means $J_{c}^{π} (μ) \leq b$ .

[F3]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: for $0 \leq r < 1$ , $\sum_{t = 0}^{\infty} r^{t} = 1 / (1 - r)$ .

Verification

1.1F1F2F3givenalgebra

At every time $t$ , the state is $s$ and the expected one-step cost is $1 / 10$ . Thus by [F2] and [F3], $J_{c}^{π} (μ) = \sum_{t = 0}^{\infty} (1 / 10)^{t} (1 / 10) = (1 / 10) / (1 - 1 / 10) = 1 / 9$ .

2.1F2step 1.1algebra

Since $1 / 9 < 1 / 8 = b$ , the policy is feasible under the expected discounted-cost constraint.

3.1givenalgebra∎

The probability that all seven independent action draws are safe is $(9 / 10)^{7} = 4,782,969 / 10,000,000$ . Hence the probability of at least one cost is $1 - (9 / 10)^{7} = 5,217,031 / 10,000,000 > 1 / 2$ , as claimed.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A finite sample can report cost satisfaction while the policy violates its expected-cost limit

Example

In a one-state CMDP with $γ = 0$ , cost $1$ for risky and $0$ for safe, let a stationary policy choose risky with probability $1 / 10$ and impose the expected-cost limit $b = 1 / 20$ . The true expected discounted cost is $1 / 10 > b$ . In ten independent one-step rollouts, the empirical mean cost is zero whenever every action is safe, an event of probability $(9 / 10)^{10} = 3,486,784,401 / 10,000,000,000$ .

Example references

A finite CMDP includes bounded transition costs and stationary randomized policies.

Expected discounted-cost feasibility constraint: Expected discounted-cost feasibility is defined by the population objective $J_{c}^{π} (μ) \leq b$ .

Facts & Assumptions

Given: One state, two actions, cost $1$ for risky and $0$ for safe, discount $γ = 0$ , policy probability $1 / 10$ for risky, and threshold $b = 1 / 20$ .

[F1]

Finite discounted constrained Markov decision process: the one-step transition law and cost signal determine the expected cost at each time.

[F2]

Expected discounted-cost feasibility constraint: at $γ = 0$ , the expected discounted cost equals the initial expected one-step cost.

Verification

1.1F1F2givenalgebra

The policy's expected one-step cost is $(1 / 10) \cdot 1 + (9 / 10) \cdot 0 = 1 / 10$ . Since $γ = 0$ , [F2] gives $J_{c}^{π} (μ) = 1 / 10 > 1 / 20 = b$ .

2.1givenstep 1.1algebra∎

Each of the ten independent rollouts is safe with probability $9 / 10$ , so the probability all ten are safe is $(9 / 10)^{10} = 3,486,784,401 / 10,000,000,000$ . On this event the empirical mean is $0 \leq b$ , despite step 1.1 showing that the population constraint is violated.

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

Exact CPO cost feasibility can disagree with a sampled line-search cost check

Example

Assume the Axiom of Choice. In a one-state CMDP with discount $γ = 0$ , let the only costs be $0$ for safe and $1$ for risky, with threshold $b = 1 / 20$ . The old policy chooses risky with probability $1 / 100$ , and the proposed policy chooses it with probability $1 / 5$ . Its exact average KL is less than the radius $δ = 4$ , while its exact expected cost is $1 / 5 > b$ . The ideal single-cost CPO cost surrogate is $J_{c}^{π} + (1 - γ)^{- 1} E_{s \sim d^{π}, a \sim π^{'}} A_{c}^{π} (s, a) \leq b$ ; because $γ = 0$ , the performance theorem makes this surrogate equal to the proposed policy's exact expected cost, so the ideal constraint rejects the proposal. If a one-row rollout sample from the old policy observes safe and supplies zero baseline-cost and advantage estimates, the empirical line-search cost is zero and passes the threshold; this sample occurs with probability $99 / 100$ .

Example references

The finite CMDP and its cost signal.

The cost value and advantage used in the exact idealized constraint.

The empirical surrogate and backtracking sample-cost check.

The exact average-KL performance/cost comparison under AC.

Every family of nonempty sets has a choice function.

Facts & Assumptions

Given: One state $s$ , two actions, a self-transition, zero reward, discount $0$ , cost $c (s, safe, 0, s) = 0$ , cost $c (s, risky, 0, s) = 1$ , threshold $b = 1 / 20$ , old policy $π (risky ∣ s) = 1 / 100$ , and proposed policy $π^{'} (risky ∣ s) = 1 / 5$ .

[A1]

The Axiom of Choice: AC is assumed for the KL form of the policy-performance theorem.

[F1]

Finite discounted constrained Markov decision process: the discounted CMDP has finite transition laws and the stated bounded cost signal.

[F2]

Expected discounted-cost feasibility constraint: with $γ = 0$ , expected discounted cost is the one-step expected cost.

[F3]

Discounted value, action-value, and advantage functions: $V_{c}^{π} (s) = J_{c}^{π} (δ_{s})$ and $A_{c}^{π} (s, a) = Q_{c}^{π} (s, a) - V_{c}^{π} (s)$ .

[F4]

Kullback–Leibler divergence: for finite action probabilities, $D_{K L} (q ∥ p) = \sum_{a} q (a) \log (q (a) / p (a))$ when $q ≪ p$ , with natural logarithms.

[F5]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log x = \int_{1}^{x} d t / t$ for $x > 0$ .

[F6]

Sample-based constrained policy optimization update: the sample line search tests the finite sample cost surrogate supplied with the on-policy batch; it does not test the exact population cost.

[F7]

Policy performance bound by average divergence: when $γ = 0$ , the total-variation remainder is zero, so the exact baseline cost surrogate equals the return difference.

Proof

1.1F1F2givenalgebra

The old expected cost is $J_{c}^{π} (μ) = 1 / 100$ , while the proposed expected cost is $J_{c}^{π^{'}} (μ) = 1 / 5$ . Since $1 / 5 > 1 / 20$ , the exact cost constraint rejects $π^{'}$ .

1.2A1F4F5givenalgebra

By [F4], the average KL at the single state is $K = (1 / 5) \log 20 + (4 / 5) \log (80 / 99)$ . The second logarithm is negative. Also [F5] gives $\log 20 = \int_{1}^{20} d t / t < 19 < 20$ , so $K < (1 / 5) 20 = 4 = δ$ . Thus the proposal satisfies the exact average-KL radius despite violating the exact cost limit.

2.1F2F3F7step 1.1algebra

The ideal CPO cost advantage under $π$ is $A_{c}^{π} (s, risky) = 1 - 1 / 100 = 99 / 100$ and $A_{c}^{π} (s, safe) = 0 - 1 / 100 = - 1 / 100$ . Its exact surrogate is therefore $J_{c}^{π} + (1 - γ)^{- 1} E_{a \sim π^{'}} A_{c}^{π} (s, a) = 1 / 100 + (1 / 5) (99 / 100) + (4 / 5) (- 1 / 100) = 1 / 5 > 1 / 20$ . By [F7], this is the proposed policy's exact expected cost at $γ = 0$ .

3.1F2F6givenstep 1.1algebra∎

Under $π$ , one sampled action is safe with probability $99 / 100$ . On that event the observed cost is zero; choosing the corresponding supplied baseline-cost estimate and cost-advantage estimate as zero makes the sample cost surrogate at $π^{'}$ equal zero. Since $0 \leq b$ , the line search in [F6] accepts this sample check if $π^{'}$ is proposed, even though step 1.1 gives its exact expected cost $1 / 5$ .

CounterexampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

An arbitrary baseline requires the old-policy residual

Statement refuted

For every finite discounted CMDP with immediate reward signal $r (s, a, ρ, s^{'}) = ρ$ , bounded function $f : S \to R$ , and stationary policies $π, π^{'}$ , define

$δ_{f} (s, a, ρ, s^{'}) : = ρ + γ f (s^{'}) - f (s), {\overset{ˉ}{δ}}_{f}^{σ} (s) : = \sum_{a \in A (s)} \sum_{ρ \in R} \sum_{s^{'} \in S} σ (a ∣ s) p (s^{'}, ρ ∣ s, a) δ_{f} (s, a, ρ, s^{'}), σ \in {π, π^{'}},$

$ϵ_{f} : = \max_{s \in S} ∣ {\overset{ˉ}{δ}}_{f}^{π^{'}} (s) ∣, L_{π, f} (π^{'}) : = \frac{1}{1 - γ} \sum_{s \in S} d^{π} (s) {\overset{ˉ}{δ}}_{f}^{π^{'}} (s),$

and

$D_{π, f}^{\pm} (π^{'}) : = L_{π, f} (π^{'}) \pm \frac{2 γ ϵ_{f}}{(1 - γ)^{2}} \sum_{s \in S} d^{π} (s) {TV}_{s} (π^{'}, π), {TV}_{s} (π^{'}, π) : = \frac{1}{2} \sum_{a \in A (s)} ∣ π^{'} (a ∣ s) - π (a ∣ s) ∣,$

where $d^{π}$ is the normalized discounted state occupancy. Then always

$D_{π, f}^{-} (π^{'}) \leq J_{r}^{π^{'}} (μ) - J_{r}^{π} (μ) \leq D_{π, f}^{+} (π^{'}) .$

Statement references

The finite discounted CMDP interface.

The normalized discounted occupancy.

The unnormalized discounted transition-signal return.

Facts & Assumptions

Given: A one-state CMDP $S = {s}$ with one action, deterministic self-transition and reward $1$ , one identically zero cost signal, initial law $μ (s) = 1$ , discount $γ = 0$ , baseline $f (s) = 0$ , and identical policies $π^{'} = π$ choosing the only action with probability one. Powers at time zero have the convention $γ^{0} = 1$ , including $γ = 0$ .

[F1]

Finite discounted constrained Markov decision process: a finite CMDP has a nonempty finite state set, normalized finite transition masses, and bounded transition reward and cost signals.

[F2]

Normalized discounted state occupancy: $d^{π} (s) = (1 - γ) \sum_{t \geq 0} γ^{t} μ_{t}^{π} (s)$ .

[F3]

Expected discounted-cost feasibility constraint: for bounded signal $g$ , $J_{g}^{π} (μ)$ is the unnormalized discounted sum of its finite-time expectations.

Counterexample

Given: The one-state model above and the definitions in the refuted statement.

1.1givenF1F2F3algebra

The deterministic transition and policy masses are normalized, and both the reward and cost are bounded, so this is a finite CMDP. By [F2] its occupancy has $d^{π} (s) = d^{π^{'}} (s) = 1$ at $γ = 0$ . By [F3] both reward returns satisfy $J_{r}^{π} (μ) = J_{r}^{π^{'}} (μ) = 1$ , so $J_{r}^{π^{'}} (μ) - J_{r}^{π} (μ) = 0$ .

2.1givenstep 1.1algebra∎

Since $f = 0$ and the reward is $1$ , the residual is $δ_{f} = 1$ and $ϵ_{f} = 1$ . The stated surrogate is $L_{π, f} (π^{'}) = 1$ . Identical policies have statewise total variation zero, so $D_{π, f}^{-} (π^{'}) = D_{π, f}^{+} (π^{'}) = 1$ . The asserted lower inequality is $1 \leq 0$ , which is false by step 1.1. Subtracting the old-policy residual expectation instead gives the corrected surrogate $1 - 1 = 0$ .

Sources

Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel, Constrained Policy Optimization, PMLR 70 (2017)