Repository navigation
refactor(ArthurMerlin): factor MA/AM amplification through BPP per-instance error bounds (#949) - #1400
Conversation
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1400 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at aea0686b0744ddf48495e30d94c2e4a130808df6
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
This PR routes the per-instance error bounds for BPP, MA and AM through shared predicates, so that MA/AM amplification and the 2^(-e) ≤ 1/4 → 2/3 step become short corollaries of the BPP lemmas. Thanks, the amplification proofs are much shorter now.
Classification. This is a refactor that keeps the meaning of existing statements, but it also adds new public API, so the delegated-review exception does not apply. I checked every redefined public predicate against its old body: SolvesWithBoundedError, SolvesWithErrorExponent, IsMerlinArthurVerifier, IsMerlinArthurVerifierWithErrorExponent, IsArthurMerlinVerifier and IsArthurMerlinVerifierWithErrorExponent. Each unfolds to its old body by delta/beta reduction plus !true ≡ false / !false ≡ true. For example, BoundedErrorAt enc p (fun z => V (z.1, List.ofFn y ++ z.2)) a true unfolds to the old filter on V (a, List.ofFn y ++ List.ofFn r) = true. So BPP, PromiseBPP, MA and AM are unchanged. The Sipser–Lautemann abstract bridge (mem_BPP_iff, which proves the abstract's self-contained BPP equals Cslib.Complexity.BPP encBits with simp only) needed no edit, which is a useful independent check. No public declaration was removed; only the private merlinArthurRepeat_ofFn_append_ofFn was replaced. New public declarations: outcomeCount, BoundedErrorAt, ErrorExponentAt, arthurMerlinAcceptCount, arthurMerlinRejectCount, arthurMerlinSlice, the two isArthurMerlinVerifier…_iff_decides… equivalences, and per-instance lemmas (BoundedErrorAt.repeatMajority, ErrorExponentAt.boundedErrorAt, .congr, .not, and the outcomeCount_* lemmas). They are mathematically routine; no new headline result.
Abstract impact. None. The SipserLautemann abstract has its own BPP and is unaffected, and the bridge is unchanged. This matches the PR's no-impact assessment.
Blocking
outcomeCount V a n trueduplicatesCslib.Complexity.acceptCount(Classes/SharpP.lean), which has exactly the same body, andoutcomeCount_true_add_outcomeCount_falserestatesacceptCount_add_card_filter_eq_false. The diff already shows the two parallel notions in use:change _ * acceptCount … ≤ _inSBP.lean,rw [← acceptCount]inPromise/Randomized.lean, andexact acceptCount_andVerifier …proving anoutcomeCount … trueequation inBPP/Amplification.lean. AGENTS.md treats this as a finding and asks the PR to name the existing notions it considered. See the inline comment for options.ci-checksis still in progress on this head, so the required check is not yet green. Please confirm it passes on the revision submitted for re-review.
Nits (non-blocking)
- Use
abbrevrather than@[reducible] defforoutcomeCount,BoundedErrorAt,ErrorExponentAt,arthurMerlinAcceptCountandarthurMerlinRejectCount(Mathlib style). - The
ArthurMerlin/Amplification.leanmodule docstring should listisArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponentunder Main results, matching its bounded-error counterpart inArthurMerlin.lean. - The PR body says "no new mathematical theorems". That is fair as a mathematical classification, but it would help to also state that the PR adds public definitions and per-instance lemmas, so reviewers apply the right review rule.
Limits: I did not build locally and relied on the author's reported scripts/check.sh run for compilation, with CI still pending. I sampled the client proof edits rather than re-deriving each one.
|
|
||
| /-- The number of strings `r` of length `n` with `V (a, r) = b`. -/ | ||
| @[reducible] | ||
| def outcomeCount (V : α × List Bool → Bool) (a : α) (n : ℕ) (b : Bool) : ℕ := |
There was a problem hiding this comment.
Blocking (duplication). At b = true this has exactly the body of Cslib.Complexity.acceptCount (Classes/SharpP.lean:70): (univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card. Likewise, outcomeCount_true_add_outcomeCount_false (line 113) restates acceptCount_add_card_filter_eq_false. Several clients in this PR now switch between the two by definitional unfolding (SBP.lean, Promise/Randomized.lean, the hc step in BPP/Amplification.lean).
I understand that BPP.lean does not import SharpP (it pulls in NP), which is presumably why the new count lives here. A concrete fix: move outcomeCount and its lemmas to a small low module that both BPP.lean and SharpP.lean import. Then define acceptCount V a n := outcomeCount V a n true as an abbrev, or restate acceptCount in terms of it, and state acceptCount_add_card_filter_eq_false through outcomeCount_add_outcomeCount_not, so there is a single counting notion. If you would rather keep this PR bounded, please say in the description that acceptCount was considered and why it was not reused, and open a follow-up issue naming both declarations, their consumers and the proposed home.
| /-- The number of random strings `r` of length `m` for which some reply `y` of length `n` is | ||
| accepted by `V` on `a`. -/ | ||
| @[reducible] | ||
| def arthurMerlinAcceptCount (V : α × List Bool → Bool) (a : α) (m n : ℕ) : ℕ := |
There was a problem hiding this comment.
nit: These two abbreviations are public API that mostly keeps IsArthurMerlinVerifier's body syntactically close to the old one. The cost is that several clients now need simp only [arthurMerlinAcceptCount, arthurMerlinRejectCount, …] (in PH.lean, SetLowerBound.lean, mem_AM, MA_subset_AM and mem_AM_of_exists). Since isArthurMerlinVerifier_iff_decidesWithBoundedError already provides the bridge to outcomeCount, consider inlining the filters again or making these private. If you keep them, abbrev is the idiomatic spelling of @[reducible] def.
| ∀ y : Fin n → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card | ||
|
|
||
| /-- Whether some reply `y` of length `q(|x.1|)` is accepted by `V` on `(x.1, x.2 ++ y)`. -/ | ||
| def arthurMerlinSlice (enc : α ↪ List Bool) (q : Polynomial ℕ) (V : α × List Bool → Bool) |
There was a problem hiding this comment.
nit: Please add a sentence to the docstring saying that this is a counting device rather than a polynomial-time verifier: it quantifies over all 2^{q(n)} replies, so DecidesWithBoundedError … (arthurMerlinSlice enc q V) A should not be read as an AM ⊆ BPP-style statement. DecidesWithBoundedError carries no computability requirement, so the equivalence is correct as stated; the note only prevents misreading.
|
Updated in
Full |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1400b for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 104a2a82a76a5b8fd130048b2030f092d1abf9f8
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
This re-review covers the delta since aea0686b and the findings of the earlier review. Thanks for the quick turnaround. The duplication is fixed cleanly, and the amplification proofs are still short corollaries of the per-instance lemmas.
Earlier findings
- Duplicated count (blocking): resolved.
outcomeCountand its lemmas are gone.BoundedErrorAtandErrorExponentAtnow inline theFinset.univ.filtercount, and the clients (inter_mem_BPP,PP,SBP,Promise/Randomized) useacceptCountandacceptCount_add_card_filter_eq_falsedirectly. There is no remaining reference tooutcomeCount,arthurMerlinAcceptCountorarthurMerlinRejectCountat this head, and nothing else in the library defines a per-instance bounded-error or error-exponent predicate. - Nits: all addressed. The two predicates are now
abbrevs, the AM count aliases are inlined again,arthurMerlinSlicenotes that it is a counting device, the Amplification module docstring lists the error-exponentiff, and the PR body mentions the new public API. - CI pending (blocking): now failing, see below.
Statements. The delta changes no statement. IsArthurMerlinVerifier and IsArthurMerlinVerifierWithErrorExponent again have their original bodies. SolvesWithBoundedError, SolvesWithErrorExponent, IsMerlinArthurVerifier and IsMerlinArthurVerifierWithErrorExponent unfold to their old bodies through the abbrevs, as in the earlier review, so BPP, PromiseBPP, MA and AM are unchanged. One edge case I checked: ErrorExponentAt … a true bounds the count of V (a, r) = !true, which reduces to the old = false count by Bool.not_true.
Abstract impact. None, as the PR says. The Sipser–Lautemann bridge needs no change.
Blocking
ci-checksfails on this head (run), inlake test:This is a semantic conflict withComplexityTests/PromiseProbabilistic.lean:115:4: Tactic `decide` failed to reduce @decide (BoundedErrorAt encBits 1 partialVerifier [true] true) (and :120:4 for [false] false)main, not with this branch alone.solvesWithBoundedError_partialSingletonBitarrived onmainin #1389, after this branch's merge base, so a localscripts/check.shon the branch would not have hit it. The cause is the abbrev: the goal is nowBoundedErrorAt encBits 1 partialVerifier [true] true, sogeneralize hk : (1 : Polynomial ℕ).eval (encBits [true]).length = kfinds no visible occurrence to abstract, anddecidethen gets stuck onPolynomial.eval. Please rebase onto currentmainand adddsimp only [BoundedErrorAt](orunfold BoundedErrorAt) before eachgeneralizein that test, as this PR already does inComplexityTests/SipserLautemann.lean. Then re-run the fullscripts/check.shon the rebased head.
No other findings in the delta.
Limits: I did not build locally. I identified the failure from the CI log and the main version of the test, and I have not checked the suggested fix in Lean. I sampled the client proof edits in the delta rather than re-deriving each one.
| DecidesWithBoundedError encBits (Polynomial.C 2) noisyHeadVerifier | ||
| {x : List Bool | x.headD false = true} := by | ||
| intro a | ||
| dsimp only [DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError, BoundedErrorAt] |
There was a problem hiding this comment.
The same unfolding is needed before generalize in solvesWithBoundedError_partialSingletonBit (ComplexityTests/PromiseProbabilistic.lean, lines 112 and 117 on current main, from #1389). Without it, generalize cannot see Polynomial.eval 1 … inside BoundedErrorAt, decide gets stuck, and ci-checks fails on this head. That test is not in this PR's diff because it landed after the merge base, so it needs a rebase first.
…stance error bounds (#949)
104a2a8 to
123a6f0
Compare
|
Rebased onto
Ready for re-review at |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1400c for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 123a6f04456fac826acf9461dcdae5cf0942cb05
Independence: the author is a separate Jetski session outside this coordinator's delegation chain.
This delta re-review covers the change since the review at 104a2a82. That review asked for one fix: lake test failed at ComplexityTests/PromiseProbabilistic.lean:115/120, where this PR conflicted with the test added in #1389. The fix is resolved.
- Rebase: the branch is rebased onto
origin/main(206ff070).git range-diffshows that both original commits (80b67eb3,22d5cc56) are patch-identical to the reviewedaea0686b/104a2a82. Library declarations and public statements are therefore unchanged since the last review. - New commit:
123a6f04adds onlydsimp only [BoundedErrorAt]before eachgeneralizein the two branches ofsolvesWithBoundedError_partialSingletonBit. This is the fix the last review suggested. It changes the test proof only, not its statement. - CI:
ci-checksandcheck-titleare green on123a6f04456fac826acf9461dcdae5cf0942cb05, and the PR is mergeable.
The mathematical content and the abstract impact are as assessed in the earlier reviews: this is an internal API/proof refactor with no headline abstract affected. This delta review did not re-examine unchanged code.
Addresses #949 (comment 113 item 9b).
Summary
This refactoring extracts per-instance bounded-error and error-exponent predicates in
BPPandBPP.Amplificationand routesMAandAMerror amplification through them, while adding the small public per-instance API needed by downstream callers (no new headline mathematical theorems).Complexity.Computability.Complexity.Classes.BPP:Cslib.Complexity.BoundedErrorAt,BoundedErrorAt.congr, andBoundedErrorAt.notas the per-instance bounded-error predicate (abbrevover the existingFinset.univ.filtercount, avoiding any duplicate counting declaration alongsideCslib.Complexity.acceptCount).PromiseProblem.SolvesWithBoundedErrorandSolvesWithBoundedError.complthroughBoundedErrorAt.Complexity.Computability.Complexity.Classes.BPP.Amplification:Cslib.Complexity.ErrorExponentAt,ErrorExponentAt.congr,BoundedErrorAt.repeatMajority, andErrorExponentAt.boundedErrorAt(proved viaBitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le).PromiseProblem.SolvesWithErrorExponent,SolvesWithBoundedError.repeatMajority, andSolvesWithErrorExponent.solvesWithBoundedErroras point-wise corollaries of the per-instance lemmas.Complexity.Computability.Complexity.Classes.ArthurMerlin&ArthurMerlin.Amplification:IsMerlinArthurVerifierandIsMerlinArthurVerifierWithErrorExponentdirectly in terms ofBoundedErrorAtandErrorExponentAton the proof-sliced verifierfun z => V (z.1, List.ofFn y ++ z.2).Cslib.Complexity.arthurMerlinSlice(the reply-existence counting slicedecide (∃ y, V (x.1, x.2 ++ List.ofFn y) = true)) and provesisArthurMerlinVerifier_iff_decidesWithBoundedErrorandisArthurMerlinVerifierWithErrorExponent_iff_decidesWithErrorExponent.IsMerlinArthurVerifier.repeatMajority,IsMerlinArthurVerifierWithErrorExponent.isMerlinArthurVerifier,IsArthurMerlinVerifier.repeatMajority, andIsArthurMerlinVerifierWithErrorExponent.isArthurMerlinVerifierto one-line corollaries ofBoundedErrorAt.repeatMajorityandErrorExponentAt.boundedErrorAt.Abstract Catalogue Impact
No headline abstract in
abstracts/catalogue.jsonis affected by this internal proof/API refactoring.Validation
./scripts/check.sh(lake build --wfail --iofail,lake exe mk_all --check,lake test --wfail --iofail,lake lint,lake exe lint-style,lake exe checkInitImports) passed.python3 -B scripts/check_tidy_surface.py,python3 -B scripts/check_hygiene.py --check-simp, andpython3 -B scripts/check_changed_files.py --base origin/mainpassed.AI Disclosure
Authored by
worker-jetski-71eb65fe(Gemini / Jetski).