{"id":"739b6310-7bb6-43db-a418-a8bc86b04c6a","arxiv_id":"2411.14268","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A new family of 3-CNF bracket formulas yields the first supercritical size-depth tradeoff for monotone circuits.","lead":"This paper proves that some monotone Boolean functions have a sharp size-depth tradeoff: they can be computed by quasipolynomial-size circuits, but any circuit of polynomial depth must be exponentially larger. It is the first proof of such a supercritical tradeoff for monotone circuits, settling a conjecture and introducing a new family of hard logic formulas called bracket formulas.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the supercritical tradeoff argument is coherent and internally consistent.","rationale":"The reader's weakest assumption targeted the recursive adversary strategy and the Cover/Size/Buffer Lemmas in Section 4. I agree that this is the most delicate part of the paper and the place where a hidden error would be most dangerous. However, on close reading the proof is internally consistent: the adversary maintains a container, Move recentres the separation interval before each recursive call, and the Cover Lemma's inductive accounting with A_ell gives enough room for the Size Lemma. The only concrete issue I found is a misstated bound on A_ell in Section 4.3, which is easily corrected to O(d w^{ell0-ell}) and does not affect the argument. The lifting theorems are used in a black-box manner appropriate for the stated parameters, and the derivation of Theorems 1 and 2 from Theorems 3 and 4 is sound. Since no actual flaw was identified, the appropriate outcome is to keep the reader's ACCEPT verdict unchanged rather than manufacture a concern. A formalization or exhaustive small-case simulation would be a valuable extra assurance but is not required to fix a known gap.","tokens_in":20252,"tokens_out":34009,"duration_ms":341055,"concrete_test":"Independently formalize Lemmas 12-18 for Algorithm 1 in a proof assistant (e.g., Lean or Isabelle), including the recurrence for A_ell and the Cover Lemma induction. Alternatively, implement the adversary for small parameters (n=2^10, w=4, e=0.1) and exhaustively simulate all prover query/forget sequences of length d^{ell0}, checking that the container invariant, the interval lower bound |I| >= n/(4w)^ell, and the Cover Lemma bound |area(C_i) cap I| <= w(A_{ell+1}+3i) all hold at every step.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After checking the recursive adversary argument in Section 4, I do not find a load-bearing flaw. The central claim rests on Theorem 4, whose Cover, Size, and Buffer Lemmas are intricate, but the area accounting checks out. Solving the recurrence A_ell = w(A_{ell+1}+3d), A_ell0=3d gives A_ell = O(d w^{ell0-ell}) = O(n^{2e}); the manuscript's intermediate bound A_ell <= O(d^{ell0} w^{ell0}) = O(n^{3e}) in Section 4.3 appears to be a typographical slip, and the intended estimate is sufficient for Eq. (4). The Move operation's claimed additional-area bound of 2w is plausible because the chosen uncovered interval is maximal, so a new opposite-colour pair can be anchored just outside the assigned block. Lemma 18's buffer argument gives the needed disjointness of legacy ancestors, and the lifting steps in Section 5 are standard with consistent parameter bookkeeping. The remaining risk is that the interval estimates in Section 4 are not machine-checked; this is a verification gap rather than an identified error.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proves a supercritical size-depth tradeoff for monotone circuits: it exhibits a monotone function f on n bits that is computable by monotone circuits of quasipolynomial size, while every monotone circuit of polynomial depth computing f requires exponential size. The proof goes through a new family of unsatisfiable 3-CNF formulas, called bracket formulas Br_n. The authors show that Br_n has resolution refutations of width O(log n) (Section 3) and, by a recursive prover-adversary strategy maintaining containers and buffers, that every width-w resolution refutation of Br_n has depth n^{Omega(log n / log w)} (Section 4). These width-depth tradeoffs are then lifted through known dag-like lifting theorems to size-depth tradeoffs for resolution and, ultimately, to the monotone circuit result (Section 5). The paper also discusses the relationship of bracket formulas to TFNP classes and compares the result with concurrent work.","tokens_in":20466,"tokens_out":19017,"duration_ms":189699,"significance":"If the proofs are completed as intended, this is an important result: it is the first supercritical size-depth tradeoff for monotone circuits, resolving a direction conjectured in prior work, and it introduces a clean new combinatorial principle that may be of independent interest. The paper is careful to state exactly how its parameters compare with the stronger conjectures and with the concurrent work of de Rezende et al. The upper-bound argument and the overall lifting architecture are clear. The main lower-bound proof in Section 4 is intricate and not machine-checked; in its current written form it contains a miscomputed estimate and a missing implication in the last lifting step, so I cannot recommend acceptance without revision.","major_comments":[{"comment":"The step 'For small delta this contradicts Theorem 2' is not justified as written. Theorem 21 applied to F := Br_n yields a resolution refutation Pi of Br_n, whereas Theorem 2 is a lower bound for the composed formula Br_n composed with the indexing gadget. No statement in the paper converts a shallow and small resolution proof of Br_n into a shallow and small resolution proof of that composed formula: Claim 20 controls only size, not depth, and the alternative route of applying Theorem 21 directly to the composed formula is not what is written. This is a load-bearing gap for the monotone circuit lower bound. Please either insert an explicit depth-preserving (and, where needed, width-preserving) simulation lemma for composition with the indexing gadget, or restructure the proof to apply Theorem 21 to Br_n composed with Ind and then invoke Theorem 19.","section":"Section 5, proof of Theorem 1"},{"comment":"The displayed bound A_l <= O(d^{ell0} w^{ell0}) = O(n^{3 epsilon}) does not follow from the recurrence A_l = w(A_{l+1} + 3d), A_{ell0} = 3d. Solving the recurrence gives A_l = O(d * w^{ell0 - l}), which with the stated parameters is O(n^{2 epsilon}) at l = 0; the term d^{ell0} is not polynomial in n. Since Eq. (4) is used in the Size Lemma to guarantee |I_i| >= n/(4w)^{ell+1}, the estimate must be corrected (or proved by a different induction) before the proof of Lemma 12 can be considered complete. The intended estimate is probably sufficient, but the written bound is false.","section":"Section 4.3, Eq. (4)"},{"comment":"The proof of Lemma 11 says 'By construction it should be evident' and leaves the main invariant (that the maintained interval I is a subinterval of the separation interval and that Move preserves the domination of the game state rho) largely informal. Because the container invariant is what prevents the prover from winning, the induction should be stated with explicit invariant conditions and a precise definition of the failure condition. This may be a presentation issue rather than an error, but as written it makes the correctness of the adversary strategy difficult to verify.","section":"Section 4.2, Lemma 11"}],"minor_comments":[{"comment":"The symbol n is used both for the number of variables of Br_n and for the number of variables of the composed formula Br_n composed with Ind, which has about n^{2+epsilon} variables. The proof should state the final lower bound with explicit variable counts or a reparameterization, so that width n^delta / log n and depth n^{gamma + delta / log n} are not ambiguous.","section":"Section 5, proof of Theorem 2"},{"comment":"In the proof of Lemma 17, the sentence about adding 'all trivial bracket pairs in tilde C_i' to the set U should say that the areas of those trivial pairs are added; otherwise the size bound |U_{i+1}| <= 3w is not immediate.","section":"Section 4.3, Lemma 17"},{"comment":"In Eq. (3) and the surrounding text, tilde I_i and I_i are used somewhat interchangeably; the distinction between the interval found before the Move operation and the interval after the Move operation should be made explicit, and Eq. (5) should be checked against Algorithm 1.","section":"Section 4.3, Size Lemma"}],"recommendation":"major_revision","confidential_remarks":"The manuscript contains a genuinely interesting contribution and the core adversary argument appears sound in outline. However, the current text is not ready for acceptance: the proof of Theorem 1 relies on an unstated implication between a resolution proof of Br_n and the hard formula of Theorem 2, and the estimate in Eq. (4) is miscomputed. Both are repairable, so I recommend major revision rather than rejection. The reader's accept verdict is more optimistic than mine, mainly because the final lifting step needs a missing simulation lemma."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: this is a legitimate advance. It gives the first supercritical size-depth tradeoff for monotone circuits, via a new family of 3-CNFs (bracket formulas) with a resolution width-depth tradeoff. The lifting from resolution to circuits is black-box, so the core work is the bracket formulas and the adversary argument in Section 4. I agree with the reader: the paper deserves acceptance; the proofs are detailed and the related work (including concurrent dRFJ+24) is handled honestly.\n\nThe genuinely new thing is Theorem 4: every width-w resolution refutation of the bracket formula needs depth n^{Omega(log n/log w)}. That is what makes the tradeoff 'supercritical' in the sense conjectured. The upper bound (width O(log n)) is simple and elegant—the prover-adversary strategy that keeps only O(log n) pairs in memory is convincing. The lower bound is where the risk lives.\n\nSection 4 is intricate. The recursive adversary with containers, buffers, and legacy ancestors is hard to check line by line. The stress-test note confirms the area accounting works out; the apparent bound A_ell <= O(n^{3e}) in Section 4.3 is a harmless overestimate (the recurrence gives O(n^{2e})). I'd flag that as a typo, not a bug. The bigger soft spot is that the Cover, Size, and Buffer Lemmas involve several 'by construction it should be evident' steps. That is normal for this kind of argument, but it means the proof needs a careful pass by the authors (or a referee) to remove informal justification. It is a verification gap, not a discovered error.\n\nOne thing I'd double-check if I were refereeing: the claim that 'the Move operation is the only source of non-trivial bracket pairs in the container'—I trust it but the picture in Section 4.2 is doing a lot of work. And the parameter bookkeeping in the recursion (ell_0 = floor(epsilon log n / log w), d = floor(n^epsilon)) is consistent, as the stress-test says.\n\nThe citation pattern looks fine. They use [GGKS20, LMM+22, FPR22] as black boxes and explicitly acknowledge concurrent work. The discussion of hardness condensation is useful context, not overselling.\n\nWho is this for? Proof complexity and monotone circuit people. It resolves a conjecture in a weaker quantitative form, with a new technique that may find other uses. It is not a civilizational result but it is a real one.\n\nRecommendation: send to a serious referee. I'd accept for peer review with confidence, expecting the main proof to survive with minor fixes. The paper should also be asked to correct the O(n^{3e}) typo and to tighten the informal steps in Section 4.","headline":"First supercritical monotone circuit tradeoff via a new bracket-formula width-depth lower bound; the proof is intricate but the stress-test holds, so this deserves serious refereeing.","tokens_in":20964,"tokens_out":1937,"would_cite":true,"duration_ms":17718,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","03F20"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper constructs a monotone function computable in quasipolynomial size for which every polynomial-depth monotone circuit needs exponential size.","keywords":["monotone circuits","size-depth tradeoff","resolution proof complexity","bracket formulas","supercritical tradeoff","width-depth tradeoff","lifting","prover-adversary games"],"falsifier":"Run the resolution game on the bracket formula with memory about $n^{{1/3}}$ and count the rounds: if the prover can force a falsified axiom in fewer than $n^{{Ω(log n / log w)}}$ rounds, the width–depth lower bound is false, and since the circuit tradeoff is derived from it by lifting, the main circuit theorem would fall as well.","tokens_in":20079,"feed_emoji":"🧮","tokens_out":9550,"duration_ms":81098,"temperature":0.7,"pith_summary":"The paper proves a supercritical size–depth tradeoff for monotone circuits: there is a monotone function f that some monotone circuit computes in quasipolynomial size, yet every monotone circuit of polynomial depth needs exponential size. This is the first result of this kind in the regime where the allowed depth is well above the critical value, and it answers a conjecture from earlier work even though it does not yet reach the conjectured quantitative parameters. The proof goes through proof complexity: the paper introduces a new family of unsatisfiable 3-CNF formulas, the bracket formulas, that have quasipolynomial-size resolution refutations but require exponential size for any polynomial-depth refutation. A lifting theorem then carries that tradeoff from resolution to monotone circuits.","feed_headline":"One function costs exponentially more at shallow monotone depth","feed_subtitle":"A quasipolynomial-size monotone circuit exists, but any polynomial-depth monotone circuit needs exponential size.","key_machinery":"The load-bearing object is the bracket formula Brn, a 3-CNF encoding of the bracket principle using pointer variables that name each bracket's mate; a well-parenthesised string is forced to contain the forbidden substring ][. The proof works in the prover–adversary game characterization of resolution width and depth. The upper bound is a recursive prover strategy that queries and forgets whole bracket pairs, keeping only O(log n) symbols in memory. The lower bound is an adversary strategy maintaining a 'container', a minimal monotone set of top-level bracket pairs that dominates the game state; nested recursion, buffer intervals, and the Cover, Size, and Buffer Lemmas bound how many indices the container may cover. Finally, dag-like lifting theorems from resolution to monotone circuits convert the width–depth tradeoff into size–depth tradeoffs.","core_discovery":"The central claim is that a simple combinatorial principle about brackets—every red/blue well-parenthesised string starting with a red bracket and ending with a blue bracket must contain the substring ][—can be encoded as a 3-CNF that is easy to refute in width but hard to refute in depth. Concretely, the bracket formula Brn admits a resolution refutation of width O(log n), and every width-w resolution refutation of Brn has depth $n^{{Ω(log n/log w)}}$. Lifting theorems then turn this width–depth tradeoff into the main circuit theorem: a monotone function computable in size $n^{{O(log n)}}$ such that every depth-$n^{{O(1)}}$ monotone circuit computing it has size exp($n^{{Ω(1)}}$). The same argument yields the analogous size–depth tradeoff for resolution, with the lower bound actually holding for semantic cutting planes as well.","pith_inferences":["Beyond the paper: the natural strengthening is to make the blow-up occur already at depth S^ε, where S is the quasipolynomial size of the efficient circuit; the conjecture from earlier work asks for exactly this, and the bracket-formula construction does not obviously obstruct it.","Beyond the paper: the bracket principle is known to sit between the TFNP classes UEOPL and EOPL, and the paper's low-width refutation shows the principle is easy in a PLS-like sense; classifying whether the principle is complete for any named class would tie these proof-complexity tradeoffs to search problems.","Beyond the paper: the paper leaves open whether bracket formulas can give Weisfeiler–Leman refinements analogous to those obtained from condensed Tseitin formulas; testing the bracket formulas in that setting is a concrete transfer question."],"forward_implications":["Every polynomial-depth monotone circuit for the exhibited function needs size exp(n^{Ω(1)}), so polynomial depth does not buy small size in the supercritical regime.","The bracket formulas give the first resolution size–depth tradeoff for a genuine 3-CNF, avoiding the quasipolynomial-clause limitation of prior tradeoffs.","The same lifting route yields an analogous size–depth tradeoff for cutting planes refutations.","Because the depth lower bound holds for every width w, the proof also yields a width–depth tradeoff: refuting Brn at width w requires depth n^{Ω(log n/log w)}.","The gap in the circuit result is from quasipolynomial size in the unrestricted-depth upper bound to exponential size under any polynomial depth restriction."],"supporting_citations":[{"why":"Its lifting theorems convert resolution width–depth bounds into monotone circuit size–depth bounds and also stated the supercritical conjecture the paper resolves.","marker":"[GGKS20]"},{"why":"Provides the previous best resolution size–depth tradeoff and the exact lifting statements the paper quotes; its quasipolynomial-clause limitation is what bracket formulas overcome.","marker":"[FPR22]"},{"why":"A simpler proof of the earlier resolution tradeoff that marks the prior state of the art which the new 3-CNF result surpasses.","marker":"[BT24]"},{"why":"Characterizes resolution depth via prover–adversary games, the setting used for the lower bound.","marker":"[Pud00]"},{"why":"Characterizes resolution width via prover–adversary games, used to phrase and prove the width and depth bounds.","marker":"[AD08]"},{"why":"Supplies the composition lemma that turns width-size refutations into small refutations after gadget composition.","marker":"[SBI04]"},{"why":"Refines the lifting construction and is cited as part of the lifting theorems used for the main results.","marker":"[LMM+22]"},{"why":"Gives the width–size relation that links narrow refutations to small ones, motivating the lifting step.","marker":"[BW01]"}],"fun_headline_variants":["Shallow depth makes monotone circuits pay exponential price","Monotone circuits: shallow depth costs exponential size","Depth vs size for monotone: poly depth costs exponential","Quasipoly size but poly depth requires exponential size","Supercritical tradeoff: quasipoly size vs exponential at poly depth"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The lower bound rests on the recursive adversary maintaining a minimal 'container' of the game state, together with the Cover, Size, and Buffer Lemmas that bound how many positions that container covers; if those interval-area estimates are off, the exponential depth lower bound collapses.","fun_headline_variants_meta":{"raw":{"variants":["Shallow depth makes monotone circuits pay exponential price","Monotone circuits: shallow depth costs exponential size","Depth vs size for monotone: poly depth costs exponential","Quasipoly size but poly depth requires exponential size","Supercritical tradeoff: quasipoly size vs exponential at poly depth"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001485,"raw_usage":{"total_tokens":5889,"prompt_tokens":798,"completion_tokens":5091,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":414,"completion_tokens_details":{"reasoning_tokens":5009}},"tokens_in":414,"tokens_out":5091,"duration_ms":32762,"temperature":1.0,"reasoning_tokens":5009,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:21:40.469989+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the resolution game on the bracket formula with memory about $n^{{1/3}}$ and count the rounds: if the prover can force a falsified axiom in fewer than $n^{{Ω(log n / log w)}}$ rounds, the width–depth lower bound is false, and since the circuit tradeoff is derived from it by lifting, the main circuit theorem would fall as well.","supporting_citations":[],"review_version":1}