From cb0a7dc17193f1de9ec4c553b6e74cc7e873ef29 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 00:56:00 +0000 Subject: [PATCH] refactor(Promise): share probability_sampleList_verifier and replace restatement tests (#884) Co-authored-by: Gemini <218195315+gemini-code-assist@users.noreply.github.com> --- .../Classes/Promise/Probabilistic.lean | 21 ++- .../Classes/Promise/Randomized.lean | 7 - ComplexityTests/PromiseProbabilistic.lean | 133 ++++++++---------- 3 files changed, 75 insertions(+), 86 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean index 12ec5aaa14..67adc0add1 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean @@ -10,7 +10,9 @@ module public import Complexity.Computability.Complexity.Classes.BPP public import Complexity.Computability.Complexity.Classes.Promise.Reduction public import Complexity.Computability.Complexity.Classes.RP +public import Complexity.Computability.Complexity.Classes.SharpP public import Complexity.Computability.Probabilistic.PPT +public import Complexity.Languages.Probabilistic.BitString public import Complexity.Languages.Probabilistic.Notation import Complexity.Computability.Complexity.Classes.RP.Closure import Complexity.Computability.Complexity.Classes.SharpP.Probability @@ -51,6 +53,8 @@ reductions (`PromiseProblem.PolyTimeReducible.mem_PromiseBPP`, complement relations between `PromiseRP` and `PromiseCoRP`. * `Cslib.Complexity.PromiseP_subset_PromiseRP`, `Cslib.Complexity.PromiseP_subset_PromiseCoRP`, `Cslib.Complexity.PromiseP_subset_PromiseBPP`. +* `Cslib.Complexity.probability_sampleList_verifier`: acceptance probability of sampling a uniform + random word for a seeded verifier. * `Cslib.Complexity.mem_PromiseBPP_iff_exists_isPPTOn`, `Cslib.Complexity.mem_PromiseRP_iff_exists_isPPTOn`, `Cslib.Complexity.mem_PromiseCoRP_iff_exists_isPPTOn`: characterizations by uniform strict PPT @@ -132,6 +136,13 @@ theorem PromiseP_subset_PromiseCoRP : PromiseP enc ⊆ PromiseCoRP enc := theorem PromiseP_subset_PromiseBPP : PromiseP enc ⊆ PromiseBPP enc := (promiseClass_mono P_subset_BPP).trans promiseClass_BPP_subset_PromiseBPP +/-- The program sampling a random string for a seeded verifier accepts with the accepted +fraction of the strings. -/ +theorem probability_sampleList_verifier (V : α × List Bool → Bool) (a : α) (n : ℕ) : + Pr[(fun w => V (a, w)) <$> BitString.sampleList n] = (acceptCount V a n : ℝ) / 2 ^ n := by + simp only [ProbComp.eval_map, BitString.eval_sampleList] + exact uniformList_acceptCount_toReal V a n + /-- **Probabilistic-program characterization of `PromiseBPP`**: a promise problem is in `PromiseBPP` exactly when a uniform strict PPT Boolean program accepts every yes-instance with probability at least `2 / 3` and rejects every no-instance with probability at least `2 / 3`. -/ @@ -146,14 +157,13 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ IsPPTOn.of_seeded ((ComputableInPolyTime.unary_eval p).comp (ComputableInPolyTime.encoding_length enc)) hV, fun a ha => ?_, fun a ha => ?_⟩ - · simp only [ProbComp.eval_map, BitString.eval_sampleList] - rw [uniformList_acceptCount_toReal, le_div_iff₀ (by positivity)] + · rw [probability_sampleList_verifier, le_div_iff₀ (by positivity)] have h : (2 : ℝ) * 2 ^ p.eval (enc a).length ≤ 3 * (acceptCount V a (p.eval (enc a).length) : ℝ) := by exact_mod_cast (hQ a).1 ha linarith - · simp only [Functor.map_map, ProbComp.eval_map, BitString.eval_sampleList] - rw [uniformList_acceptCount_toReal (V := fun x => !V x), le_div_iff₀ (by positivity)] + · rw [Functor.map_map, probability_sampleList_verifier (V := fun x => !V x), + le_div_iff₀ (by positivity)] have h : (2 : ℝ) * 2 ^ p.eval (enc a).length ≤ 3 * (acceptCount (fun x => !V x) a (p.eval (enc a).length) : ℝ) := by simpa only [acceptCount, Bool.not_eq_true'] using @@ -204,8 +214,7 @@ theorem mem_PromiseRP_iff_exists_isPPTOn : Q ∈ PromiseRP enc ↔ IsPPTOn.of_seeded ((ComputableInPolyTime.unary_eval p).comp (ComputableInPolyTime.encoding_length enc)) hV, fun a ha => ?_, fun a ha hmem => ?_⟩ - · simp only [ProbComp.eval_map, BitString.eval_sampleList] - rw [uniformList_acceptCount_toReal, le_div_iff₀ (by positivity)] + · rw [probability_sampleList_verifier, le_div_iff₀ (by positivity)] have h : (2 : ℝ) ^ p.eval (enc a).length ≤ 2 * (acceptCount V a (p.eval (enc a).length) : ℝ) := by exact_mod_cast (hQ a).1 ha diff --git a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean index 1ab4fb5b41..e57e860172 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean @@ -430,13 +430,6 @@ private theorem probability_and2 (M : α → ProbComp Bool) (a : α) : simp [ProbComp.eval_map, PMF.map_apply] rw [htrue, hfalse, mul_zero, add_zero] -/-- The program sampling a random string for a seeded verifier accepts with the accepted -fraction of the strings. -/ -private theorem probability_sampleList_verifier (V : β × List Bool → Bool) (b : β) (n : ℕ) : - Pr[(fun w => V (b, w)) <$> BitString.sampleList n] = (acceptCount V b n : ℝ) / 2 ^ n := by - simp only [ProbComp.eval_map, BitString.eval_sampleList] - exact uniformList_acceptCount_toReal V b n - /-- **`PromiseCoRP` is closed under `RPReducible`** (library lemma): if `X` reduces to `Y` by a randomized one-sided reduction and `Y ∈ PromiseCoRP encB`, then `X ∈ PromiseCoRP encA`. -/ theorem RPReducible.mem_PromiseCoRP (hXY : RPReducible encA encB X Y) diff --git a/ComplexityTests/PromiseProbabilistic.lean b/ComplexityTests/PromiseProbabilistic.lean index ebeafa3a37..e69aecdfcc 100644 --- a/ComplexityTests/PromiseProbabilistic.lean +++ b/ComplexityTests/PromiseProbabilistic.lean @@ -4,87 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ +import Complexity.Computability.Complexity.Classes.BPP.Amplification import Complexity.Computability.Complexity.Classes.Promise.Randomized import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List -/-! Tests for probabilistic promise classes (`PromiseBPP`, `PromiseRP`, `PromiseCoRP`) and -randomized one-sided promise reductions (`RPReducible`, `RPReducibleWithError`), including -nonvacuous coin-flip solvers, soundness strictly between `2 / 3` and `1`, and the `s ≤ 0` edge -case. -/ +/-! Tests for probabilistic promise classes (`PromiseBPP`, `PromiseRP`, `PromiseCoRP`), +`probability_sampleList_verifier`, error amplification (`SolvesWithBoundedError.repeatMajority`) on +a genuinely partial promise problem, and randomized one-sided promise reductions (`RPReducible`, +`RPReducibleWithError`). -/ namespace ComplexityTests.PromiseProbabilistic open Cslib Cslib.Complexity Cslib.Probability Turing.MultiTapeTM -variable {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} - -/-! ### Randomized reductions on promise problems -/ - -example {X : PromiseProblem α} {Y : PromiseProblem β} : - PromiseProblem.RPReducible encA encB X Y ↔ - ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧ - (∀ a ∈ X.yes, ∀ b ∈ (Cslib.ProbComp.eval (R a)).support, b ∈ Y.yes) ∧ - ∀ a ∈ X.no, 2 / 3 ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.no).toReal := - Iff.rfl - -example {X : PromiseProblem α} {Y : PromiseProblem β} : - PromiseProblem.RPReducible encA encB X Y ↔ - ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧ - (∀ a ∈ X.yes, ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.yes).toReal = 1) ∧ - ∀ a ∈ X.no, 2 / 3 ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.no).toReal := - PromiseProblem.rpReducible_iff_toOuterMeasure_eq_one - -example {X : PromiseProblem α} {Y : PromiseProblem β} {s : α → ℝ} : - PromiseProblem.RPReducibleWithError encA encB s Xᶜ Yᶜ ↔ - ∃ R : α → Cslib.ProbComp β, Cslib.Probability.IsPPTOn encA encB R ∧ - (∀ a ∈ X.no, ∀ b ∈ (Cslib.ProbComp.eval (R a)).support, b ∈ Y.no) ∧ - ∀ a ∈ X.yes, s a ≤ ((Cslib.ProbComp.eval (R a)).toOuterMeasure Y.yes).toReal := - PromiseProblem.rpReducibleWithError_compl_iff - -example {X : PromiseProblem α} {Y : PromiseProblem β} - (h : PromiseProblem.PolyTimeReducible encA encB X Y) : - PromiseProblem.RPReducible encA encB X Y := - h.rpReducible - -example {X : PromiseProblem α} : PromiseProblem.RPReducible encA encA X X := - PromiseProblem.RPReducible.refl encA X - -example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} - {s₁ : α → ℝ} {s₂ : ℝ} (hs₂ : 0 ≤ s₂) - (hXY : PromiseProblem.RPReducibleWithError encA encB s₁ X Y) - (hYZ : PromiseProblem.RPReducibleWithError encB encC (fun _ => s₂) Y Z) : - PromiseProblem.RPReducibleWithError encA encC (fun a => s₁ a * s₂) X Z := - hXY.trans hYZ hs₂ - -example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} - {s₁ : α → ℝ} {s₂ : ℝ} (hs₂ : s₂ ≤ 1) - (hXY : PromiseProblem.RPReducibleWithError encA encB s₁ X Y) - (hYZ : PromiseProblem.RPReducibleWithError encB encC (fun _ => s₂) Y Z) : - PromiseProblem.RPReducibleWithError encA encC (fun a => s₁ a + s₂ - 1) X Z := - hXY.trans_add hYZ hs₂ - -example {X : PromiseProblem α} {Y : PromiseProblem β} {Z : PromiseProblem γ} - {s : β → ℝ} {f : α → β} (hf : ComputableInPolyTime f encA encB) - (hyes : Set.MapsTo f X.yes Y.yes) (hno : Set.MapsTo f X.no Y.no) - (hYZ : PromiseProblem.RPReducibleWithError encB encC s Y Z) : - PromiseProblem.RPReducibleWithError encA encC (fun a => s (f a)) X Z := - hYZ.of_computableInPolyTime hf hyes hno - -example {X : PromiseProblem α} {Y : PromiseProblem β} - (hXY : PromiseProblem.RPReducible encA encB X Y) - (hY : Y ∈ PromiseCoRP encB) : X ∈ PromiseCoRP encA := - hXY.mem_PromiseCoRP hY - -example {X : PromiseProblem α} {Y : PromiseProblem β} - (hXY : PromiseProblem.RPReducible encA encB X Y) - (hY : Y ∈ PromiseBPP encB) : X ∈ PromiseBPP encA := - hXY.mem_PromiseBPP hY - -example {X : PromiseProblem α} {Y : PromiseProblem β} - (hXY : PromiseProblem.RPReducible encA encB Xᶜ Yᶜ) - (hY : Y ∈ PromiseRP encB) : X ∈ PromiseRP encA := - hXY.mem_PromiseRP_of_compl hY - /-! ### Nonvacuous concrete instances -/ /-- A concrete `PromiseRP` solver using a real 1-bit coin flip: on `true`, @@ -139,4 +71,59 @@ example : PromiseProblem.RPReducibleWithError encBool encBool (fun _ => 0) simp only [ProbComp.eval_pure, PMF.support_pure, Set.mem_singleton_iff] at hb exact hb +/-! ### Error amplification on a genuinely partial promise problem -/ + +/-- A genuinely partial promise problem on bit strings (`yes = {[true]}`, `no = {[false]}`), +leaving `[]` outside the promise. -/ +def partialSingletonBit : PromiseProblem (List Bool) where + yes := {[true]} + no := {[false]} + disjoint := by simp + +/-- The promise of `partialSingletonBit` is a proper subset of `Set.univ` (`[]` is outside the +promise). -/ +example : partialSingletonBit.yes ∪ partialSingletonBit.no ≠ Set.univ := by + intro h + have hmem : ([] : List Bool) ∈ partialSingletonBit.yes ∪ partialSingletonBit.no := + h ▸ Set.mem_univ [] + simp [partialSingletonBit] at hmem + +/-- A 1-bit verifier that returns the first input bit when present and falls back to the first +random bit on `[]`. -/ +def partialVerifier (p : List Bool × List Bool) : Bool := + p.1.headD (p.2.headD false) + +/-- On the out-of-promise input `[]`, `partialVerifier` accepts with probability `1 / 2`, violating +the `2 / 3` bounded-error margin on both sides. -/ +example : + Pr[(fun w => partialVerifier ([], w)) <$> BitString.sampleList 1] = 1 / 2 := by + rw [probability_sampleList_verifier] + have hcard : acceptCount partialVerifier [] 1 = 1 := by decide + rw [hcard] + norm_num + +/-- Despite accepting the out-of-promise instance `[]` with probability `1 / 2`, `partialVerifier` +solves `partialSingletonBit` with bounded error. -/ +theorem solvesWithBoundedError_partialSingletonBit : + partialSingletonBit.SolvesWithBoundedError encBits 1 partialVerifier := by + intro a + refine ⟨fun ha => ?_, fun ha => ?_⟩ + · obtain rfl : a = [true] := ha + generalize hk : (1 : Polynomial ℕ).eval (encBits [true]).length = k + rw [Polynomial.eval_one] at hk + subst hk + decide + · obtain rfl : a = [false] := ha + generalize hk : (1 : Polynomial ℕ).eval (encBits [false]).length = k + rw [Polynomial.eval_one] at hk + subst hk + decide + +/-- Majority amplification (`SolvesWithBoundedError.repeatMajority`) reduces the error on +`partialSingletonBit` to `2 ^ (-q(n))` without requiring any margin outside the promise. -/ +example (q : Polynomial ℕ) : + partialSingletonBit.SolvesWithErrorExponent encBits q (12 * q * 1) + (repeatMajority encBits (6 * q) 1 partialVerifier) := + solvesWithBoundedError_partialSingletonBit.repeatMajority q + end ComplexityTests.PromiseProbabilistic