The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

early stopping instrument

DefinitionHalting a boosting run when a held-out score stops improving. The rule reads the held-out fold, so it is a harness and the round count is a fitted parameter. Chapter 7 section 7.5. Also early-stopping.
ExampleBoosting for 200 rounds and keeping round 45, where the held-out score peaked, makes 45 a fitted parameter.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id early-stopping, kind instrument.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equationnone
Assumptions and scope
  • Halting a boosting or gradient run when a held-out score stops improving. The stopping rule reads the held-out fold, so the fold it reads is no longer held out for the reported score, and a scorer that has read the test fold scores it perfectly.
  • Early stopping is a harness. The round count it picks is a fitted parameter, and the report states which fold picked it and which fold scored it.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Leakage.lean, lean/DataMiningAsObservation/CrossValidation.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
00.51050100roundsheld-out scorestop here, chosen on the held-out fold
Halting a boosting run when a held-out score stops improving.

Equation

none

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Chapter 7 section 7.5 of Data Mining as Observation, after ESL 10.12.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Leakage.lean, theorems errors_lookup_eq_zero, lookup_default, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

lean/DataMiningAsObservation/CrossValidation.lean, theorems sizes_sum, accuracy_weighted, accuracy_mean_of_equal, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 7.

Related

harness; leakage; cross-validation; boosting; split.

See also

Book equations stated beside the entry’s terms, not defining it: 8.1, 8.2.

Ledger rows that cite the entry’s records without naming it: NEG-4.

Sources-table rows that share a record with the entry without naming it: chapter 6 section 6.4, chapter 6 section 6.5, chapter 7 section 7.2.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← drifteffective rank →