Selecting a candidate by repeated trials

OracleComp.selectBest count trials test estimates the acceptance probability of each candidate below count and returns the candidate with the largest success count. It is an ordinary bounded program. The correctness rule charges one estimation failure per candidate and loses twice the estimation tolerance relative to the best candidate. No independence between estimates is needed by the selection argument; each estimate uses the independent trials in countTrue.

Main definitions

• Cslib.OracleComp.selectUpdate: update the next index and the running best index and count.
• Cslib.OracleComp.selectStep: estimate one candidate and update the running empirical maximum.
• Cslib.OracleComp.selectBest: select an index by empirical success count.
• Cslib.OracleComp.selectFrom, .sampleBest: select from a list or a sampled candidate pool.

Main results

• Cslib.ProbComp.selectBest_error_pow, .selectFrom_error_pow: statistical selection bounds.
• Cslib.ProbComp.sampleBest_error_pow: combine discovery and validation failures.
• Cslib.ProbComp.selectStep_bounded, .sampleBest_support: bounds on every execution.

References

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The deviation estimate is the Hoeffding bound from [Hoe63].

def Cslib.OracleComp.selectUpdate (state : ℕ × ℕ × ℕ) (successes : ℕ) : ℕ × ℕ × ℕ

Update the next index, best index, and best success count, preferring later indices on ties.

def Cslib.OracleComp.selectStep {Query : Type u} {spec : OracleSpec Query} (trials : ℕ) (test : ℕ → OracleComp spec Bool) (state : ℕ × ℕ × ℕ) : OracleComp spec (ℕ × ℕ × ℕ)

Estimate one candidate and update the running empirical maximum.

def Cslib.OracleComp.selectBest {Query : Type u} {spec : OracleSpec Query} (count trials : ℕ) (test : ℕ → OracleComp spec Bool) : OracleComp spec ℕ

Return an index with the largest observed success count. When there are no candidates, return zero.

def Cslib.OracleComp.selectFrom {Query : Type u} {spec : OracleSpec Query} {α : Type} (values : List α) (trials : ℕ) (test : α → OracleComp spec Bool) (fallback : α) : OracleComp spec α

Select an empirically best value from a list, returning the fallback for an empty list.

def Cslib.OracleComp.sampleBest {Query : Type u} {spec : OracleSpec Query} {α : Type} (count trials : ℕ) (source : OracleComp spec α) (test : α → OracleComp spec Bool) (fallback : α) : OracleComp spec α

Draw a candidate pool and select the candidate with the highest empirical score.

theorem Cslib.ProbComp.selectFrom_support {α : Type} (values : List α) (trials : ℕ) (test : α → ProbComp Bool) (fallback : α) {chosen : α} (hchosen : chosen ∈ (eval (OracleComp.selectFrom values trials test fallback)).support) : chosen = fallback ∨ chosen ∈ values

Selection can only return a listed candidate or the supplied fallback. This holds on every execution, independently of estimation accuracy.

theorem Cslib.ProbComp.sampleBest_support {α : Type} (count trials : ℕ) (source : ProbComp α) (test : α → ProbComp Bool) (fallback : α) {chosen : α} (hchosen : chosen ∈ (eval (OracleComp.sampleBest count trials source test fallback)).support) : chosen = fallback ∨ chosen ∈ source.eval.support

Empirical selection preserves the support of its candidate sampler, apart from the fixed fallback. In particular, bounds on descriptions survive every statistical failure.

theorem Cslib.ProbComp.selectStep_bounded (trials : ℕ) (test : ℕ → ProbComp Bool) (i : ℕ) (state : ℕ × ℕ × ℕ) (hstate : state.1 = i ∧ state.2.1 ≤ i ∧ state.2.2 ≤ trials) (next : ℕ × ℕ × ℕ) (hnext : next ∈ (eval (OracleComp.selectStep trials test state)).support) : next.1 = i + 1 ∧ next.2.1 ≤ i + 1 ∧ next.2.2 ≤ trials

Candidate selection keeps both indices within the elapsed count and the success count within the trial budget on every execution, regardless of statistical estimation errors.

theorem Cslib.ProbComp.selectBest_error_le (count trials : ℕ) (hcount : 0 < count) (test : ℕ → ProbComp Bool) {ε error : ℝ} (herror : 0 ≤ error) (hestimate : ∀ i < count, ((eval (OracleComp.countTrue trials (test i))).toOuterMeasure {successes : ℕ | ε ≤ |↑successes / ↑trials - ((test i).eval true).toReal|}).toReal ≤ error) : ((eval (OracleComp.selectBest count trials test)).toOuterMeasure {chosen : ℕ | ¬(chosen < count ∧ ∀ i < count, ((test i).eval true).toReal ≤ ((test chosen).eval true).toReal + 2 * ε)}).toReal ≤ ↑count * error

If every empirical probability is accurate except with probability error, selection loses at most twice the tolerance relative to every candidate, except with probability count * error. The returned index is in range on this same event.

theorem Cslib.ProbComp.selectBest_error_pow (count confidence inverseTolerance : ℕ) (hcount : 0 < count) (htolerance : 0 < inverseTolerance) (test : ℕ → ProbComp Bool) : ((eval (OracleComp.selectBest count ((confidence + 1) * inverseTolerance ^ 2) test)).toOuterMeasure {chosen : ℕ | ¬(chosen < count ∧ ∀ i < count, ((test i).eval true).toReal ≤ ((test chosen).eval true).toReal + 2 / ↑inverseTolerance)}).toReal ≤ ↑count * (1 / 2) ^ confidence

A polynomial trial budget selects within twice the requested inverse tolerance of the best candidate, with one exponentially small failure term per candidate.

theorem Cslib.ProbComp.selectBest_test_error_le (count confidence inverseTolerance : ℕ) (htolerance : 0 < inverseTolerance) (test : ℕ → ProbComp Bool) (i : ℕ) (hi : i < count) : ((do let chosen ← OracleComp.selectBest count ((confidence + 1) * inverseTolerance ^ 2) test test chosen).eval false).toReal ≤ ((test i).eval false).toReal + 2 / ↑inverseTolerance + ↑count * (1 / 2) ^ confidence

A fresh test of the selected candidate fails at most as often as any specified candidate, up to twice the estimation tolerance and the probability of a selection error.

theorem Cslib.ProbComp.selectFrom_error_pow {α : Type} (values : List α) (hvalues : 0 < values.length) (confidence inverseTolerance : ℕ) (htolerance : 0 < inverseTolerance) (test : α → ProbComp Bool) (fallback : α) : ((eval (OracleComp.selectFrom values ((confidence + 1) * inverseTolerance ^ 2) test fallback)).toOuterMeasure {chosen : α | ¬(chosen ∈ values ∧ ∀ value ∈ values, ((test value).eval true).toReal ≤ ((test chosen).eval true).toReal + 2 / ↑inverseTolerance)}).toReal ≤ ↑values.length * (1 / 2) ^ confidence

Empirical selection from a nonempty list loses at most twice the estimation tolerance relative to every listed candidate, except for one small failure term per candidate.

theorem Cslib.ProbComp.sampleBest_error_pow {α : Type} (source : ProbComp α) (test : α → ProbComp Bool) (fallback : α) (confidence inverseSuccess inverseTolerance : ℕ) (hsuccess : 0 < inverseSuccess) (htolerance : 0 < inverseTolerance) (threshold : ℝ) (hgood : 1 / ↑inverseSuccess ≤ (source.eval.toOuterMeasure {value : α | threshold ≤ ((test value).eval true).toReal}).toReal) : ((eval (OracleComp.sampleBest ((confidence + 1) * inverseSuccess ^ 2) ((confidence + 1) * inverseTolerance ^ 2) source test fallback)).toOuterMeasure {chosen : α | ¬threshold - 2 / ↑inverseTolerance ≤ ((test chosen).eval true).toReal}).toReal ≤ (↑((confidence + 1) * inverseSuccess ^ 2) + 1) * (1 / 2) ^ confidence

A noticeable chance of drawing a good candidate can be amplified by sampling a pool and estimating every candidate. The two failure terms pay separately for discovery and selection.