ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

DAgger queries expert labels on learner-visited states

Example

Use states $g, b$ , initial state $g$ , actions $A (g) = {c, e}$ and $A (b) = {r, e}$ , and deterministic transitions/costs: at $g$ , $c$ returns to $g$ with cost $0$ and $e$ moves to $b$ with cost $1$ ; at $b$ , $r$ moves to $g$ with cost $0$ and $e$ returns to $b$ with cost $1$ . The expert chooses $c$ at $g$ and $r$ at $b$ . The learner class contains two deterministic policies: $π^{b a d}$ chooses $e$ at both states, and $π^{g o o d}$ chooses $c$ at $g$ and $r$ at $b$ . Run two DAgger rounds with horizon $T = 2$ , one trajectory per round, expert-use probabilities $β_{1} = β_{2} = 0$ , initial policy $π^{b a d}$ , and statewise 0–1 disagreement loss. The round-1 rollout visits $g$ and then $b$ ; DAgger queries the expert at both states, aggregates the labels $(g, c)$ and $(b, r)$ , and fits $π^{g o o d}$ as the unique minimum-loss policy. The second rollout then remains at $g$ . The label $(b, r)$ could not be obtained from expert-only demonstrations because the expert stays at $g$ .

The diagram labels each deterministic transition by action/task-cost and marks the initial state; the expert and the two learner policies are specified in the text.

diagram failed to render:
\begin{tikzpicture}[>=stealth]
  \node[draw,circle] (g) at (0,0) {$g$};
  \node[draw,circle] (b) at (4,0) {$b$};
  \draw[->] (-1.5,0) -- (g) node[midway,above] {start};
  \draw[->] (g) edge[loop above] node[above] {$c/0$} (g);
  \draw[->] (g) to[bend left=18] node[above] {$e/1$} (b);
  \draw[->] (b) edge[loop above] node[above] {$e/1$} (b);
  \draw[->] (b) to[bend left=18] node[below] {$r/0$} (g);
\end{tikzpicture}

Example references

Ross, Gordon, and Bagnell, A Reduction of Imitation Learning and Structured Prediction to No-Regret Online Learning: Algorithm 3.1, §3, PDF p. 3.

Bagnell, Boots, and Choudhury, Modern Adaptive Control and Reinforcement Learning, Chapter 6: PDF pp. 4–6 / printed pp. 57–59.

Facts & Assumptions

Given: The two-state MDP, expert, learner class, two DAgger rounds, and loss in the Example.

[F1]

Finite-horizon imitation learning and expert-surrogate loss: the deterministic expert label at state $s$ is $π^{*} (s)$ , and DAgger's training loss evaluates candidate policies on labeled states.

[F2]

Dataset Aggregation (DAgger): each round executes the current expert/learner mixture, queries the expert on every visited state, aggregates the labels, and updates by minimizing cumulative empirical loss.

[A1]

$T = 2$ , $m = 1$ , $N = 2$ , $β_{1} = β_{2} = 0$ , and the initial learned policy is $π^{b a d}$ .

Verification

1.1A1F1F2construct

With $β_{1} = 0$ , the first round executes $π^{b a d}$ . From $S_{0} = g$ it takes $e$ to $S_{1} = b$ ; at both visited states the expert labels are $c$ at $g$ and $r$ at $b$ . By [F2], both labeled pairs enter the aggregate dataset.

2.1A1F2step 1.1algebra

On this two-example dataset, $π^{g o o d}$ has total 0–1 loss $0$ , while $π^{b a d}$ disagrees on both labeled states and has loss $2$ . Thus the unique FTL minimizer is $π^{g o o d}$ , which is the next policy.

3.1A1F1F2step 2.1algebra∎

In round 2, $β_{2} = 0$ and $π^{g o o d}$ takes $c$ at $g$ , so the state remains $g$ and the expert label is $c$ . Adding this pair preserves $π^{g o o d}$ as the unique zero-loss minimizer. Since the expert itself remains at $g$ on every expert-only rollout, it never labels $b$ ; the first interactive DAgger round supplies that missing recovery label.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stéphane Ross, Geoffrey J. Gordon, and J. Andrew Bagnell, A Reduction of Imitation Learning and Structured Prediction to No-Regret Online Learning (standard reference, not scraped)
James A. Bagnell, Byron Boots, and Sanjiban Choudhury, Modern Adaptive Control and Reinforcement Learning, Chapter 6: An Invitation to Imitation (standard reference, not scraped)