Youden F1 bound correction

Equation

Book equation 5.4.

\[\begin{gathered} F_1^{\max}\ \le\ \sup_{t\in[J,\,1]}\ \frac{2t\pi}{t\pi+\pi+(t-J)(1-\pi)},\qquad J=\max_{\tau}\big(\mathrm{TPR}-\mathrm{FPR}\big),\qquad \pi=\text{prevalence}, \\ J\le 2A-1\ \text{when the ROC curve is concave, and not in general.} \end{gathered}\]

Conditions

• The Youden form holds for every score with a finite sample.
• The AUROC form holds for concave ROC curves, and as a pruning bound it is safe only there.
• Inside a tree search either form bounds the formula itself and not its descendants, so pruning a subtree by its root’s ceiling is a heuristic in both cases.

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

Ledger

none

First stated

The AUROC form, theorem “AUROC-F1 Bound” in theory-radar/paper/astar_paper.tex and the derivation in theory-radar/src/symbolic_search/_auroc_proof.py, repository DOI 10.5281/zenodo.20660206. The corrected form at theory-radar 1b3d105.

Measurements

Rerun of the A* paper’s pruning tables by theory-radar/rerun_youden_2026_09_03.py. Part A is depth-2 pairwise enumeration on eight datasets, exhaustive against the AUROC pre-filter at seven thresholds and against Youden pruning. Part B is the depth-3 A* search with 50,000 expansions in strict mode (no pre-filter), the published fast mode (AUROC pre-filter at 0.52), and the youden mode.

Part A, recorded at commit aedc053 of theory-radar.

Part B.

Failures and corrections

• theory-radar/ERRATA.md:3-75 at 37c4e6c. 2026-09-03. The AUROC to F1 bound holds only for concave ROC curves What was claimed. Theorem “AUROC-F1 Bound” in paper/astar_paper.tex, the derivation in src/symbolic_search/_auroc_proof.py, and the pruning bounds in run_astar_v2.py and src/symbolic_search/_heuristic_dag.py all rested on the statement that any ROC curve with area A has maximum Youden index J = max(TPR − FPR) at most 2A − 1. Why it is wrong. The statement holds for concave ROC curves (equivalently, scores whose likelihood ratio is monotone), because a concave curve lies above the two chords through its Youden point and so has area at least (1 + J)/2. It fails for non-concave curves. Counterexample, found by an external reviewer of the companion textbook: rank three quarters of the positives above every negative and the remaining quarter below every negative. AUROC is 0.75, the maximum Youden index is 0.75, and at prevalence one half the best thresholded F1 is 0.857, above the 0.80 the AUROC form of the ceiling allows. The sound ceiling for that score, from J = 0.75, is 0.889, and the score sits under it. The auroc_f1_bound formula in run_astar_v2.py, 2Aπ/(Aπ + (1 − A)(1 − π)), is not a valid upper bound either: at prevalence 0.1 the same score reaches F1 0.857 against a “bound” of 0.5. Consequence for reported results. The searches that used these bounds to prune could have discarded a candidate formula whose ROC curve was not concave and whose true best F1 exceeded the computed ceiling. The formulas and wins reported by those runs are therefore what a pruned search found, and are lower bounds on what an unpruned search would find. The Monotone Invariance Theorem and the results that do not depend on the AUROC bound are unaffected. Correction. The sound form of the ceiling substitutes the measured maximum Youden index of the candidate’s own scores for 2A − 1. It holds for every score, costs the same sort as AUROC, and is what max_f1_for_youden and youden_f1_bound now compute. The AUROC form is retained under its original names with a docstring stating the concavity condition, and the pruning sites now use the measured index. A rerun of the published searches under the corrected bound was done on 2026-09-03 and 2026-09-04, rerun_youden_2026_09_03.py, results in results/rerun_youden_2026_09_03.json, run on the Atlas workstation, CPU only. Rerun, part A, the pre-filter admissibility table (tab:auroc). Depth-2 pairwise enumeration on the eight datasets, exhaustive against the AUROC pre-filter at the seven published thresholds, with the sound Youden ceiling beside it. The evaluation counts under the pre-filter reproduce the published table (Breast Cancer 8700 pairs, 2576 evaluated at 0.75; Wine 1560, 413; Circles 20, 4; Moons 20, 2). The pre-filter lost no optimum on any dataset at any threshold, which is what the paper reported. That was luck of the data, not the theorem: the retracted ceiling sat below the F1 a pair formula actually reach

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/YoudenF1.lean, theorems f1_eq, f1_le_of_youden, auroc_eq, youden_eq, youden_exceeds_auroc_form, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 5.

Related

Monotone Invariance Theorem; formula search; safe pruning; Apriori principle.

See also

none

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.