feat(MachineLearning/PACLearning): add VersionSpace abstraction#592
Open
Zetetic-Dhruv wants to merge 1 commit into
Open
feat(MachineLearning/PACLearning): add VersionSpace abstraction#592Zetetic-Dhruv wants to merge 1 commit into
Zetetic-Dhruv wants to merge 1 commit into
Conversation
Adds the classical version space abstraction (Mitchell 1982, Angluin 1980) to the PAC learning module. Version space — the subset of a concept class consistent with observed labeled data — is the structural substrate every sample complexity theorem operates on (Baby PAC, Sauer-Shelah, PAC lower bounds, NFL). This PR complements leanprover#492 by providing: - VersionSpace C S: the consistent subset of C given sample S - versionSpace_subset, versionSpace_empty_sample: sanity lemmas - versionSpace_antitone: structural monotonicity (more data → smaller VS), dual to sample complexity monotonicity - IsConsistent A C: predicate on learners (output always in version space) - IsConsistent.output_mem_conceptClass, output_consistent: consistent learner properties - mem_versionSpace_of_realizable: under realizable data, the target concept lies in the version space (the realizable-case bridge) - versionSpace_nonempty_of_realizable: corollary No measure theory, no new Mathlib dependencies, ~150 lines, 0 sorry. Together with leanprover#492 these suffice to state the Baby PAC theorem, Sauer-Shelah sample complexity, PAC lower bounds, and NFL as structural statements rather than ad-hoc computations.
Author
SamuelSchlesinger
suggested changes
May 22, 2026
Contributor
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
I want to see the bridge that makes this useful: version-space membership is exactly zero empirical error. I think that is what will motivate this PR and make the downstream work easier. The stuff you do have is sound and I appreciate this PR overall, my requests are mostly just stylistic commentary and generalization requests.
| /-- *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`), | ||
| then `c` itself lies in the version space `VersionSpace C S`. -/ | ||
| theorem mem_versionSpace_of_realizable {m : ℕ} {C : ConceptClass α β} |
Contributor
There was a problem hiding this comment.
Lets take c implicit here to match the following theorem.
Contributor
There was a problem hiding this comment.
I also think something like:
theorem ae_mem_versionSpace_of_realizable
[MeasurableSpace α] [MeasurableSpace β]
{C : ConceptClass α β} {c : α → β} (hc : c ∈ C) (hcm : Measurable c)
(P : Measure α) [IsProbabilityMeasure P] (m : ℕ) :
∀ᵐ S : LabeledSample α β m
∂(Measure.pi (fun _ : Fin m => P.map (fun x => (x, c x)))),
c ∈ VersionSpace C S := ...
might be desirable here?
|
|
||
| @[expose] public section | ||
|
|
||
| /-! # Version Space |
Contributor
There was a problem hiding this comment.
Lets move this above the section to match the rest of the files in cslib.
|
|
||
| /-- A consistent learner's output agrees with the sample on every observed | ||
| point. -/ | ||
| theorem IsConsistent.output_consistent {m : ℕ} {A : Learner α β m} |
Contributor
There was a problem hiding this comment.
Lets rename this to output_agrees or just output cause Consistent is already in the namespace.
| pages = {203--226}, | ||
| year = {1982}, | ||
| doi = {10.1016/0004-3702(82)90040-6} | ||
| } |
Contributor
There was a problem hiding this comment.
I think we should cite "Version Spaces: A Candidate Elimination Approach to Rule Learning" instead, or at least in addition.
| (S : LabeledSample α β n) : | ||
| VersionSpace C S ⊆ VersionSpace C (fun i => S (Fin.castLE hmn i)) := by | ||
| intro h hh | ||
| exact ⟨hh.1, fun i => hh.2 (Fin.castLE hmn i)⟩ |
Contributor
There was a problem hiding this comment.
Lets generalize this, something like:
theorem versionSpace_reindex {m n : ℕ} (f : Fin m → Fin n)
(C : ConceptClass α β) (S : LabeledSample α β n) :
VersionSpace C S ⊆ VersionSpace C (S ∘ f) :=
fun _ hh => ⟨hh.1, fun i => hh.2 (f i)⟩
this theorem pops out with f := Fin.castLE hmn.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the classical version space abstraction (Mitchell 1982, Angluin 1980) as a companion to the PAC learning definitions from #492.
VersionSpace C S: the subset ofCwhose concepts agree withSon every sample pointversionSpace_subset,versionSpace_empty_sample: sanity lemmasversionSpace_antitone: more data gives a smaller version spaceIsConsistent A C: predicate on learners whose output always lies in the version spacemem_versionSpace_of_realizable,versionSpace_nonempty_of_realizable: realizable-case bridgeFoundation for downstream proofs (Sauer-Shelah, PAC lower bounds, infinite NFL).