Learning a predictor from sampled descriptions

Validation samples a labeled source example and its weight coin. On acceptance it checks the prediction; otherwise it returns a fresh fair bit. The resulting acceptance probability measures weighted prediction bias without rejection sampling. Candidate generation and validation remain ordinary probabilistic programs with separately synthesized strict PPT certificates.

Main definitions

• weightedTrial: validate a weighted example with a fair rejection branch.
• learn: sample both predictor orientations and select by empirical score.

Main results

• learn_goodPredictor_error_pow: the concrete learner meets the boosting correlation contract.
• learn_length_le: every returned description has the charged size, even on failed trials.
• isPPTOn_learn: certify the complete learner through shared program combinators.

References

• Thomas Holenstein, Key Agreement from Weak Bit Agreement, STOC 2005, Section 2.2, the uniform hard-core construction and its learner calls. [Hol05].
• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, the prediction reduction following Game 5. [Hol06]. The weighted validation and explicit candidate selection implement the learner for our fresh-mask version of the reduction.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed tidy-machine certificates.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.weightedTrial {α : Type} (source : ProbComp α) (mask test : α → ProbComp Bool) : ProbComp Bool

Run a trial on a freshly weighted example, with a fair baseline when its weight coin fails.

theorem Cslib.Crypto.Pseudoentropy.Boosting.weightedTrial_probability {α : Type} [Fintype α] (source : ProbComp α) (mask test : α → ProbComp Bool) : ((weightedTrial source mask test).eval true).toReal = 1 / 2 + ∑ value : α, (source.eval value).toReal * (((mask value).eval true).toReal * (((test value).eval true).toReal - 1 / 2))

Acceptance above a fair baseline is exactly the mask-weighted trial bias.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_weightedTrial {α Param : Type} {input : Param ↪ List Bool} {sample : α ↪ List Bool} {source : Param → ProbComp α} {mask test : Param → α → ProbComp Bool} (hsource : Probability.IsPPTOn input sample source) (hmask : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool fun (pair : Param × α) => mask pair.1 pair.2) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input sample) Turing.MultiTapeTM.encBool fun (pair : Param × α) => test pair.1 pair.2) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Param) => weightedTrial (source a) (mask a) (test a)

Weighted validation is strict PPT, including examples on which the weight coin fails.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_weightedTrial_bind {α Code : Type} (candidates : ProbComp Code) (source : ProbComp α) (mask : α → ProbComp Bool) (test : Code → α → ProbComp Bool) : (do let code ← candidates weightedTrial source mask (test code)).eval = (weightedTrial source mask fun (value : α) => do let code ← candidates test code value).eval

Saved predictor randomness can be sampled before or after the validation example and weight coin. Thus validation measures the original randomized predictor's weighted bias.

theorem Cslib.Crypto.Pseudoentropy.Boosting.weightedTrial_not {α : Type} (source : ProbComp α) (mask test : α → ProbComp Bool) : ((weightedTrial source mask fun (value : α) => not <$> test value).eval true).toReal = 1 - ((weightedTrial source mask test).eval true).toReal

Complementing the trial negates its weighted bias. The rejected branch remains fair.

theorem Cslib.Crypto.Pseudoentropy.Boosting.weightedTrial_correlation {α : Type} [Fintype α] (source : ProbComp α) (mask : α → ProbComp Bool) (predict truth : α → Bool) : ((weightedTrial source mask fun (value : α) => pure (predict value == truth value)).eval true).toReal = 1 / 2 + (∑ value : α, (source.eval value).toReal * (((mask value).eval true).toReal * BitString.signedVote (predict value) (truth value))) / 2

A deterministic predictor's validation rate is one half plus half its weighted correlation.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.randomSign (candidates : ProbComp (List Bool)) : ProbComp (List Bool)

Add a fresh fair orientation bit to a sampled predictor description.

def Cslib.Crypto.Pseudoentropy.Boosting.signedTest (test : List Bool → ProbComp Bool) (code : List Bool) : ProbComp Bool

A leading sign bit complements a trial's answer; the remaining word is its original code.

def Cslib.Crypto.Pseudoentropy.Boosting.signedPredict {α : Type} (predict : List Bool → α → Bool) (code : List Bool) (value : α) : Bool

Interpret the same leading sign bit when evaluating the final deterministic predictor.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.signedTest_false (test : List Bool → ProbComp Bool) (code : List Bool) : signedTest test (false :: code) = test code

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.signedTest_true (test : List Bool → ProbComp Bool) (code : List Bool) : signedTest test (true :: code) = not <$> test code

theorem Cslib.Crypto.Pseudoentropy.Boosting.randomSign_good_probability (candidates : ProbComp (List Bool)) (test : List Bool → ProbComp Bool) {ε : ℝ} (hε : 0 ≤ ε) : (|((candidates >>= test).eval true).toReal - 1 / 2| - ε) / 2 ≤ ((randomSign candidates).eval.toOuterMeasure {code : List Bool | 1 / 2 + ε ≤ ((signedTest test code).eval true).toReal}).toReal

Either sign of an average validation bias supplies a noticeable chance of drawing a positively biased signed candidate. The sign choice is made by the program's fair coin.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.learn (candidates : ProbComp (List Bool)) (test : List Bool → ProbComp Bool) (confidence inverseGap : ℕ) : ProbComp (List Bool)

A bounded learner samples both orientations and selects by repeated validation trials.

theorem Cslib.Crypto.Pseudoentropy.Boosting.learn_error_pow (candidates : ProbComp (List Bool)) (test : List Bool → ProbComp Bool) (confidence inverseGap : ℕ) (hgap : 0 < inverseGap) (hbias : 1 / ↑inverseGap ≤ |((candidates >>= test).eval true).toReal - 1 / 2|) : ((learn candidates test confidence inverseGap).eval.toOuterMeasure {code : List Bool | ¬1 / 2 + 1 / (4 * ↑inverseGap) ≤ ((signedTest test code).eval true).toReal}).toReal ≤ (↑((confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ confidence

An inverse-polynomial average validation bias, of either sign, yields a positively biased predictor except with an explicit exponentially small discovery-and-selection error.

theorem Cslib.Crypto.Pseudoentropy.Boosting.signedTest_weightedTrial {α : Type} (source : ProbComp α) (mask : α → ProbComp Bool) (predict : List Bool → α → Bool) (truth : α → Bool) (code : List Bool) : ((signedTest (fun (code : List Bool) => weightedTrial source mask fun (value : α) => pure (predict code value == truth value)) code).eval true).toReal = ((weightedTrial source mask fun (value : α) => pure (signedPredict predict code value == truth value)).eval true).toReal

The selected orientation is used by the final predictor, and its validation rate is the same rate estimated during learning.

theorem Cslib.Crypto.Pseudoentropy.Boosting.learn_correlation_error_pow {α : Type} [Fintype α] (candidates : ProbComp (List Bool)) (source : ProbComp α) (mask : α → ProbComp Bool) (predict : List Bool → α → Bool) (truth : α → Bool) (confidence inverseGap : ℕ) (hgap : 0 < inverseGap) (hbias : 1 / ↑inverseGap ≤ |((do let code ← candidates weightedTrial source mask fun (value : α) => pure (predict code value == truth value)).eval true).toReal - 1 / 2|) : ((learn candidates (fun (code : List Bool) => weightedTrial source mask fun (value : α) => pure (predict code value == truth value)) confidence inverseGap).eval.toOuterMeasure {code : List Bool | ¬1 / (2 * ↑inverseGap) ≤ ∑ value : α, (source.eval value).toReal * (((mask value).eval true).toReal * BitString.signedVote (signedPredict predict code value) (truth value))}).toReal ≤ (↑((confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ confidence

The learned deterministic predictor has positive weighted correlation. The advantage hypothesis concerns the original candidate distribution, before choosing an orientation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.learn_length_le (candidates : ProbComp (List Bool)) (test : List Bool → ProbComp Bool) (confidence inverseGap bound : ℕ) (hbound : ∀ code ∈ candidates.eval.support, code.length ≤ bound) {code : List Bool} (hcode : code ∈ (learn candidates test confidence inverseGap).eval.support) : code.length ≤ bound + 1

Each orientation adds exactly one bit, and empirical selection preserves this bound even when its statistical tests fail. The empty fallback also satisfies it.

theorem Cslib.Crypto.Pseudoentropy.Boosting.learn_goodPredictor_error_pow {α : Type} [Fintype α] (candidates : ProbComp (List Bool)) (source : ProbComp α) (mask : α → ProbComp Bool) (predict : List Bool → α → Bool) (truth : α → Bool) (state : State) (params : Parameters) (hparams : params.Valid) (inverseGap bound : ℕ) (hgap : 0 < inverseGap) (hgamma : params.gamma ≤ 1 / (2 * ↑inverseGap)) (hbound : ∀ code ∈ candidates.eval.support, code.length ≤ bound) (hcodeBound : bound + 1 ≤ params.codeBound) (hmask : ∀ (value : α), ((mask value).eval true).toReal = weight params.rate (state.margin (signedPredict predict) truth value - ↑state.threshold)) (hbias : 1 / ↑inverseGap ≤ |((do let code ← candidates weightedTrial source mask fun (value : α) => pure (predict code value == truth value)).eval true).toReal - 1 / 2|) : ((learn candidates (fun (code : List Bool) => weightedTrial source mask fun (value : α) => pure (predict code value == truth value)) params.confidence inverseGap).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (signedPredict predict) truth params state code}).toReal ≤ (↑((params.confidence + 1) * (4 * inverseGap) ^ 2) + 1) * (1 / 2) ^ params.confidence

The concrete learner meets the boosting loop's contract for the truncated description. Its validation mask is the current soft weight, and its target correlation covers gamma. The remaining cryptographic premise is the candidate distribution's noticeable validation bias.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_randomSign {Param : Type} {input : Param ↪ List Bool} {source : Param → ProbComp (List Bool)} (hsource : Probability.IsPPTOn input Turing.MultiTapeTM.encBits source) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : Param) => randomSign (source a)

Adding a random orientation preserves the sampler's strict PPT certificate.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_signedTest {Param : Type} {input : Param ↪ List Bool} {test : Param → List Bool → ProbComp Bool} {code : Param → List Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (pair : Param × List Bool) => test pair.1 pair.2) (hcode : Turing.MultiTapeTM.ComputableTidilyInPolyTime code input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Param) => signedTest (test a) (code a)

Validation of signed descriptions is strict PPT for any supplied efficient trial.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPolyTime_signedPredict {α : Type} {input : α ↪ List Bool} {predict : List Bool → α → Bool} (hpredict : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × α) => predict pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits input) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × α) => signedPredict predict pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits input) Turing.MultiTapeTM.encBool

Reading the orientation and running the saved evaluator remains deterministic polynomial time on every description, including malformed or truncated ones.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_learn {Param : Type} {input : Param ↪ List Bool} {candidates : Param → ProbComp (List Bool)} {test : Param → List Bool → ProbComp Bool} {confidence inverseGap : Param → ℕ} (hcandidates : Probability.IsPPTOn input Turing.MultiTapeTM.encBits candidates) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (pair : Param × List Bool) => test pair.1 pair.2) (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (hgap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : Param) => learn (candidates a) (test a) (confidence a) (inverseGap a)

The complete learner is strict PPT in its input, confidence, and inverse bias parameters.