Documentation

Complexity.Computability.Circuit.Boolean.HardnessAmplification.WorstCase

From worst-case to average-case hardness by local list decoding #

Let f be a Boolean function on n = m * b bits. Its encoding (Cslib.Circuits.Boolean.hardnessEncode) [STV01] is the concatenation of the Reed–Muller code with the Hadamard code: read f as a function on (BitString b) ^ m, take its low-degree extension p to F ^ m for a field F of q = 2 ^ w elements containing BitString b (Cslib.Code.lowDegreeExtension), a polynomial of total degree at most d = m * (2 ^ b - 1), and output the parity enc (p x) ⬝ r of the w bits of p x selected by r. The encoding is a Boolean function on m * w + w bits (Cslib.Code.concat of the extension with the Hadamard code, Cslib.Circuits.Boolean.hardnessEncode_append_eq_concat). Informally, given the truth table of f and the field arithmetic, it is evaluated with 2 ^ n terms of the extension, in time 2 ^ O(n); this module formalizes no running time.

The reconstruction theorem (Cslib.Circuits.Boolean.complexity_le_of_agree_hardnessEncode): if a circuit of size s agrees with the encoding of f on a 1 / 2 + ε fraction of its inputs, then f has a circuit of size at most reconstructionCost, an explicit polynomial in s, q, 2 ^ K, 3 ^ L, 2 ^ b and the number of monomials M ≤ (D + 1) ^ 2 used by Sudan decoding, for parameters K, L, D satisfying explicit inequalities. The circuit for f is built in four stages, each querying the previous one:

  1. Goldreich–Levin decoding of the inner code, with fixed masks and guess, gives a function G : F ^ m → F that agrees with p on at least an ε / 2 ^ (K + 2) fraction of F ^ m (Cslib.Circuits.Boolean.exists_glPredictor_agree).
  2. Local list decoding along lines with advice (Cslib.Code.lineListDecode) gives a function that computes p at all but a small fraction of the points (Cslib.Code.exists_card_lineListDecode_ne_le).
  3. Self-correction by interpolation along lines and majority trees computes p at every point of the grid h (BitString b) ^ m (Cslib.Code.exists_forall_majTree_eq).
  4. Reading off f from the value of p on the grid.

The stages are bit-blasted De Morgan circuits whose costs are bounded by Cslib.Circuits.Boolean.bitSynthesis_glPredictor, Cslib.Circuits.Boolean.BitSynthesis.lineListDecode and Cslib.Circuits.Boolean.BitSynthesis.selfCorrect. In the ranges forced by the hypotheses the reconstruction cost is at most 2 ^ 11 * 3 ^ L * m * w ^ 2 * q ^ 9 * 4 ^ K * (s + 1) (Cslib.Circuits.Boolean.reconstructionCost_le, Cslib.Circuits.Boolean.complexity_le_pow_of_agree_hardnessEncode). Informally (none of the following asymptotics is formalized here), the smallest admissible parameters have 2 ^ K = O(w / ε ^ 2), 3 ^ L = O((m * b) ^ (log₂ 3)), D = O(√(d * q)) and q = poly(d, w, 1 / ε), so for a block length b = Θ(log (n / ε)) the reconstructed circuit has size polynomial in s, n and 1 / ε, and the encoding has O(n + log (1 / ε)) input bits when m = n / b.

The theorem is nonuniform: the masks and guess of the Goldreich–Levin stage, the advice point of the line stage and the directions of the self-correction stage are fixed by counting arguments, and the circuits are obtained from synthesis bounds rather than constructed by an algorithm. Membership of the encoding in E for f in E, and the derandomization of BPP from worst-case hardness, are separate steps.

Main definitions #

Main results #

References #

The encoding #

source
noncomputable def Cslib.Circuits.Boolean.truthTableExtension {F : Type u_1} {m b : ℕ} [Field F] (h : BitString b ↪ F) (f : BooleanFunction (m * b)) :
(Fin m → F) → F

The low-degree extension of the truth table of f, read as a function on (BitString b) ^ m with values 0 and 1: a codeword of the Reed–Muller code of degree m * (2 ^ b - 1).

Instances For
    source
    theorem Cslib.Circuits.Boolean.truthTableExtension_mem_reedMuller {F : Type u_1} {m b : ℕ} [Field F] (h : BitString b ↪ F) (f : BooleanFunction (m * b)) :
    truthTableExtension h f ∈ Code.reedMuller F m (m * (2 ^ b - 1))

    The extension of a truth table on (BitString b) ^ m is a codeword of the Reed–Muller code of degree m * (2 ^ b - 1).

    source
    theorem Cslib.Circuits.Boolean.truthTableExtension_block {F : Type u_1} {m b : ℕ} [Field F] (h : BitString b ↪ F) (f : BooleanFunction (m * b)) (x : BitString (m * b)) :
    (truthTableExtension h f fun (i : Fin m) => h (x.block i)) = if f x = true then 1 else 0

    On the grid, the extension of a truth table is the truth table: at the point whose coordinates embed the blocks of x, it is 1 if f x and 0 otherwise.

    source
    noncomputable def Cslib.Circuits.Boolean.hardnessEncode {F : Type u_1} {w m b : ℕ} [Field F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) :
    BooleanFunction (m * w + w)

    The worst-case-to-average-case encoding [STV01]. On an input of m * w + w bits, read the first m * w bits as a point x of F ^ m and the last w bits as r, and output the parity enc (p x) ⬝ r of the bits of p x = truthTableExtension h f x selected by r.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.hardnessEncode_append {F : Type u_1} {w m b : ℕ} [Field F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) (x : BitString (m * w)) (r : BitString w) :
      hardnessEncode enc h f (Fin.append x r) = enc (truthTableExtension h f (pointOfBits enc x)) ⬝ᵥ r

      The encoding at the input (x, r) is the parity of the bits of p x selected by r.

      source
      theorem Cslib.Circuits.Boolean.hardnessEncode_append_eq_concat {F : Type u_1} {w m b : ℕ} [Field F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) (x : BitString (m * w)) (r : BitString w) :
      hardnessEncode enc h f (Fin.append x r) = Code.concat (fun (a : F) => BitString.hadamardCode (enc a)) (truthTableExtension h f) (pointOfBits enc x, r)

      The encoding is a concatenated code (Cslib.Code.concat): the outer word is the extension of the truth table, read at the point with bits x, and the inner code is the Hadamard code (Cslib.BitString.hadamardCode) of the bits of the field element.

      The Goldreich–Levin stage #

      source
      theorem Cslib.Circuits.Boolean.exists_glPredictor_agree {F : Type u_1} {w m b : ℕ} [Field F] [Fintype F] [DecidableEq F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) (C : BooleanFunction (m * w + w)) {ε : ℝ} (hε : 0 < ε) (hagree : (1 / 2 + ε) * 2 ^ (m * w + w) ≤ ↑{y : BitString (m * w + w) | C y = hardnessEncode enc h f y}.card) {K : ℕ} (hK : 0 < K) (hsize : ↑w ≤ 2 * (ε / 2) ^ 2 * ↑(2 ^ K - 1)) :
      ∃ (masks : Fin K → BitString w) (guess : BitString K), ε * 2 ^ (m * w) ≤ 2 ^ (K + 2) * ↑{x : Fin m → F | glPredictor enc C masks guess x = truthTableExtension h f x}.card

      The Goldreich–Levin stage. If C agrees with the encoding of f on a 1 / 2 + ε fraction of the inputs and w ≤ 2 * (ε / 2) ^ 2 * (2 ^ K - 1) with K ≥ 1, then for some masks and guess the Goldreich–Levin decoder agrees with the extension of f on at least ε * 2 ^ (m * w) / 2 ^ (K + 2) points of F ^ m.

      The reconstruction theorem #

      source
      def Cslib.Circuits.Boolean.reconstructionCost (w b m D K L s q M : ℕ) :
      ℕ

      The size of the circuit reconstructed from a predictor of size s for the encoding, with K masks, Sudan parameter D with M monomials, majority trees of depth L and a field of q elements: reading the grid point from the input, the self-correction stage over the line stage over the Goldreich–Levin stage, and reading off f from the value of the extension.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.complexity_le_of_agree_hardnessEncode {F : Type u_1} {w m b : ℕ} [Field F] [Fintype F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) {C : BooleanFunction (m * w + w)} {s : ℕ} (hC : complexity interpretation (single C) ≤ s) {ε : ℝ} (hε : 0 < ε) (hagree : (1 / 2 + ε) * 2 ^ (m * w + w) ≤ ↑{y : BitString (m * w + w) | C y = hardnessEncode enc h f y}.card) {K D L : ℕ} (hK : 0 < K) (hsize : ↑w ≤ 2 * (ε / 2) ^ 2 * ↑(2 ^ K - 1)) (hd : 1 ≤ m * (2 ^ b - 1)) (hn : Fintype.card F < (Code.Sudan.monomials (m * (2 ^ b - 1)) D).card) (hmargin : 2 ^ (K + 3) * ↑D ≤ ↑(Fintype.card F) * ε) (herr : 6 * (↑(m * (2 ^ b - 1)) + 1) * (1 / ↑(Fintype.card F) ^ m + 2 ^ (K + 4) / (↑(Fintype.card F) * ε) + ↑D / (↑(Fintype.card F) - 1)) ≤ 1) (hL : m * b ≤ 2 ^ L) :
        complexity interpretation (single f) ≤ reconstructionCost w b m D K L s (Fintype.card F) (Code.Sudan.monomials (m * (2 ^ b - 1)) D).card

        The reconstruction theorem [STV01]. Let F be a field of q elements with an encoding enc : F ≃ BitString w, let h : BitString b ↪ F, let f be a Boolean function on m * b bits, and let d = m * (2 ^ b - 1) ≥ 1. Suppose a Boolean function C with a De Morgan circuit of size at most s agrees with the encoding hardnessEncode enc h f on a 1 / 2 + ε fraction of its 2 ^ (m * w + w) inputs. Let the parameters K ≥ 1, D and L satisfy

        • w ≤ 2 * (ε / 2) ^ 2 * (2 ^ K - 1) (Goldreich–Levin decoding),
        • q < #(Sudan.monomials d D) (more monomials of (1, d)-weighted degree at most D than points on a line; this holds when 2 * d * q < (D + 1) * (D + 2)),
        • 2 ^ (K + 3) * D ≤ q * ε (lines have more than D agreements on average),
        • 6 * (d + 1) * (1 / q ^ m + 2 ^ (K + 4) / (q * ε) + D / (q - 1)) ≤ 1 (few errors are left for self-correction), and
        • m * b ≤ 2 ^ L (majority trees of depth L correct all 2 ^ (m * b) grid points).

        Then f has a De Morgan circuit with at most reconstructionCost w b m D K L s q (#(Sudan.monomials d D)) gates.

        A polynomial bound on the reconstruction cost #

        source
        theorem Cslib.Circuits.Boolean.reconstructionCost_le {w b m D K L s q M : ℕ} (hq : q = 2 ^ w) (hw : 1 ≤ w) (hm : 1 ≤ m) (hb : 2 ^ b ≤ q) (hD : D < q) (hM : M ≤ q ^ 2) (hdq : m * (2 ^ b - 1) + 1 ≤ q) :
        reconstructionCost w b m D K L s q M ≤ 2 ^ 11 * 3 ^ L * m * w ^ 2 * q ^ 9 * 4 ^ K * (s + 1)

        The reconstruction cost is polynomial: with q = 2 ^ w and the parameters in the ranges guaranteed by the hypotheses of complexity_le_of_agree_hardnessEncode (D < q, d + 1 ≤ q, at most q ^ 2 monomials, 2 ^ b ≤ q), the reconstructed circuit has at most 2 ^ 11 * 3 ^ L * m * w ^ 2 * q ^ 9 * 4 ^ K * (s + 1) gates.

        source
        theorem Cslib.Circuits.Boolean.complexity_le_pow_of_agree_hardnessEncode {F : Type u_1} {w m b : ℕ} [Field F] [Fintype F] (enc : F ≃ BitString w) (h : BitString b ↪ F) (f : BooleanFunction (m * b)) {C : BooleanFunction (m * w + w)} {s : ℕ} (hC : complexity interpretation (single C) ≤ s) {ε : ℝ} (hε : 0 < ε) (hagree : (1 / 2 + ε) * 2 ^ (m * w + w) ≤ ↑{y : BitString (m * w + w) | C y = hardnessEncode enc h f y}.card) {K D L : ℕ} (hK : 0 < K) (hsize : ↑w ≤ 2 * (ε / 2) ^ 2 * ↑(2 ^ K - 1)) (hd : 1 ≤ m * (2 ^ b - 1)) (hn : Fintype.card F < (Code.Sudan.monomials (m * (2 ^ b - 1)) D).card) (hmargin : 2 ^ (K + 3) * ↑D ≤ ↑(Fintype.card F) * ε) (herr : 6 * (↑(m * (2 ^ b - 1)) + 1) * (1 / ↑(Fintype.card F) ^ m + 2 ^ (K + 4) / (↑(Fintype.card F) * ε) + ↑D / (↑(Fintype.card F) - 1)) ≤ 1) (hL : m * b ≤ 2 ^ L) :
        complexity interpretation (single f) ≤ 2 ^ 11 * 3 ^ L * m * w ^ 2 * Fintype.card F ^ 9 * 4 ^ K * (s + 1)

        The reconstruction theorem with a polynomial bound [STV01]. Under the hypotheses of complexity_le_of_agree_hardnessEncode, with q = |F| = 2 ^ w, the function f has a De Morgan circuit with at most 2 ^ 11 * 3 ^ L * m * w ^ 2 * q ^ 9 * 4 ^ K * (s + 1) gates.