{"id":"f9c2b628-1f00-46b2-a708-872a15c93129","arxiv_id":"2506.17210","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A new family of knapsack polynomials over finite fields requires super-polynomial-size refutations in constant-depth multilinear Ideal Proof System, with additional roABP lower bounds and a translation lemma toward CNF lower bounds.","lead":"This paper proves that certain algebraic proof systems cannot efficiently refute a specially designed unsolvable polynomial equation over small finite fields. The result is a step toward long-sought lower bounds for a prominent propositional proof system, AC^0[p]-Frege, and it also shows how algebraic lower bounds could be converted into theorem-proving lower bounds.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 24's 'construct by induction' hides a load-bearing balanced-word condition; Corollary 23's proof that balance alone implies |w_P|-|w_N|≥-b is false.","rationale":"The reader identified the balanced-word assertion as the weakest assumption, and that is indeed the central gap: every step of the main lower bound is anchored to a word with very specific properties. My read goes slightly further: Corollary 23's proof asserts a general implication from balance to a total-length bound that is false for natural balanced words, so the theorem requires not merely an existence proof but an existence proof of a word satisfying a stronger, unstated condition. The concrete test above would settle whether the construction exists for the relevant parameters. I do not see a reason to reject outright: the surrounding machinery, including Forbes' set-multilinearization over all fields, the full-degree lemmas, and the roABP and translation results, is well supported or plausibly repairable, and a suitable word construction may well exist in the cited prior work. The honest verdict remains conditional: Theorem 24 should be accepted only once the balanced-word construction, with the additional |w_P|-|w_N|≥-k condition and a correct relative-rank exponent, is supplied and verified.","tokens_in":33795,"tokens_out":20224,"duration_ms":218887,"concrete_test":"Enumerate all sign patterns of length d=8,12,16 with entries +αk and -k for α=3/4, k=4, keeping runs of equal sign of length at most 2, and compute the overlap graph, |w_P|-|w_N|, and Δ_G(N_w) under the definitions in Section 3.1. If no pattern has |w_P|-|w_N|≥-k and Δ_G(N_w)≤3, then Lemma 26's required word does not exist. If such patterns do exist, take the word claimed by the induction in Theorem 24, verify the inequality, and recompute Lemma 26's size bound using the actual relative rank instead of the asserted 2^{-k}.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The main finite-field lower bound, Theorem 24, reduces to Lemma 26, which requires a balanced word w over the alphabet {αk,-k} whose set-multilinear coefficient matrix has relative rank at least 2^{-k/2}. The proof of Theorem 24 contains only the sentence 'Construct, by induction, a balanced word w in Z^d over the alphabet {αk,-k}' and gives no construction. This is load-bearing because Corollary 23, which supplies the relative-rank lower bound, asserts that balance plus |w_i|≤b implies |w_P|-|w_N|≥-b. That implication is not justified and is false under the natural contiguous-interval reading of the overlap graph: an alternating word (+αk,-k,+αk,-k,...) is balanced, yet |w_P|-|w_N|=(α-1)k·d/2, which is less than -k for large d. For such words the relative rank is 2^{(|w_P|-|w_N|)/2}, exponentially small, and the combination with Claim 27 in Lemma 26 no longer yields s ≥ 2^{k(λ/256-1)/(2Δ)}. The missing construction must therefore produce a balanced word satisfying the additional total-length condition |w_N|≤|w_P|+k and Δ_G(N_w)≤3; the paper neither proves this nor cites a lemma establishing it.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies lower bounds for fragments of the Ideal Proof System over finite fields. The central results claimed are: (1) a super-polynomial lower bound for constant-depth multilinear IPS_LIN' refutations of a knapsack mod p instance over any field of fixed characteristic p≥5 (Theorem 24); (2) a separation of this system over finite fields from the characteristic-zero system via a symmetric knapsack instance (Theorem 36); (3) exponential lower bounds for roABP-IPS_LIN' over finite fields, in both fixed and arbitrary variable orders (Theorems 43 and 46), together with a limitation of the functional method (Theorem 49); and (4) a translation lemma showing that algebraic-instance lower bounds against bounded-depth IPS over finite fields imply CNF lower bounds and hence AC^0[p]-Frege lower bounds (Theorem 60). The proofs combine the functional lower bound method, Forbes's set-multilinearization over all fields, the BDS24 rank parameters, and the GHT22 framework.","tokens_in":34189,"tokens_out":12211,"duration_ms":126472,"significance":"If the missing pieces are supplied, these are substantial results: they would give the first lower bounds for constant-depth multilinear IPS over any fixed finite field, removing the large-characteristic assumption that underpins earlier work, and the roABP results give simple finite-field analogues of previous large-field bounds. The translation lemma is a clean conceptual contribution that removes the extension axioms from the earlier ST25 translation. The paper proves several key technical lemmas in detail (Lemma 19, Lemma 21, Lemma 33) and correctly exploits Forbes's set-multilinearization result and the BDS24 improved parameters. However, two load-bearing proofs are only sketched or omitted (the balanced-word construction inside Theorem 24, and Lemma 35), and there is an exponent mismatch in Lemma 26, so the manuscript is not yet in a publishable state.","major_comments":[{"comment":"The proof contains the sentence 'Construct, by induction, a balanced word w in Z^d over the alphabet {αk,-k}' but gives neither the construction nor a reference to a lemma establishing it. This is load-bearing: Lemma 26 needs a balanced word with those block lengths, Corollary 23 needs the resulting balance to imply |w_P|-|w_N| ≥ -b, and the scattered partition in the comment after Theorem 24 needs Δ_G(N_w)≤3. Please provide an explicit inductive construction with these parameters, or identify the exact lemma in [GHT22]/[BDS24] and verify that its parameters match d=⌊log n/4⌋ and the stated ranges of α and k.","section":"§3.5, proof of Theorem 24"},{"comment":"The proof of Lemma 35 is omitted ('essentially the same as the proof of Theorem 24 ... and is omitted here'). Since the degree lower bound Lemma 33 is structurally different from the knapsack-mod-p degree argument, and since Theorem 36 is the paper's separation claim, the reduction needs to be written out. At minimum, specify which parts of the Theorem 24 proof carry over verbatim and where Lemma 33 is invoked.","section":"§4.2, Lemma 35"},{"comment":"The inequality chain in the proof gives 2^{-k} ≤ rel-rank(F) ≤ s 2^Δ 2^{-kλ/256}, which yields s ≥ 2^{k(λ/256-1)-Δ}, not the stated s ≥ 2^{k(λ/256-1)/(2Δ)}. The discrepancy should be corrected or explained; as written, the statement of Lemma 26 does not follow from its proof.","section":"§3.5, Lemma 26"},{"comment":"The implication 'w is balanced and |w_i|≤b implies |w_P|-|w_N| ≥ -b' is asserted without proof. It is true under the contiguous-interval interpretation of A(i)_w and B(j)_w (the negative intervals partition [1,|w_N|], so |w_N|>|w_P|+b would leave the last negative interval disjoint from all positive intervals), but the argument should be included, since this inequality is what converts full rank into the relative-rank bound rel-rank ≥ 2^{-b/2}.","section":"§3.4, Corollary 23"}],"minor_comments":[{"comment":"Several lemmas are cited as 'Theorem 18', 'Theorem 19', 'Theorem 20', and 'Theorem 33'; these cross-references should be changed to 'Lemma'.","section":"Throughout §3 and §4"},{"comment":"The word 'acheive' should be 'achieve'.","section":"§5.4"},{"comment":"The phrase 'constant characteristics q' should be 'constant characteristic q'.","section":"§5.2, Corollary 43"},{"comment":"The notation SCNF(C(x)) is used in the proof where Definition 58 writes SCNF(C(x)=0); please make the notation uniform.","section":"§6, Theorem 59"},{"comment":"The quoted set-multilinearization bound poly(s, Θ(d/ln d)^d) would benefit from an explicit statement of the dependence of implicit constants on the field, because Theorem 24 later converts this bound into a concrete n^{Ω(λ/Δ)} lower bound.","section":"§3.5, Lemma 28"}],"recommendation":"major_revision","confidential_remarks":"The central missing construction of the balanced word may be obtainable from [GHT22], but the authors must supply it rather than deferring; the concurrent-work comparison in Section 1.4 is otherwise fair. If the authors provide the construction and the proof of Lemma 35, the paper would be a strong contribution. No citation-pattern concerns beyond the heavy reliance on [GHT22], which is appropriate given the framework."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nHere's my read of arXiv:2506.17210. The headline result — super-polynomial lower bounds for constant-depth multilinear IPS_LIN' over fixed finite fields — is not established as written. The gap is concrete: Corollary 23 asserts that a balanced word with |w_i|≤b satisfies |w_P|-|w_N|≥-b, but an alternating word (+αk,-k,+αk,-k,...) is balanced and has |w_P|-|w_N|=(α-1)k·d/2, which for large d is far below -b. So the relative-rank lower bound 2^{-b/2} does not follow from balance alone. The proof of Theorem 24 then says 'Construct, by induction, a balanced word w∈Z^d over the alphabet {αk,-k}' without giving the construction or the extra condition (essentially |w_N|≤|w_P|+k and Δ_G(N_w)≤3) that would make Corollary 23 true. That is load-bearing: Lemma 26 depends on it.\n\nThat said, there is real substance here. The knapsack-mod-p instance is a new construction, and the degree lemma (Lemma 19) plus the rank argument (Lemma 21) are spelled out carefully. The separation result (Theorem 36) — using the symmetric knapsack of degree 2 and Fermat's little theorem for the upper bound — is a nice idea, though its proof relies on Lemma 35 which is omitted ('essentially the same'). The roABP sections look solid: the hard instance f=∏(1-x_i)-2 is a genuine simplification over HLT24, and the multiples-method proof for the system (f,g,x²-x) is clean. The translation lemma (Section 6) is a genuine contribution: it removes extension axioms from ST25 and gives a direct route from algebraic-instance lower bounds to CNF lower bounds, with the caveat that it does not apply to the paper's own multilinear lower bound, a point the authors acknowledge. There is also a minor exponent discrepancy in Lemma 26, easy to fix.\n\nBottom line: this paper deserves a serious referee, but the referee should demand a proof of the balanced-word construction or a revised statement, and a corrected Corollary 23, before the main theorem is trusted. The roABP and translation results may stand independently. I would cite the translation lemma, and I would bring it to a reading group to discuss the gap.","headline":"Real progress on IPS over finite fields, but the main lower bound currently rests on a false corollary and an unproved balanced-word construction; salvageable, not there yet.","tokens_in":34756,"tokens_out":3707,"would_cite":true,"duration_ms":36584,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","68Q17","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that no polynomial-size constant-depth multilinear Ideal Proof System refutation of a knapsack-mod-p polynomial exists over any fixed finite field of characteristic at least 5.","keywords":["algebraic proof complexity","Ideal Proof System","finite fields","AC0[p]-Frege","constant-depth circuits","knapsack polynomial","set-multilinear circuits","read-once oblivious algebraic branching programs"],"falsifier":"Exhibit a balanced word $w$ over $\\{\\alpha k,-k\\}$ in the parameter range of Theorem 24 whose positive positions cannot be partitioned into fewer than $p$ groups with pairwise disjoint overlaps; that single example would break the construction of $\\mathrm{ks}_{w,p}$ and the rank lower bound. Alternatively, for a fixed such word, compute the minimal size of a product-depth-$\\Delta$ set-multilinear circuit computing the projection $\\Pi_w(1/\\mathrm{ks}_{w,p})$: a polynomial-size circuit in $n$ would disprove Lemma 26.","tokens_in":33577,"feed_emoji":"🧮","tokens_out":14726,"duration_ms":131066,"temperature":0.7,"pith_summary":"This paper proves lower bounds for the Ideal Proof System (IPS), an algebraic proof system in which a refutation is a single algebraic circuit witnessing that 1 lies in the ideal generated by a set of polynomial equations over a field. Earlier IPS lower bounds were proved only over large or characteristic-zero fields, while finite fields are the natural setting for proving lower bounds for propositional proof systems such as $AC^{0}$[p]-Frege. The central result is that a knapsack-mod-p polynomial, a variant of a previously studied subset-sum-style instance, has no polynomial-size constant-depth multilinear IPS_LIN' refutation over any field of characteristic p>=5. The paper also separates this finite-field proof system from the characteristic-zero one, proves exponential lower bounds for read-once algebraic branching program refutations over finite fields, and shows that any lower bound for a non-multilinear constant-depth IPS instance over a finite field would produce a hard CNF formula and hence an $AC^{0}$[p]-Frege lower bound.","feed_headline":"Knapsack mod p refutations need super-polynomial size","feed_subtitle":"Over any fixed prime field, constant-depth multilinear refutations of this instance stay super-polynomial, a step toward AC0[p]-Frege.","key_machinery":"The load-bearing object is the knapsack-mod-p polynomial $\\mathrm{ks}_{w,p}$, together with the relative rank of the coefficient matrix of its reciprocal—that is, the rank divided by the square root of the product of the row and column counts. The word $w$ must be balanced, meaning every index has at least one overlap with an index of the opposite sign, and must admit a scattered partition of its positive indices into fewer than p parts; these conditions make the embedded p-1 powers Boolean functions and let the instance be shifted to an unsatisfiable one. The argument's engine is a rank lower bound (Lemma 21): for the multilinear polynomial $f$ that agrees with $1/\\mathrm{ks}_{w,p}$ on Boolean assignments, the matrix $M_w(f)$ has full rank, by an induction on submonomials of the negative variables. Full rank feeds through the set-multilinearization result [For24] and the improved set-multilinear-to-rank bound [BDS24], and the final size lower bound follows; the carrying identity is the full-degree lemma, which says that a multilinear polynomial inverse of a sum of full-degree Boolean functions minus a constant must itself have full degree.","core_discovery":"The paper's central claim is Theorem 24: for every prime p>=5 and every field F of characteristic p, any product-depth at most $\\Delta$ multilinear $\\mathrm{IPS}_{\\mathrm{LIN}}'$ refutation over F of the knapsack-mod-p instance $\\mathrm{ks}_{w,p}$ has size at least $n^{\\Omega(\\lambda/\\Delta)}$, where $\\Delta \\le \\log\\log\\log n / 4$ and $\\lambda = \\lfloor d^{1/G(\\Delta)} \\rfloor$ with $d = \\lfloor \\log n / 4 \\rfloor$. The hard instance $\\mathrm{ks}_{w,p}$ is built from a balanced integer word $w$ over the two-symbol alphabet $\\{\\alpha k, -k\\}$, with a scattered partition of its positive indices into fewer than p parts, and with each summand raised to the p-1 power so that Fermat's little theorem forces it to be Boolean-valued; a suitable shift $\\beta$ then makes the whole polynomial unsatisfiable over Boolean assignments. The lower-bound argument reduces refutation size to a full-rank statement about the coefficient matrix of the reciprocal function $1/\\mathrm{ks}_{w,p}$ over Boolean assignments, and then rules out small set-multilinear circuits for that projection using a set-multilinearization theorem that works over all fields [For24] together with improved rank-to-size parameters [BDS24]. The paper also proves a separation (Theorem 36): the degree-2 symmetric knapsack $\\mathrm{ks}_{w,e2}$ has polynomial-size constant-depth multilinear $\\mathrm{IPS}_{\\mathrm{LIN}}'$ refutations over any field of characteristic p>=3, but requires super-polynomial size over every characteristic-zero field.","pith_inferences":["Beyond the paper: the unproved balanced-word existence claim, if it fails for some parameters, would not necessarily destroy the whole lower-bound method; a different word family or a different scattered partition might restore the rank argument, and testing the construction explicitly for small d and k is a cheap way to check the route.","Beyond the paper: the translation lemma's removal of extension axioms suggests that any proof system that can internally derive the finite-field axioms and Lagrange interpolation identities can convert algebraic-instance lower bounds into propositional ones; it would be natural to see whether the same internal bit-arithmetic works for polynomial calculus or Nullstellensatz fragments over finite fi","Beyond the paper: the separation instance $\\mathrm{ks}_{w,e2}$ shows that the characteristic of the field can change the complexity of the same algebraic instance; one could look for a family whose required refutation size varies with p, giving a finer map of how IPS strength depends on the ground field.","Beyond the paper: the paper's limitation statement for roABP-IPS means that non-placeholder roABP-IPS lower bounds over finite fields would need a method that is not the functional lower bound method; lower-bound-by-multiples is the natural candidate, but it has not yet been pushed to non-placeholder instances in this setting."],"forward_implications":["For every fixed prime p>=5, the knapsack-mod-p polynomial is a concrete super-polynomial hard instance for constant-depth multilinear $\\mathrm{IPS}_{\\mathrm{LIN}}'$ over all fields of characteristic p.","The same instance also stays hard over characteristic-zero fields, so it supplies new hard instances for the earlier characteristic-zero proof system as well.","The degree-2 symmetric knapsack separates the two settings: it has short constant-depth multilinear refutations over fields of characteristic at least 3, but all such refutations over characteristic-zero fields require super-polynomial size.","Over any fixed finite field, explicit instances force any roABP-$\\mathrm{IPS}_{\\mathrm{LIN}}'$ refutation, in any variable order, to have exponential size; the paper also shows the functional lower bound method alone cannot produce non-placeholder versions of these bounds over finite fields.","If any instance is shown hard for non-multilinear bounded-depth IPS over a finite field, the translation lemma converts it into a hard CNF and hence, by known simulations, into an AC^0[p]-Frege lower bound."],"supporting_citations":[{"why":"Supplies the knapsack instance template and the characteristic-zero lower-bound strategy that the paper adapts to finite fields; the hard instance $\\mathrm{ks}_{w,p}$ is a variant of its $\\mathrm{ks}_w$.","marker":"[GHT22]"},{"why":"Introduces the functional lower bound method and the lower-bound-by-multiples machinery, and provides the full-degree and coefficient-dimension lemmas used throughout.","marker":"[FSTW21]"},{"why":"Gives the set-multilinearization theorem that works over all fields, removing the large-characteristic restriction that blocked the prior approach in finite fields.","marker":"[For24]"},{"why":"Supplies the original constant-depth algebraic circuit lower bounds and the set-multilinearization and rank-reduction framework that the proof builds on.","marker":"[LST21]"},{"why":"Provides improved parameters relating set-multilinear formula size to relative rank of the coefficient matrix, used in the key Lemma 26.","marker":"[BDS24]"},{"why":"Defines the Ideal Proof System and records the simulation of AC^0[p]-Frege by constant-depth IPS over F_p, which the translation lemma targets.","marker":"[GP18]"},{"why":"Provides the extension-axiom translation lemma between circuit equations and CNF encodings that Section 6 refines by removing extension axioms.","marker":"[ST25]"},{"why":"Formalizes the functional lower bound method and states the barrier result that the paper extends in its limitation discussion for roABP-IPS over finite fields.","marker":"[HLT24]"},{"why":"Lucas's theorem underlies the lemma that elementary symmetric sums of a single nonzero base-p digit take few Boolean values, making the separating instance unsatisfiable.","marker":"[Luc78]"}],"fun_headline_variants":["Knapsack mod p needs super-poly constant-depth IPS refutations","Finite-field IPS: knapsack mod p is hard for constant-depth","Super-poly lower bound for IPS over prime fields via knapsack","Multilinear IPS over finite fields fails on knapsack mod p"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The weakest load-bearing premise is a one-sentence assertion in the proof of Theorem 24 that a balanced integer word $w$ over $\\{\\alpha k,-k\\}$ with exactly $d$ positions and with its positive positions partitionable into fewer than $p$ disjoint groups exists; the construction is not given, and if no such word exists for the stated parameters the rank lower bound, and with it the finite-field lower bound, would not go through.","fun_headline_variants_meta":{"raw":{"variants":["Knapsack mod p needs super-poly constant-depth IPS refutations","Finite-field IPS: knapsack mod p is hard for constant-depth","Super-poly lower bound for IPS over prime fields via knapsack","Multilinear IPS over finite fields fails on knapsack mod p"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000416,"raw_usage":{"total_tokens":2331,"prompt_tokens":1314,"completion_tokens":1017,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":930,"completion_tokens_details":{"reasoning_tokens":938}},"tokens_in":930,"tokens_out":1017,"duration_ms":9861,"temperature":1.0,"reasoning_tokens":938,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:12:48.747456+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a balanced word $w$ over $\\{\\alpha k,-k\\}$ in the parameter range of Theorem 24 whose positive positions cannot be partitioned into fewer than $p$ groups with pairwise disjoint overlaps; that single example would break the construction of $\\mathrm{ks}_{w,p}$ and the rank lower bound. Alternatively, for a fixed such word, compute the minimal size of a product-depth-$\\Delta$ set-multilinear circuit computing the projection $\\Pi_w(1/\\mathrm{ks}_{w,p})$: a polynomial-size circuit in $n$ would disprove Lemma 26.","supporting_citations":[],"review_version":1}