From ddc003e01cdcc5436a6e0f671067a9593b5c0997 Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Sat, 15 Jun 2024 19:17:27 +0100 Subject: [PATCH 1/4] Write down precise constants in the asymptotic complexity 1. Alice takes 5000 k^2 t log t + smaller terms 2. Bob takes 20000/9 k^2 t log t + smaller terms 3. Vera takes 106000 * k^2 + 1 --- Debate/Correct.lean | 30 +--------------------- Debate/Cost.lean | 62 +++++++++++++++++++++++++++++++++++++++++++++ Debate/Details.lean | 37 +++++++++++++++++++++++++++ 3 files changed, 100 insertions(+), 29 deletions(-) diff --git a/Debate/Correct.lean b/Debate/Correct.lean index fe27404..aff7b06 100644 --- a/Debate/Correct.lean +++ b/Debate/Correct.lean @@ -1,3 +1,4 @@ +import Debate.Cost import Debate.Details import Debate.Protocol @@ -24,35 +25,6 @@ theorem soundness (o : Oracle) (L : o.lipschitz t k) (eve : Alice) d ≤ ((debate eve (bob p.s p.b p.q) (vera p.c p.s p.v) t).prob' o).prob false := soundness_p o L eve p m -/-- Default valid parameters (not tuned) -/ -def defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where - v := 1/100 - c := 1/(100*k) - s := 2/(100*k) - b := 5/(100*k) - q := 1/(100*(t+1)) - k0 := k0 - cs := by rw [div_lt_div_right]; norm_num; positivity - sb := by rw [div_lt_div_right]; norm_num; positivity - q1 := by - rw [div_le_one]; apply one_le_mul_of_one_le_of_one_le (by norm_num) - simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]; positivity - v1 := by norm_num - qv := by - rw [←div_div]; apply div_le_self (by norm_num) - simp only [le_add_iff_nonneg_left, Nat.cast_nonneg] - bw := by - simp only [div_eq_mul_inv, mul_inv, ←mul_assoc, mul_comm _ k⁻¹, inv_mul_cancel (ne_of_gt k0)] - norm_num - complete := by - simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)] - rw [mul_comm_div, div_self (Nat.cast_add_one_ne_zero t)]; norm_num - sound := by - simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)] - rw [mul_comm k 5, mul_div_assoc, div_self (ne_of_gt k0), mul_comm_div, - div_self (Nat.cast_add_one_ne_zero t)] - norm_num - /-- The debate protocol is correct with probability 3/5, using the default parameters -/ theorem correctness (k : ℝ) (k0 : 0 < k) (t : ℕ) : let p := defaults k t k0 diff --git a/Debate/Cost.lean b/Debate/Cost.lean index 3782325..4f13084 100644 --- a/Debate/Cost.lean +++ b/Debate/Cost.lean @@ -1,5 +1,7 @@ import Comp.Basic +import Debate.Details import Debate.Protocol +import Mathlib.Data.Complex.ExponentialBounds /-! # Query complexity for each agent in the debate protocol @@ -109,6 +111,44 @@ theorem bob_debate_cost (o : Oracle) (alice : Alice) (vera : Vera) (t : ℕ): · refine exp_le_of_forall_le (fun y m ↦ ?_) induction y; repeat simp only [Comp.cost_pure, le_refl] +/-- `Nat.ceil` adds at most one -/ +lemma Nat.ceil_le_add_one {x : ℝ} (x0 : 0 ≤ x) : ⌈x⌉₊ ≤ x + 1 := by + rw [natCast_ceil_eq_intCast_ceil x0] + exact (Int.ceil_lt_add_one x).le + +/-- Alice makes `O(k^2 t log t)` queries with default parameters -/ +theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) : + let p := defaults k t k0 + (debate (alice p.c p.q) bob vera t).cost' o AliceId ≤ + (t+1) * (5000 * k^2 * Real.log (200 * (t+1)) + 1) := by + refine le_trans (alice_debate_cost _ _ _ _) ?_ + refine mul_le_mul_of_nonneg_left ?_ (by positivity) + simp only [defaults, samples, ← Real.log_inv] + generalize hn : (t+1 : ℝ) = n + field_simp + simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] + norm_num + simp only [mul_comm (Real.log _)] + refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _) + exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith)) + +/-- Bob makes `O(k^2 t log t)` queries with default parameters -/ +theorem bob_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (vera : Vera) : + let p := defaults k t k0 + (debate alice (bob p.s p.b p.q) vera t).cost' o BobId ≤ + (t+1) * (20000 / 9 * k^2 * Real.log (200 * (t+1)) + 1) := by + generalize hd : (20000 / 9 : ℝ) = d + refine le_trans (bob_debate_cost _ _ _ _) ?_ + refine mul_le_mul_of_nonneg_left ?_ (by positivity) + simp only [defaults, samples, ← Real.log_inv] + generalize hn : (t+1 : ℝ) = n + field_simp + simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] + norm_num + simp only [hd, mul_comm (Real.log _)] + refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _) + exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith)) + /-! ### Vera cost @@ -175,3 +215,25 @@ theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ): · simp only [Comp.cost_bind, Comp.cost_allow_all, vera_cost, Comp.prob_allow_all, Comp.cost_pure, exp_const, add_zero, le_refl] · simp only [Comp.cost_pure, Nat.cast_nonneg] + +/-- A calculation used in `vera_fast` -/ +lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by + rw [← le_div_iff (by norm_num), Real.log_le_iff_le_exp (by norm_num)] + norm_num + rw [← Real.exp_one_rpow, div_eq_mul_inv, Real.rpow_mul (by positivity), + Real.le_rpow_inv_iff_of_pos (by norm_num) (by positivity) (by norm_num)] + refine le_trans ?_ (Real.rpow_le_rpow (by norm_num) Real.exp_one_gt_d9.le (by norm_num)) + norm_num + +/-- Vera makes `O(k^2)` queries with default parameters -/ +theorem vera_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (bob : Bob) : + let p := defaults k t k0 + (debate alice bob (vera p.c p.s p.v) t).cost' o VeraId ≤ 106000 * k^2 + 1 := by + refine le_trans (vera_debate_cost _ _ _ _) ?_ + simp only [defaults, samples, ← Real.log_inv] + field_simp + refine le_trans (Nat.ceil_le_add_one (by positivity)) ?_ + simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] + norm_num [← mul_assoc] + refine mul_le_mul_of_nonneg_right ?_ (by positivity) + exact log_mul_le diff --git a/Debate/Details.lean b/Debate/Details.lean index 0da4bcd..6504a83 100644 --- a/Debate/Details.lean +++ b/Debate/Details.lean @@ -604,11 +604,17 @@ Meh, let's get very lazy: /-- A valid set of parameters for the debate protocol -/ structure Params (w d k : ℝ) (t : ℕ) where + /-- Vera's failure probability -/ v : ℝ + /-- Alice's probability goal: Honest Alice's claimed probabilities are usually off by `≤ c` -/ c : ℝ + /-- Vera's acceptance probability goal: Vera usually accepts if probabilities are off by `≤ s` -/ s : ℝ + /-- Vera's rejection probability goal: Vera usually rejects if probabilities are off by `≥ b` -/ b : ℝ + /-- Alice's and Bob's failure probability -/ q : ℝ + /-- Basic inequalities -/ k0 : 0 < k c0 : 0 < c := by positivity cs : c < s @@ -619,7 +625,9 @@ structure Params (w d k : ℝ) (t : ℕ) where v1 : v ≤ 1 qv : q ≤ v bw : k * b ≤ w + /-- Inequality sufficient for completeness -/ complete : d ≤ (1-v) * (w - k * c - q * (t+1)) + /-- Inequality sufficient for soundness -/ sound : d ≤ (1-v) * (1 - q * (t+1)) * (w - k * b) /-- Completeness for any valid parameters -/ @@ -645,3 +653,32 @@ theorem soundness_p (o : Oracle) (L : o.lipschitz t k) (eve : Alice) · apply add_le_add_right m · linarith [p.bw] · apply pow_nonneg; linarith [p.q1] + +/-- Default valid parameters (not tuned) -/ +def defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where + v := 1/100 + c := 1/(100*k) + s := 2/(100*k) + b := 5/(100*k) + q := 1/(100*(t+1)) + k0 := k0 + cs := by rw [div_lt_div_right]; norm_num; positivity + sb := by rw [div_lt_div_right]; norm_num; positivity + q1 := by + rw [div_le_one]; apply one_le_mul_of_one_le_of_one_le (by norm_num) + simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]; positivity + v1 := by norm_num + qv := by + rw [←div_div]; apply div_le_self (by norm_num) + simp only [le_add_iff_nonneg_left, Nat.cast_nonneg] + bw := by + simp only [div_eq_mul_inv, mul_inv, ←mul_assoc, mul_comm _ k⁻¹, inv_mul_cancel (ne_of_gt k0)] + norm_num + complete := by + simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)] + rw [mul_comm_div, div_self (Nat.cast_add_one_ne_zero t)]; norm_num + sound := by + simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)] + rw [mul_comm k 5, mul_div_assoc, div_self (ne_of_gt k0), mul_comm_div, + div_self (Nat.cast_add_one_ne_zero t)] + norm_num From c78c892ed3fe227c5359fe18fd5b9a0db257f24b Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Sat, 15 Jun 2024 19:55:45 +0100 Subject: [PATCH 2/4] Use Nat.ceil_lt_add_one Thanks to Ruben Van de Velde for pointing this out! https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/log.20200.20*.2020000.20.E2.89.A4.20106000/near/444895276 --- Debate/Cost.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/Debate/Cost.lean b/Debate/Cost.lean index 4f13084..0cec7de 100644 --- a/Debate/Cost.lean +++ b/Debate/Cost.lean @@ -111,11 +111,6 @@ theorem bob_debate_cost (o : Oracle) (alice : Alice) (vera : Vera) (t : ℕ): · refine exp_le_of_forall_le (fun y m ↦ ?_) induction y; repeat simp only [Comp.cost_pure, le_refl] -/-- `Nat.ceil` adds at most one -/ -lemma Nat.ceil_le_add_one {x : ℝ} (x0 : 0 ≤ x) : ⌈x⌉₊ ≤ x + 1 := by - rw [natCast_ceil_eq_intCast_ceil x0] - exact (Int.ceil_lt_add_one x).le - /-- Alice makes `O(k^2 t log t)` queries with default parameters -/ theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) : let p := defaults k t k0 @@ -129,7 +124,7 @@ theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) : simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] norm_num simp only [mul_comm (Real.log _)] - refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _) + refine le_trans (Nat.ceil_lt_add_one ?_).le (le_refl _) exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith)) /-- Bob makes `O(k^2 t log t)` queries with default parameters -/ @@ -146,7 +141,7 @@ theorem bob_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (vera : Vera) simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] norm_num simp only [hd, mul_comm (Real.log _)] - refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _) + refine le_trans (Nat.ceil_lt_add_one ?_).le (le_refl _) exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith)) /-! @@ -232,7 +227,7 @@ theorem vera_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (bob : Bob) : refine le_trans (vera_debate_cost _ _ _ _) ?_ simp only [defaults, samples, ← Real.log_inv] field_simp - refine le_trans (Nat.ceil_le_add_one (by positivity)) ?_ + refine le_trans (Nat.ceil_lt_add_one (by positivity)).le ?_ simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] norm_num [← mul_assoc] refine mul_le_mul_of_nonneg_right ?_ (by positivity) From b56e9dbde1c4b919dcc903e0acea25b1185164b2 Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Wed, 28 Aug 2024 18:33:55 +0100 Subject: [PATCH 3/4] Address review comments See https://github.com/google-deepmind/debate/pull/3. --- Debate/Correct.lean | 6 +++--- Debate/Cost.lean | 16 ++++++++-------- Debate/Details.lean | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Debate/Correct.lean b/Debate/Correct.lean index aff7b06..feec70e 100644 --- a/Debate/Correct.lean +++ b/Debate/Correct.lean @@ -27,8 +27,8 @@ theorem soundness (o : Oracle) (L : o.lipschitz t k) (eve : Alice) /-- The debate protocol is correct with probability 3/5, using the default parameters -/ theorem correctness (k : ℝ) (k0 : 0 < k) (t : ℕ) : - let p := defaults k t k0 + let p := Params.defaults k t k0 Correct (3/5) k t (alice p.c p.q) (bob p.s p.b p.q) (vera p.c p.s p.v) where half_lt_w := by norm_num - complete o eve L m := completeness o L eve (defaults k t k0) m - sound o eve L m := soundness o L eve (defaults k t k0) m + complete o eve L m := completeness o L eve (.defaults k t k0) m + sound o eve L m := soundness o L eve (.defaults k t k0) m diff --git a/Debate/Cost.lean b/Debate/Cost.lean index 0cec7de..a9f09fa 100644 --- a/Debate/Cost.lean +++ b/Debate/Cost.lean @@ -113,12 +113,12 @@ theorem bob_debate_cost (o : Oracle) (alice : Alice) (vera : Vera) (t : ℕ): /-- Alice makes `O(k^2 t log t)` queries with default parameters -/ theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) : - let p := defaults k t k0 + let p := Params.defaults k t k0 (debate (alice p.c p.q) bob vera t).cost' o AliceId ≤ (t+1) * (5000 * k^2 * Real.log (200 * (t+1)) + 1) := by refine le_trans (alice_debate_cost _ _ _ _) ?_ refine mul_le_mul_of_nonneg_left ?_ (by positivity) - simp only [defaults, samples, ← Real.log_inv] + simp only [Params.defaults, samples, ← Real.log_inv] generalize hn : (t+1 : ℝ) = n field_simp simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] @@ -129,13 +129,13 @@ theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) : /-- Bob makes `O(k^2 t log t)` queries with default parameters -/ theorem bob_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (vera : Vera) : - let p := defaults k t k0 + let p := Params.defaults k t k0 (debate alice (bob p.s p.b p.q) vera t).cost' o BobId ≤ (t+1) * (20000 / 9 * k^2 * Real.log (200 * (t+1)) + 1) := by generalize hd : (20000 / 9 : ℝ) = d refine le_trans (bob_debate_cost _ _ _ _) ?_ refine mul_le_mul_of_nonneg_left ?_ (by positivity) - simp only [defaults, samples, ← Real.log_inv] + simp only [Params.defaults, samples, ← Real.log_inv] generalize hn : (t+1 : ℝ) = n field_simp simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] @@ -212,7 +212,7 @@ theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ): · simp only [Comp.cost_pure, Nat.cast_nonneg] /-- A calculation used in `vera_fast` -/ -lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by +lemma log_200_mul_20000_le : Real.log 200 * 20000 ≤ 106000 := by rw [← le_div_iff (by norm_num), Real.log_le_iff_le_exp (by norm_num)] norm_num rw [← Real.exp_one_rpow, div_eq_mul_inv, Real.rpow_mul (by positivity), @@ -222,13 +222,13 @@ lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by /-- Vera makes `O(k^2)` queries with default parameters -/ theorem vera_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (bob : Bob) : - let p := defaults k t k0 + let p := Params.defaults k t k0 (debate alice bob (vera p.c p.s p.v) t).cost' o VeraId ≤ 106000 * k^2 + 1 := by refine le_trans (vera_debate_cost _ _ _ _) ?_ - simp only [defaults, samples, ← Real.log_inv] + simp only [Params.defaults, samples, ← Real.log_inv] field_simp refine le_trans (Nat.ceil_lt_add_one (by positivity)).le ?_ simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)] norm_num [← mul_assoc] refine mul_le_mul_of_nonneg_right ?_ (by positivity) - exact log_mul_le + exact log_200_mul_20000_le diff --git a/Debate/Details.lean b/Debate/Details.lean index 6504a83..444e7b1 100644 --- a/Debate/Details.lean +++ b/Debate/Details.lean @@ -655,7 +655,7 @@ theorem soundness_p (o : Oracle) (L : o.lipschitz t k) (eve : Alice) · apply pow_nonneg; linarith [p.q1] /-- Default valid parameters (not tuned) -/ -def defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where +def Params.defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where v := 1/100 c := 1/(100*k) s := 2/(100*k) From 1e348a747482371bf8238615daec89c78a1d4072 Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Mon, 9 Sep 2024 19:05:11 +0100 Subject: [PATCH 4/4] Remove errant space Co-authored-by: Eric Wieser --- Debate/Cost.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Debate/Cost.lean b/Debate/Cost.lean index a9f09fa..519e789 100644 --- a/Debate/Cost.lean +++ b/Debate/Cost.lean @@ -212,7 +212,7 @@ theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ): · simp only [Comp.cost_pure, Nat.cast_nonneg] /-- A calculation used in `vera_fast` -/ -lemma log_200_mul_20000_le : Real.log 200 * 20000 ≤ 106000 := by +lemma log_200_mul_20000_le : Real.log 200 * 20000 ≤ 106000 := by rw [← le_div_iff (by norm_num), Real.log_le_iff_le_exp (by norm_num)] norm_num rw [← Real.exp_one_rpow, div_eq_mul_inv, Real.rpow_mul (by positivity),