From 058c81fdb6d8c8d3944fee2e89f04573e989b768 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 25 Jul 2026 17:15:26 +0200 Subject: [PATCH] fix(PACLearning): restrict consistency to realizable samples --- .../PACLearning/VersionSpace.lean | 57 ++++++++++--------- CslibTests.lean | 1 + CslibTests/PACLearning.lean | 56 ++++++++++++++++++ 3 files changed, 87 insertions(+), 27 deletions(-) create mode 100644 CslibTests/PACLearning.lean diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index 5d5f1d178..9083733a4 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -21,8 +21,8 @@ Angluin (1980). - `VersionSpace C S`: the subset of `C` whose concepts agree with `S` on every sample point. -- `IsConsistent A C`: a learner is consistent with `C` if its output always lies - in the version space at the received sample. +- `IsConsistent A C`: a learner is consistent with `C` if its output lies in + the version space at every realizable sample. - `empiricalMiscount h S`: number of sample points where `h` errs (`[DecidableEq β]`). - `empiricalMeasure S`: the uniform Dirac mixture over the sample. - `empiricalError h S`: the empirical distribution's mass on the disagreement set. @@ -35,7 +35,7 @@ Angluin (1980). - `mem_versionSpace_iff_empiricalMiscount_zero`: combinatorial bridge. - `mem_versionSpace_iff_empiricalError_zero`: measure-theoretic bridge. - `IsConsistent.empiricalMiscount_eq_zero`, `IsConsistent.empiricalError_eq_zero`: - consistent learners achieve zero error / miscount on every sample. + consistent learners achieve zero error / miscount on every realizable sample. - `mem_versionSpace_of_realizable`, `Realizable.versionSpace_nonempty`: realizable samples give non-empty version spaces. - `ae_mem_versionSpace_of_realizable`: under iid sampling from a realizable @@ -169,49 +169,52 @@ theorem empiricalError_eq_div [DecidableEq β] simp only [Measure.dirac_apply, Set.indicator, Set.mem_ofPred_eq, Pi.one_apply, smul_eq_mul] rw [Finset.sum_boole, ← ENNReal.div_eq_inv_mul] +/-! ### Realizable Samples -/ + +/-- A labeled sample `S` is *realizable* by concept class `C` if some concept +in `C` labels every sample point correctly. -/ +def Realizable {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : Prop := + ∃ c ∈ C, ∀ i : Fin m, (S i).2 = c (S i).1 + /-! ### Consistent Learners -/ -/-- A learner is *consistent* with the concept class `C` if, on every labeled -sample it receives, its output hypothesis lies in the version space of `C` at -that sample — i.e. the output is in `C` and agrees with every observed -labeled pair. -/ +/-- A learner is *consistent* with the concept class `C` if, on every sample +realizable by `C`, its output hypothesis lies in the version space of `C` at +that sample — i.e. the output is in `C` and agrees with every observed labeled +pair. No condition is imposed on samples that no concept in `C` can realize. -/ def IsConsistent {m : ℕ} (A : Learner α β m) (C : ConceptClass α β) : Prop := - ∀ S : LabeledSample α β m, A S ∈ VersionSpace C S + ∀ S : LabeledSample α β m, Realizable C S → A S ∈ VersionSpace C S -/-- A consistent learner's output is always in the concept class. -/ +/-- A consistent learner's output is in the concept class on every realizable sample. -/ theorem IsConsistent.output_mem_conceptClass {m : ℕ} {A : Learner α β m} - {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) : - A S ∈ C := (hA S).1 + {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) + (hS : Realizable C S) : + A S ∈ C := (hA S hS).1 -/-- A consistent learner's output agrees with the sample on every observed -point. -/ +/-- On every realizable sample, a consistent learner's output agrees with +every observed point. -/ theorem IsConsistent.output_agrees {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) (S : LabeledSample α β m) - (i : Fin m) : - A S (S i).1 = (S i).2 := (hA S).2 i + (hS : Realizable C S) (i : Fin m) : + A S (S i).1 = (S i).2 := (hA S hS).2 i -/-- A consistent learner has zero empirical miscount on every sample. -/ +/-- A consistent learner has zero empirical miscount on every realizable sample. -/ theorem IsConsistent.empiricalMiscount_eq_zero [DecidableEq β] {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} (hA : IsConsistent A C) - (S : LabeledSample α β m) : + (S : LabeledSample α β m) (hS : Realizable C S) : empiricalMiscount (A S) S = 0 := - (mem_versionSpace_iff_empiricalMiscount_zero.mp (hA S)).2 + (mem_versionSpace_iff_empiricalMiscount_zero.mp (hA S hS)).2 -/-- A consistent learner has zero empirical error on every sample. -/ +/-- A consistent learner has zero empirical error on every realizable sample. -/ theorem IsConsistent.empiricalError_eq_zero [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] {m : ℕ} {A : Learner α β m} {C : ConceptClass α β} - (hA : IsConsistent A C) (S : LabeledSample α β m) : + (hA : IsConsistent A C) (S : LabeledSample α β m) (hS : Realizable C S) : empiricalError (A S) S = 0 := - (mem_versionSpace_iff_empiricalError_zero.mp (hA S)).2 - -/-! ### Realizable case -/ + (mem_versionSpace_iff_empiricalError_zero.mp (hA S hS)).2 -/-- A labeled sample `S` is *realizable* by concept class `C` if some concept -in `C` labels every sample point correctly. -/ -def Realizable {m : ℕ} (C : ConceptClass α β) (S : LabeledSample α β m) : Prop := - ∃ c ∈ C, ∀ i : Fin m, (S i).2 = c (S i).1 +/-! ### Realizable Version Spaces -/ /-- *Realizable version-space nonemptiness.* If a target concept `c` lies in `C` and the sample `S` is labeled by `c` (i.e. every `(S i).2 = c (S i).1`), diff --git a/CslibTests.lean b/CslibTests.lean index b26f3aa5d..a2d5d0761 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -12,4 +12,5 @@ import CslibTests.ImportWithMathlib import CslibTests.LTS import CslibTests.LambdaCalculus import CslibTests.MLL +import CslibTests.PACLearning import CslibTests.Reduction diff --git a/CslibTests/PACLearning.lean b/CslibTests/PACLearning.lean new file mode 100644 index 000000000..1bcf17e6f --- /dev/null +++ b/CslibTests/PACLearning.lean @@ -0,0 +1,56 @@ +import Cslib.MachineLearning.PACLearning.VersionSpace + +namespace CslibTests.PACLearning + +open Cslib.MachineLearning.PACLearning + +/-- A learner on two samples over a singleton domain that predicts the first label. -/ +def firstLabelLearner : Learner Unit Bool 2 := + fun S _ => (S 0).2 + +/-- Two different labels for the same point form an unrealizable sample. -/ +def contradictorySample : LabeledSample Unit Bool 2 := + fun i => if i = 0 then ((), false) else ((), true) + +theorem contradictorySample_not_realizable : + ¬ Realizable (Set.univ : ConceptClass Unit Bool) contradictorySample := by + rintro ⟨c, _, hc⟩ + simpa [contradictorySample] using + (hc (0 : Fin 2)).trans (hc (1 : Fin 2)).symm + +/-- Regression: consistency does not require a learner to fit an unrealizable +contradictory sample. -/ +theorem firstLabelLearner_consistent : + IsConsistent firstLabelLearner (Set.univ : ConceptClass Unit Bool) := by + intro S hS + obtain ⟨c, _, hc⟩ := hS + rw [mem_versionSpace_iff] + refine ⟨Set.mem_univ _, fun i => ?_⟩ + change (S 0).2 = (S i).2 + calc + (S 0).2 = c (S 0).1 := hc 0 + _ = c (S i).1 := congrArg c (Subsingleton.elim _ _) + _ = (S i).2 := (hc i).symm + +example : + firstLabelLearner contradictorySample (contradictorySample 1).1 ≠ + (contradictorySample 1).2 := by + simp [firstLabelLearner, contradictorySample] + +/-- A realizable sample used to guard the positive consistency guarantee. -/ +def constantTrueSample : LabeledSample Unit Bool 2 := + fun _ => ((), true) + +theorem constantTrueSample_realizable : + Realizable (Set.univ : ConceptClass Unit Bool) constantTrueSample := by + refine ⟨fun _ => true, Set.mem_univ _, ?_⟩ + intro i + rfl + +example (i : Fin 2) : + firstLabelLearner constantTrueSample (constantTrueSample i).1 = + (constantTrueSample i).2 := + firstLabelLearner_consistent.output_agrees + constantTrueSample constantTrueSample_realizable i + +end CslibTests.PACLearning