Formal verification confirms limits of circuits computing parity function
Formalizing PARITY Circuit Lower Bounds in Lean
Computational ComplexityLogic in Computer Science
Summary
Some problems are harder to compute with certain kinds of simple circuits than others. This work uses a computer tool called Lean to carefully prove that making a circuit that computes the parity (odd or even count of bits) requires a lot of size if the circuit has limited depth. The authors also show a way to build small and efficient formulas for parity with slightly different circuit rules, confirming known boundaries between complexity classes. This formal proof in Lean helps ensure these complexity results are error-free.
What this means in practice
- •For hardware engineers: Use formal bounds to evaluate feasibility of low-depth circuit designs for parity computations in hardware.
- •For software verification teams: Incorporate formal proofs of circuit complexity limits into verification workflows to ensure correctness of crucial computational components.
A theory result. No direct application yet.
Authors
Saint Wesonga
Abstract
We formalize Hastad's PARITY lower bound in Lean using the switching lemma. For every fixed d >= 2, formulas and DAG circuits of computation depth at most d computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))) for all sufficiently large n. This matches the classical upper bound up to constants in the exponent and implies that PARITY is not in nonuniform AC0. We also construct a polynomial-size, logarithmic-depth bounded-fan-in formula family for PARITY, providing a witness to NC1 is not a subset of AC0 for the formalized models. The Lean source code is available at https://github.com/formalcs/circuit-complexity and is checked with Lean 4.33.1 and mathlib 4.33.1.