Pipeline-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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Active querying, version spaces, and abstention

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite pool-based realizable active-learning instance

Definition

Let $(X, Σ)$ be a nonempty measurable space, let $D_{X}$ be a probability measure on it, and let $H$ be a finite nonempty set of measurable classifiers $h : X \to {0, 1}$ . A finite pool-based realizable active-learning instance consists of an ordered pool $U = (u_{1}, \dots, u_{m}) \in X^{m}$ for some $m \geq 0$ , an unknown target $h^{*} \in H$ , and a deterministic exact label oracle $O : X \to {0, 1}$ satisfying $O (x) = h^{*} (x)$ at every queried point. A fresh feature $X \sim D_{X}$ has target label $h^{*} (X)$ ; the pool itself need not be sampled from $D_{X}$ . For a set $Q \subseteq {1, \dots, m}$ of queried indices with observed labels $(y_{i})_{i \in Q}$ , the version space is $V (Q, y) = {h \in H : h (u_{i}) = y_{i} for every i \in Q}$ . For any $V \subseteq H$ , its disagreement region is $DIS (V) = {x \in X : \exists h, g \in V, h (x) \neq g (x)}$ . Since $V$ is finite and every classifier is measurable, $DIS (V)$ is measurable. The pointwise exact-oracle assumption is stronger than standard distributional PAC realizability: zero population risk only requires agreement almost surely under the joint law and does not prescribe oracle values at every pool point.

Definition references

Supervised prediction problems: supplies the measurable instance and label spaces, measurable predictors, and joint-law framework specialized here to binary labels.

Realizable and agnostic PAC learning: defines standard PAC realizability by a finite-class member of zero population risk; that almost-sure condition alone does not prescribe pointwise labels on arbitrary pool entries.

Steve Hanneke, Theory of Active Learning, version 1.1, §§2.1–2.2 and §5.1

Daniel Joseph Hsu, Algorithms for Active Learning, Chapter 2

AlgorithmAlgorithm: AI-adaptedProof: Not applicableOpen item page →

Finite-pool version-space query procedure

Definition

Input a finite pool-based realizable active-learning instance with ordered pool $U = (u_{1}, \dots, u_{m})$ and a nonnegative integer query budget $b$ . Initialize the current version space $V = H$ , query count $q = 0$ , pool index $i = 1$ , an empty query log, and an empty status record for each pool index. While $i \leq m$ , first check whether every $h \in V$ gives the same label at $u_{i}$ . If so, record that unanimous label as a prediction and set $i \leftarrow i + 1$ , even when $q = b$ . Otherwise, if $q = b$ , mark indices $i, i + 1, \dots, m$ as abstentions and return the current $V$ , records, and query log. If instead $q < b$ , query $y = O (u_{i})$ , append $(i, y)$ to the query log, record the queried label, replace $V$ by ${h \in V : h (u_{i}) = y}$ , set $q \leftarrow q + 1$ and $i \leftarrow i + 1$ , and, if now $q = b$ , mark all remaining indices $i, \dots, m$ as abstentions and return. If the scan reaches $i = m + 1$ , return the current $V$ , records, and query log. The query budget limits oracle calls; the procedure scans each pool index at most once and reports unresolved suffix entries as abstentions when it stops at the budget.

Definition references

Finite pool-based realizable active-learning instance: fixes the measurable binary classifier class, finite ordered pool, pointwise exact target oracle, version spaces, and disagreement region used by this procedure.

Steve Hanneke, Theory of Active Learning, version 1.1, §5.1

Daniel Joseph Hsu, Algorithms for Active Learning, Chapter 2 §§2.1–2.2

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Finite-pool version-space invariant and query bound

Statement

Let $H$ be a finite nonempty class of binary classifiers, let $U = (u_{1}, \dots, u_{m})$ be a finite ordered pool with $m \geq 0$ , let $h^{*} \in H$ , let the deterministic oracle return $h^{*} (u_{i})$ at every query, and run the finite-pool version-space query procedure with any integer budget $b \geq 0$ . At every stage the current version space contains $h^{*}$ and is nonempty; each pool label recorded as a unanimous prediction equals $h^{*}$ at that point; and the procedure terminates after at most $m$ pool iterations. If it makes $q$ queries, then $q \leq \min {m, ∣ H ∣ - 1}$ . Moreover, on any execution for which each oracle-selected branch has size at most $ρ$ times its pre-query version space, for a fixed $0 < ρ < 1$ , one has $q \leq \log ∣ H ∣ / \log (1 / ρ)$ , where $\log$ is the natural logarithm.

Statement references

Finite pool-based realizable active-learning instance: fixes the finite measurable binary class, pool, target, and pointwise exact oracle.

Finite-pool version-space query procedure: scans each pool index once, queries only disagreements while budget permits, and restricts the version space to hypotheses matching each exact answer.

The natural logarithm as the inverse of the exponential function: defines $\log x$ for $x > 0$ as the inverse of the real exponential.

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: proves that $\log$ is strictly increasing, $\log (x y) = \log x + \log y$ , and $\log 1 = 0$ .

Steve Hanneke, Theory of Active Learning, version 1.1, §5.1

Daniel Joseph Hsu, Algorithms for Active Learning, Chapter 2 §2.2.2

Facts & Assumptions

Given: A finite nonempty class $H$ , ordered pool $U = (u_{1}, \dots, u_{m})$ , target $h^{*} \in H$ , exact oracle $O (u_{i}) = h^{*} (u_{i})$ , and query budget $b \geq 0$ .

[F1]

Finite pool-based realizable active-learning instance: the pool is finite and ordered, $h^{*}$ belongs to $H$ , and every queried label is the pointwise target label.

[F2]

Finite-pool version-space query procedure: the procedure starts at $V = H$ , queries only when current classifiers disagree and $q < b$ , increments $q$ once per response, and on a query replaces $V$ by the classifiers matching that oracle answer; unanimous positions are recorded without querying, including when $q = b$ .

[F3]

The natural logarithm as the inverse of the exponential function: for every $x > 0$ , $\log x$ is the unique real $y$ satisfying $\exp (y) = x$ .

[F4]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing, $\log (x y) = \log x + \log y$ for positive $x, y$ , and $\log 1 = 0$ .

[A1]

No choice axiom is assumed or used; the proof uses finite sets, finite filtering, and induction over the pool scan and query count.

Proof

1.1F1F2A1givenconstruct

Initially $V = H$ , so [F1] gives $h^{*} \in V$ . If a query is made at $u_{i}$ , [F1] gives its answer $y = h^{*} (u_{i})$ , and [F2] replaces $V$ by ${h \in V : h (u_{i}) = y}$ , which still contains $h^{*}$ . If no query is made, $V$ is unchanged. Induction over the scan therefore keeps $h^{*}$ in every current $V$ , so $V$ is never empty. The finite filters make no arbitrary selections, as recorded in [A1].

1.2F2givenalgebra

At each loop pass the algorithm either advances from index $i$ to $i + 1$ or returns. Since $U$ has $m$ indices, after at most $m$ such advances it returns, including when $m = 0$ . It queries at most once per visited index, hence $q \leq m$ .

1.3F2giveninduction

Initially $q = 0 \leq b$ . The only update that increases $q$ is made in the branch $q < b$ , so it preserves $q \leq b$ ; when $q = b$ , the algorithm does not query and either records a unanimous label or returns at a disagreement. Induction over the scan gives $q \leq b$ , in particular no queries when $b = 0$ .

2.1F2step 1.1

When [F2] records a unanimous label at $u_{i}$ , every $h \in V$ has that value there. Since $h^{*} \in V$ by step 1.1, the recorded value equals $h^{*} (u_{i})$ .

2.2F1F2step 1.1algebra

At every query, [F2] says the current classifiers disagree at the queried point. One of them is $h^{*}$ by step 1.1, so at least one current classifier has label different from the exact answer and is removed. Version spaces only shrink; consequently each query removes at least one distinct member of $H ∖ {h^{*}}$ . After $q$ queries at least $q$ such members have been removed, while $h^{*}$ remains, giving $q \leq ∣ H ∣ - 1$ .

3.1step 1.2step 2.2algebra

Combining the pool-index bound in step 1.2 with step 2.2 gives $q \leq \min {m, ∣ H ∣ - 1}$ .

4.1F1F3F4step 1.1algebra∎

Under the additional branch-size hypothesis, after $r$ queries induction gives $∣ V_{r} ∣ \leq ρ^{r} ∣ H ∣$ . Step 1.1 gives $∣ V_{q} ∣ \geq 1$ , so $1 \leq ρ^{q} ∣ H ∣$ . Since $ρ^{q} ∣ H ∣ > 0$ , [F4] gives $0 = \log 1 \leq \log (ρ^{q} ∣ H ∣) = q \log ρ + \log ∣ H ∣$ , where the product law is applied repeatedly to the integer power $ρ^{q}$ . Also $1 / ρ > 1$ , so [F4] gives $\log (1 / ρ) > 0$ and, by applying its product law to $ρ (1 / ρ) = 1$ , $\log ρ = - \log (1 / ρ)$ . Rearranging yields $q \leq \log ∣ H ∣ / \log (1 / ρ)$ . For $q = 0$ the same conclusion follows from $∣ H ∣ \geq 1$ .

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Unanimous version-space prediction and disagreement abstention

Statement

Fix a finite pool-based realizable active-learning instance, run the ascending-scan procedure for any finite number of steps, and let $V$ be the resulting current version space. Let $X \sim D_{X}$ be a fresh feature independent of the query history. Define the selective prediction rule $g_{V} (x)$ to be the common label $c \in {0, 1}$ when every $h \in V$ has $h (x) = c$ , and to be the abstention symbol $⊥$ otherwise. Then $DIS (V)$ is measurable, $D_{X} ({x : g_{V} (x) = ⊥}) = D_{X} (DIS (V)),$ and $D_{X} ({x : g_{V} (x) \in {0, 1}, g_{V} (x) \neq h^{*} (x)}) = 0.$ These probabilities are for a fixed query history; the formula gives the abstention probability but no automatic upper bound on it from $∣ V ∣$ .

Statement references

Finite pool-based realizable active-learning instance: defines $D_{X}$ , finite measurable classifiers, and $DIS (V)$ .

Finite-pool version-space query procedure: defines the current version space after each finite pool scan step.

Finite-pool version-space invariant and query bound: proves that every such current version space contains $h^{*}$ .

Steve Hanneke, Theory of Active Learning, version 1.1, §§2.1–2.2 and §5.1

Daniel Joseph Hsu, Algorithms for Active Learning, Chapter 2 §§2.1–2.2.2

Facts & Assumptions

Given: A current version space $V$ from the stated finite-pool procedure and a fresh feature $X \sim D_{X}$ independent of the fixed query history.

[F1]

Finite pool-based realizable active-learning instance: $H$ is finite, its binary classifiers are measurable, and $DIS (V)$ consists of points where two members of $V$ give different labels.

[F2]

Finite-pool version-space query procedure: the query history yields a current version space by finite filtering of $H$ using observed oracle labels.

[F3]

Finite-pool version-space invariant and query bound: under the pointwise exact-oracle assumption, every current version space contains $h^{*}$ .

[A1]

The fresh feature is sampled independently of the fixed query history from the probability measure $D_{X}$ .

[A2]

No choice axiom is assumed; only a finite union over pairs in $V$ is used.

Proof

1.1F1F2A2givenconstruct

For each pair $h, g \in V$ , the disagreement set ${x : h (x) \neq g (x)}$ is the union of $h^{- 1} ({0}) \cap g^{- 1} ({1})$ and $h^{- 1} ({1}) \cap g^{- 1} ({0})$ . These sets are measurable because $h$ and $g$ are measurable. Since $V$ is finite by [F1] and [F2], $DIS (V)$ is a finite union of measurable sets and is measurable; this finite union uses no choice axiom by [A2].

2.1A1F1step 1.1algebra

By the definition of $g_{V}$ , $g_{V} (x) = ⊥$ exactly when the members of $V$ do not all agree at $x$ , which is exactly when $x \in DIS (V)$ . Thus the two events in the first equality are identical, and their $D_{X}$ probabilities agree for the fresh feature in [A1].

3.1F3givenalgebra∎

If $g_{V} (x) \in {0, 1}$ , all classifiers in $V$ give that common label at $x$ . By [F3], $h^{*} \in V$ , so the common label equals $h^{*} (x)$ . Therefore the wrong-prediction event is empty and has probability zero under $D_{X}$ .

RemarkRemark: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Exact labels, slow version-space shrinkage, and abstention limits

Remark

The invariant requires the pointwise exact-oracle assumption; standard distributional zero-risk realizability alone need not prescribe labels at pool points of zero input probability. A noisy response can remove the true target from the version space. The ascending-scan query count has no uniform bound by a constant times $\log ∣ H ∣$ over all finite classes; the conditional branch-shrink hypothesis in the query theorem is essential for its logarithmic bound. For fresh features, abstention probability is $D_{X} (DIS (V))$ , which can equal one even when $∣ V ∣ = 2$ . No VC-dimension, disagreement-coefficient, or distribution-free active label-complexity rate is asserted; $\log$ is the natural logarithm.

Remark references

Finite pool-based realizable active-learning instance: states the pointwise exact-oracle convention and defines the pool model.

Realizable and agnostic PAC learning: defines standard distributional realizability by zero population risk.

Population and empirical risk: defines population risk as the expected loss under the joint law.

Population and empirical risks are measurable: proves that the population risk is a defined measurable integral in the supervised model.

Finite-pool version-space query procedure: gives the fixed ascending scan and exact-label version-space update.

Finite-pool version-space invariant and query bound: proves target retention, the finite query bound, and the conditional logarithmic branch-shrink bound.

Unanimous version-space prediction and disagreement abstention: gives the exact fresh-feature abstention probability and zero answered-point error.

The natural logarithm as the inverse of the exponential function: defines the natural logarithm on positive reals.

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: supplies the monotonicity, product, and reciprocal laws used in the finite growth comparison.

Steve Hanneke, Theory of Active Learning, version 1.1, §§2.1–2.2 and §5.1

Daniel Joseph Hsu, Algorithms for Active Learning, Chapter 2 §§2.1–2.2.3

Facts & Assumptions

Given: The exact-target finite-pool model, the ascending-scan procedure, and the standard supervised-learning risk convention.

[F1]

Supervised prediction problems: the joint law is a probability measure on the product of the measurable feature and label spaces.

[F2]

Population and empirical risk: population risk is the integral of loss under that joint law; for zero-one classification loss it is the probability of a prediction error.

[F3]

Population and empirical risks are measurable: for a measurable supervised predictor, the loss is measurable and population risk is a defined integral.

[F4]

Realizable and agnostic PAC learning: distributional realizability means some $h \in H$ has $R_{P} (h) = 0$ .

[F5]

Finite pool-based realizable active-learning instance: the exact oracle returns $h^{*} (x)$ at every queried point, and $D_{X}$ is the law for fresh features.

[F6]

Finite-pool version-space query procedure: the procedure scans pool indices in order and removes classifiers that disagree with each queried exact label.

[F7]

Finite-pool version-space invariant and query bound: the target remains in every current version space; the shrink-factor query bound applies only under its stated branch-size hypothesis.

[F8]

Unanimous version-space prediction and disagreement abstention: for a fresh independent feature, the rule abstains exactly on $DIS (V)$ and makes no error when it answers.

[F9]

The natural logarithm as the inverse of the exponential function: for $x > 0$ , $\log x$ is the unique real $y$ satisfying $\exp (y) = x$ .

[F10]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing, satisfies $\log (x y) = \log x + \log y$ for positive $x, y$ , and has $\log 1 = 0$ .

[A1]

All witnesses are explicit finite sets and probability laws; no choice axiom or IID sampling assumption is used.

Proof

1.1A1F1F2F3F4F5construct

Let $X = {a, b}$ with its full sigma-algebra and label set ${0, 1}$ with its discrete sigma-algebra. Take the joint law $P = δ_{(a, 0)}$ , use zero-one loss $ℓ (\hat{y}, y) = 1 {\hat{y} \neq y}$ , and set $D_{X} = P_{X} = δ_{a}$ , where $P_{X}$ is the input marginal of $P$ . Define $H = {h_{0}, h_{1}}$ by $h_{0} (a) = h_{0} (b) = 0$ and $h_{1} (a) = 0$ , $h_{1} (b) = 1$ . For pool $U = (b)$ , choose target $h^{*} = h_{1}$ and exact oracle $O = h_{1}$ . The zero-one error events are measurable by [F1] and [F3], and [F2] defines their risks as their $P$ -probabilities. Both risks are zero, so [F4] declares the law realizable by either classifier. Yet $h_{0}$ and $h^{*}$ give different labels at the pool point $b$ , whose $D_{X}$ -probability is zero. Thus distributional realizability does not prescribe the label at every possible pool point; [F5]'s pointwise oracle condition is a genuinely stronger interface.

1.2F6construct

Let $X = {a}$ , $H = {h_{0}, h_{1}}$ with $h_{0} (a) = 0$ and $h_{1} (a) = 1$ , target $h^{*} = h_{0}$ , and budget $b \geq 1$ . If the filtering update is fed the noisy response $1$ at the initial disagreement $a$ , [F6] replaces $V = {h_{0}, h_{1}}$ by ${h_{1}}$ , deleting the true target. Hence the invariant proof cannot be extended to arbitrary noisy responses.

1.3F5F6construct

For any $m \geq 2$ , take $X = {x_{1}, \dots, x_{m}}$ , target $h_{*} (x_{j}) = 1$ , alternatives $h_{i} (x_{j}) = 0$ exactly when $j = i$ , pool $(x_{1}, \dots, x_{m})$ , and budget $b \geq m$ . Before query $i$ , the version space is ${h_{*}, h_{i}, \dots, h_{m}}$ : this is true initially and, at $x_{i}$ , the exact positive label removes only $h_{i}$ . Thus all $m$ indices are queried and $q = m = ∣ H ∣ - 1$ .

2.1F7F9F10step 1.3algebra

Set $m = 2^{k} - 1$ for integers $k \geq 2$ . Then $∣ H ∣ = 2^{k}$ and $q = 2^{k} - 1$ . By repeated application of [F10]'s product law, $\log ∣ H ∣ = k \log 2$ , and strict increase with $2 > 1$ gives $\log 2 > \log 1 = 0$ . The ratio $q / (k \log 2)$ is at least $2^{k - 1} / (k \log 2)$ ; the latter is unbounded because its consecutive-term ratio is $2 k / (k + 1) \geq 4 / 3$ . Therefore no uniform constant multiple of $\log ∣ H ∣$ bounds the query count, while [F7]'s logarithmic guarantee remains valid when its branch-shrink premise holds.

3.1A1F5F8construct∎

Let $X = {a}$ , $H = {h_{0}, h_{1}}$ with $h_{0} (a) = 0$ , $h_{1} (a) = 1$ , target $h^{*} = h_{0}$ , current version space $V = H$ , and $D_{X} ({a}) = 1$ . The initial version space is consistent with the exact-target model. Then $DIS (V) = X$ , so [F8] gives abstention probability $D_{X} (DIS (V)) = 1$ although $∣ V ∣ = 2$ . This verifies that finiteness alone does not force the disagreement mass to be small. All witnesses are explicit finite constructions, as stated in [A1].

4 · Examples, counterexamples and false statements

None yet.

Active querying, version spaces, and abstention

2 · Logical flowchart

3 · Definitions, theorems and proofs

Finite pool-based realizable active-learning instance

Definition

Definition references

Finite-pool version-space query procedure

Definition

Definition references

Finite-pool version-space invariant and query bound

Statement

Statement references

Facts & Assumptions

Proof

Unanimous version-space prediction and disagreement abstention

Statement

Statement references

Facts & Assumptions

Proof

Exact labels, slow version-space shrinkage, and abstention limits

Remark

Remark references

Facts & Assumptions

Proof

4 · Examples, counterexamples and false statements

Sources