Training and evaluating a boosted predictor

train runs the clocked loop and selects the final slope. Its result is the stored state paired with a natural numerator. predict uses only this description and the public observation; training labels are never supplied at prediction time.

The correctness bound adds the loop's guard and learner failures to the final selection failure. The learner's correlation contract remains an explicit hypothesis. The efficiency certificates compose the programming rules, independently of these probabilistic guarantees.

Main definitions

• finish, train: select a final model after the clocked boosting loop.
• predict, predictionError: evaluate that model on public observations and measure its error.

Main results

• isPPTOn_train, isPPTOn_predict: compositional training and prediction certificates.
• train_sound, train_predict_error: combine guard, learner and slope-selection failures.

References

[Hol05], Section 2.2, Lemma 2.4 and Claims 2.15–2.16. As in Selection, the final predictor uses empirical selection over a finite slope grid. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.finish (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (params : Parameters) (state : State) : ProbComp (State × ℕ)

Keep a stopped majority predictor, or select a slope from fresh labeled samples.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.train (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (learn : State → ProbComp (List Bool)) (params : Parameters) : ProbComp (State × ℕ)

Train one predictor description using the clocked loop and uniform final selection.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.predict (evaluate : List Bool → List Bool → Bool) (precision : ℕ) (model : State × ℕ) (observation : List Bool) : ProbComp Bool

Evaluate a learned description on public information alone. The numerator is unused when the majority stopping test succeeded.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_finish {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {source : α → ProbComp (List Bool × Bool)} {params : α → Parameters} {state : α → State} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input State.encoding) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Parameters.encoding) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair State.encoding Turing.MultiTapeTM.encUnary) fun (a : α) => finish evaluate (source a) (params a) (state a)

Final selection composes the evaluator, source, stored state, and encoded parameters.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_train {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {source : α → ProbComp (List Bool × Bool)} {learn : α → State → ProbComp (List Bool)} {params : α → Parameters} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hlearn : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input State.encoding) Turing.MultiTapeTM.encBits fun (pair : α × State) => learn pair.1 pair.2) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Parameters.encoding) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair State.encoding Turing.MultiTapeTM.encUnary) fun (a : α) => train evaluate (source a) (learn a) (params a)

Training is strict PPT on every execution, including guard and learner failures.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_predict {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {precision : α → ℕ} {model : α → State × ℕ} {observation : α → List Bool} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hprecision : Turing.MultiTapeTM.ComputableTidilyInPolyTime precision input Turing.MultiTapeTM.encUnary) (hmodel : Turing.MultiTapeTM.ComputableTidilyInPolyTime model input (Turing.MultiTapeTM.encPair State.encoding Turing.MultiTapeTM.encUnary)) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observation input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => predict evaluate (precision a) (model a) (observation a)

Applying a trained predictor requires only efficient observations and the stored description.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.predictionError {α : Type u_1} (source : PMF α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (precision : ℕ) (model : State × ℕ) : ℝ

Prediction error on a source. This semantic definition also permits infinite source types.

theorem Cslib.Crypto.Pseudoentropy.Boosting.predictionError_stopped {α : Type u_1} (source : PMF α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (precision : ℕ) (model : State × ℕ) (hstopped : model.1.stopped = true) : predictionError source observe truth evaluate precision model = (source.toOuterMeasure {x : α | BitString.listStrictMajority (State.votes evaluate model.1 (observe x)) ≠ truth x}).toReal

A stopped model has exactly its deterministic majority error.

theorem Cslib.Crypto.Pseudoentropy.Boosting.predictionError_active {α : Type} [Fintype α] (source : PMF α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (precision : ℕ) (model : State × ℕ) (hactive : model.1.stopped = false) : predictionError source observe truth evaluate precision model = clippedError source (model.1.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth) (↑model.2 / ↑(Probability.dyadicSize precision))

An active model has exactly the clipped error used by the slope-selection theorem.

theorem Cslib.Crypto.Pseudoentropy.Boosting.finish_sound {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (params : Parameters) (hparams : params.Valid) {state : State} (hstate : State.Successful source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state) (hbounded : State.Bounded params.clock params.codeBound state) : ((finish evaluate ((fun (x : α) => (observe x, truth x)) <$> source) params state).eval.toOuterMeasure {model : State × ℕ | ¬predictionError source.eval observe truth evaluate params.predictionGridBound model ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance}).toReal ≤ (↑(Probability.dyadicSize params.predictionGridBound) + 1) * (1 / 2) ^ params.confidence

Either stopping branch gives the same prediction advantage, except for final slope selection.

theorem Cslib.Crypto.Pseudoentropy.Boosting.train_sound {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (learn : State → ProbComp (List Bool)) (params : Parameters) (hparams : params.Valid) {error : ℝ} (herror : 0 ≤ error) (hlearn : ∀ (state : State), (params.delta ≤ density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth x - ↑state.threshold) → ((learn state).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state code}).toReal ≤ error) : ((train evaluate ((fun (x : α) => (observe x, truth x)) <$> source) learn params).eval.toOuterMeasure {model : State × ℕ | ¬predictionError source.eval observe truth evaluate params.predictionGridBound model ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance}).toReal ≤ ↑params.clock * (2 * (1 / 2) ^ params.confidence + error) + (↑(Probability.dyadicSize params.predictionGridBound) + 1) * (1 / 2) ^ params.confidence

The complete training algorithm has one failure bound for guards, learners, and selection. All obligations refer to the supplied source and the descriptions actually stored by the loop.

theorem Cslib.Crypto.Pseudoentropy.Boosting.train_predict_error {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (learn : State → ProbComp (List Bool)) (params : Parameters) (hparams : params.Valid) {error : ℝ} (herror : 0 ≤ error) (hlearn : ∀ (state : State), (params.delta ≤ density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth x - ↑state.threshold) → ((learn state).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state code}).toReal ≤ error) : ((do let x ← source let model ← train evaluate ((fun (x : α) => (observe x, truth x)) <$> source) learn params (fun (answer : Bool) => answer == truth x) <$> predict evaluate params.predictionGridBound model (observe x)).eval false).toReal ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance + ↑params.clock * (2 * (1 / 2) ^ params.confidence + error) + (↑(Probability.dyadicSize params.predictionGridBound) + 1) * (1 / 2) ^ params.confidence

Averaging over training gives an overall prediction-error bound. Training is independent of the challenge, and only its public observation reaches the trained predictor.