Reproduce “Convergent Gate Elimination and Constructive Circuit Lower Bounds” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Marco Carmosino, Ngu Dang, Tim Jackman
This research formalizes gate elimination as a convergent term graph rewriting system for DeMorgan and {∧,⊕,¬} bases, while identifying non-confluence in U2 and B2 bases. It then applies this formalized approach to yield the first constructive circuit lower bound via gate elimination, providing an efficient algorithm to find counterexamples for DeMorgan circuits attempting to compute XOR_n with fewer than 3(n-1) gates.
Key insights
- Gate elimination can be formalized as a convergent term graph rewriting system for DeMorgan and {∧,⊕,¬} bases, ensuring unique normal forms regardless of simplification order.
- The choice of Boolean basis fundamentally impacts formal simplification properties; U2 and B2 bases do not support confluent simplification.
- Gate elimination, a "simple" and inductive proof technique, can be leveraged to provide constructive circuit lower bounds, generating explicit counterexamples.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.