Rollout improves a sequentially improving heuristic (Prop. 6.4.2)

Proved

BertsekasDP.rollout_sequential_improvement

by Shuze Chen · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

costimprovementrollout

Proposition 6.4.2 (rollout improves on a sequentially improving heuristic). Let the base heuristic $\mathcal{H}$ be sequentially improving, i.e. $\min_{j \in N(i)} H(j) \le H(i)$ at every non-destination node $i$ , and let $(i_1, \dots, i_{\bar m})$ be a path generated by a terminating run of the rollout algorithm $R\mathcal{H}$ from a non-destination node $i_1$ to a destination $i_{\bar m}$ . Then the rollout cost improves on the heuristic,

g(i_{\bar m}) \;\le\; H(i_1),

and is in fact the least of the heuristic cost at the start and at every neighbor visited along the way (Eq. (6.37)):

g(i_{\bar m}) \;=\; \min\Bigl\{\, H(i_1), \; \min_{j \in N(i_1)} H(j), \; \dots, \; \min_{j \in N(i_{\bar m - 1})} H(j) \,\Bigr\}.

This is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, and the ancestor of the improvement step in Monte-Carlo tree search and modern reinforcement learning. The second identity is stronger than the first: it says the rollout has an automatic cost sorting property, always ending at the best destination among all those its base heuristic proposed along the run, so it can exhibit good behavior that the base heuristic alone never would.

Formalization Note The equality is phrased as a least element (IsLeast) of the displayed set, which asserts both that $g(i_{\bar m})$ is a lower bound and that it is attained by one of the listed values. Ties in the neighbor selection are permitted; the run is any complete node sequence satisfying the rollout selection rule.

Preamble

import Mathlib
import Definitions.Def_BertsekasGraphSearch

Formal statement

namespace BertsekasDP

theorem rollout_sequential_improvement {V : Type} [Fintype V] [DecidableEq V]
    (G : BertsekasGraphSearch V) (H : BertsekasBaseHeuristic G)
    (himp : BertsekasSeqImproving G H)
    (l : List V) (hrun : BertsekasIsRolloutRun G H l)
    (i₁ : V) (hhead : l.head? = some i₁) (hstart : i₁ ∉ G.dest)
    (d : V) (hlast : l.getLast? = some d) :
    G.cost d ≤ BertsekasHeurCost G H i₁ ∧
    IsLeast {c : ℝ | c = BertsekasHeurCost G H i₁ ∨
        ∃ v ∈ l.dropLast, ∃ j ∈ BertsekasNbrs G v, c = BertsekasHeurCost G H j}
      (G.cost d) := by sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 6.4.2

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $V$ be a finite type with decidable equality, $G$ a graph structure, $H$ a base heuristic, and assume BertsekasSeqImproving holds for $(G,H)$ (at every non-destination vertex with at least one out-neighbour, the minimum of $\hat H$ over out-neighbours is $\le \hat H$ at the vertex itself). Suppose $l$ is a list satisfying BertsekasIsRolloutRun for $(G,H)$ ; $i_1$ is the first element of $l$ , with $i_1 \notin G.\mathrm{dest}$ ; and $d$ is the last element of $l$ . The conclusion is a conjunction:

$G.\mathrm{cost}(d) \le \hat H(i_1)$ : the vertex cost of the run's final (destination) vertex is at most the heuristic cost of the starting vertex.
$G.\mathrm{cost}(d)$ is the least element (membership plus lower bound, in the IsLeast sense) of the set

\Big\{ c \in \mathbb{R} \;\Big|\; c = \hat H(i_1) \;\lor\; \exists\, v \in l',\ \exists\, j \in \mathcal{N}(v),\ c = \hat H(j) \Big\},

where $l'$ is $l$ with its last element removed: the set consisting of $\hat H(i_1)$ together with the heuristic costs of all out-neighbours of all non-final vertices of the run. Conjunct (1) is the special case of the lower-bound half of (2) applied to the element $\hat H(i_1)$ ; the statement nevertheless asserts both explicitly. The proof is left as sorry.

Human review

Endorsed by Community (Bot) · Sep 11, 2026
Endorsed by Shuze Chen · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph