{"id":"e4ab58f9-0996-485b-9253-e28d332da606","arxiv_id":"2411.16348","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A new algebraic verification method for and-inverter graphs derives linear relations from local degree-ordered Gröbner bases and checks multiplier specifications with linear rewriting only.","lead":"The paper proves that a linear specification can be checked using only the linear polynomials in a degree-ordered Gröbner basis, then turns this into a circuit verification tool. The method solves all tested ABC-optimized multiplier benchmarks and complements existing algebraic verifiers on hard carry-lookahead designs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Algorithm 4's local extraction is incomplete: a correct AIG with two independent implementations of the same product (v=x∧y, u=p∧q) yields no linear polynomial with leading term v in the local sub-circuit, so Algorithm 2 returns false despite v−u ∈ I; the §4.2 completeness claim is false.","rationale":"The paper's strongest theoretical claim (Theorem 1) is correct: for a full drl-Gröbner basis, linear reduction is complete. The practical algorithm, however, claims completeness by invoking Theorem 1 on sub-ideals generated by local sub-circuits. This invocation is invalid. I constructed a concrete correct AIG where the full ideal contains a linear polynomial with the required leading term, but the Algorithm 4 sub-circuit does not. The gap is not merely a missing proof; it is a false statement about Algorithm 2's behavior. This is the same weak point the reader identified, and the counterexample confirms it. Consequently, the article's central 'soundness and completeness' claim for the implemented technique is false as stated, although the theoretical core remains sound and the tool may still be a useful sound heuristic. The paper must either remove the completeness claim or restrict it to cases where local sufficiency is proven. Given the false central claim, I recommend REJECT as a verdict adjustment.","tokens_in":18587,"tokens_out":28413,"duration_ms":266448,"concrete_test":"Construct the described AIG (with inverter chains on a,b,c,d so that v has distance ≥6 from inputs, and with x,y,p,q each used in both polarities to prevent preprocessing elimination). Run the public MultiLinG artifact with the linear specification S = v − u. If it returns 'incorrect' (or ⊥), the completeness claim in §4.2 is falsified. Independently verify the gap by computing the drl-Gröbner basis of the full circuit and of the Algorithm 4 sub-circuit C_v: the full basis contains a linear polynomial with leading term v (e.g., v−u), while the local basis does not.","verdict_should_be":"REJECT","load_bearing_attack":"Section 4.2 states that if Algorithm 4, after exhausting all distances, finds no linear polynomial with leading term v, then 'the circuit is incorrect. This follows from Theorem 1.' The inference is invalid: Theorem 1 applies to a drl-Gröbner basis of the full circuit ideal, whereas Algorithm 4 computes a drl-Gröbner basis only for the sub-ideal of a local sub-circuit C_{v,d}. Absence of a linear polynomial in that sub-ideal does not imply absence in the full ideal. Concretely, build an AIG with inputs a,b,c,d; gates x=a∧b, y=c∧d, v=x∧y, plus an independent implementation u=p∧q with p=a∧c, q=b∧d. Both v and u equal a·b·c·d, so v−u ∈ I, and the full drl-Gröbner basis contains a linear polynomial with leading term v. But C_v (v, its ancestors, siblings, and one parent iteration) contains v,x,y,a,b,c,d,p,q but not u; its ideal has no linear polynomial with leading term v because no variable equals the product of v's children modulo the local generators. Algorithm 4 returns ∅ and Algorithm 2 returns ⊥, a false negative. Padding distances with inverter chains to ≥6 avoids the implementation's non-linear fallback. Thus the claimed completeness of the practical method is false.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an algebraic verification method for and-inverter graphs (AIGs) based on extracting linear polynomials from degree reverse lexicographic (drl) Gröbner bases. The theoretical part proves Theorem 1: for a drl-Gröbner basis G of an ideal I, a linear polynomial p lies in I if and only if p reduces to zero using only the degree-≤1 polynomials G1 of G. The paper also proves Lemma 3 on linearizing a specification by introducing extension variables. To avoid computing a full drl-Gröbner basis for large circuits, the paper presents Algorithms 2–4, which compute drl-Gröbner bases for local sub-circuits and extract a linear polynomial with a desired leading term; the paper claims that failure to find such a polynomial implies the circuit is incorrect, citing Theorem 1. The method is implemented in the tool MultiLinG and evaluated on multiplier benchmarks, including optimized ABC multipliers and aoki multipliers.","tokens_in":18934,"tokens_out":8988,"duration_ms":84138,"significance":"Theorem 1 and Lemma 3 are elegant and correctly proved; they show that for a complete drl-Gröbner basis the ideal membership of a linear specification can be decided using only linear operations, avoiding monomial blow-up in the reduction phase. The paper makes the theoretical contribution accessible and demonstrates a working implementation on real multiplier benchmarks, including optimized circuits that are hard for previous algebraic tools. However, the practical completeness claim—that the local sub-circuit computation in Algorithm 4 is sufficient to witness all linear relations present in the full ideal—is not justified and is in fact false. The provided counterexample shows that Algorithm 2 can return a 'circuit incorrect' verdict for a correct circuit, so the method as described is not a sound decision procedure for AIG verification. The theoretical result remains valuable, but the practical algorithm needs either a correctness proof under explicit sufficient conditions or a repositioning as a heuristic.","major_comments":[{"comment":"The sentence 'If we still did not find a linear polynomial at this point, we know that the circuit is incorrect. This follows from Theorem 1' is not a valid inference. Theorem 1 applies to a drl-Gröbner basis of the entire ideal I of the full circuit. Algorithm 4 computes a drl-Gröbner basis only for the ideal generated by the gate polynomials of a local sub-circuit C_{v,d}. The absence of a linear polynomial with leading term v in that local ideal does not imply its absence in I. A concrete counterexample is an AIG with inputs a,b,c,d and gates x=a∧b, y=c∧d, v=x∧y, p=a∧c, q=b∧d, u=p∧q. In the Boolean ring, v=u=abcd, so v−u is in the full circuit ideal I. For a variable order with v>u, the reduced drl-Gröbner basis of I contains a linear polynomial with leading term v. Yet the sub-circuit C_v constructed by Algorithm 4 includes v, x, y, a, b, c, d and their parents, but never u, because u is neither an ancestor nor a sibling of v. The ideal generated by the local gate polynomials contains no linear polynomial with leading term v, since v occurs only in the quadratic polynomial v−xy. Algorithm 4 therefore returns ∅ and Algorithm 2 returns ⊥ for a circuit that is correct, so the claimed completeness, and even the soundness of the ⊥ verdict, is false. The authors must either prove a local completeness theorem with explicit sufficient conditions on the sub-circuit, or weaken the claim so that a failed local extraction yields 'unknown' rather than 'incorrect'.","section":"Section 4.2"},{"comment":"The construction of C_{v,d}—including v, its children up to distance d, siblings, and parents of the collected nodes—does not, even as d reaches dist(v), cover all gates that are topologically smaller than v in the whole DAG. The statement in the text that in the worst case the algorithm has computed a full drl-Gröbner basis 'for all gate polynomials that are topologically smaller than v' is inaccurate: only ancestors of v (plus their siblings and parents) are collected, not arbitrary gates that appear earlier in the topological order, such as independent implementations u in the counterexample above. A completeness proof for Algorithm 4 would need to show that any linear polynomial with leading term v in the full ideal is contained in the ideal generated by the polynomials of the constructed sub-circuit; the counterexample shows this is not true in general, so the proof obligation is substantial and cannot be discharged by invoking Theorem 1.","section":"Algorithm 4 (Section 4.2)"},{"comment":"The experimental evaluation does not report cases where the tool fails despite the circuit being correct, i.e., where local extraction misses a linear relation. On the aoki benchmarks MultiLinG solves only 29 of 192 instances, but the paper attributes the failures to time/memory limits and does not analyze whether any of the 163 unsolved instances would be rejected if allowed more resources. Given the false-negative counterexample in Section 4.2, the paper should measure and report the rate of wrong 'incorrect' verdicts on correct circuits, or adjust the algorithm to return 'unknown' when the full drl-Gröbner basis is not computed. Without such data or a correctness guarantee, the presented method cannot be regarded as a formal verification technique, and the empirical claims need to be qualified accordingly.","section":"Section 5.1, Section 5.3"}],"minor_comments":[{"comment":"The phrase 'the division algorithm ... will only select polynomials in G whose leading monomials also have degree 1' is slightly imprecise: a reduction step selects a polynomial whose leading monomial divides the current leading monomial, and for a linear polynomial only degree-1 leading monomials can divide it. Rephrasing this would improve clarity.","section":"Section 3, proof of Theorem 1"},{"comment":"The initial distance d=3 and the depth-dependent fall-back to non-linear rewriting for distances below six are heuristic parameters that are not part of the completeness argument. The paper should explicitly state that these choices are heuristics and do not affect the theoretical guarantees only if the local-completeness claim is abandoned or proven under different hypotheses.","section":"Section 4.2, Algorithm 4"},{"comment":"The fall-back to non-linear rewriting when the distance of a node to the primary inputs is below six is a further heuristic whose interaction with the claimed completeness is not discussed. If this fall-back is used, the reduction is no longer performed only by linear polynomials, so even the conditional completeness obtained from a full drl-Gröbner basis would not apply to the resulting reduction path.","section":"Section 5.1"},{"comment":"The four gate-polynomial forms are all of degree two, but the observation that the polynomial encoding forms a Gröbner basis with respect to the lexicographic order relies on the UMLT property and on the Boolean input polynomials; citing the precise result (e.g., the relevant theorem from the authors' earlier work) at this point would help the reader.","section":"Section 2.2, Definition 10"}],"recommendation":"major_revision","confidential_remarks":"The theoretical contribution (Theorem 1 and Lemma 3) is sound and could be the basis of a solid paper. The practical algorithm, however, is not a decision procedure as claimed: the local extraction can miss linear relations present in the full ideal, leading to false 'incorrect' verdicts on correct circuits. The paper should be revised either by proving local completeness under explicit conditions, or by presenting the local method as a sound-but-incomplete heuristic (returning 'unknown' when extraction fails) and adjusting all claims, the title, and the abstract accordingly. The experimental evaluation should also report the rate of wrong rejections on correct benchmarks."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe paper is worth a read for the theory, but be careful about the practical claims. The main theoretical result, Theorem 1, is correct and new in this context: if the specification is linear, then membership in an ideal can be decided using only the linear elements of a degree-reverse-lex Grobner basis. Lemma 3 (linearization) also holds. These are solid contributions.\n\nThe practical algorithm, though, is not complete in the way the paper claims. Algorithm 4 computes a Grobner basis for a local sub-circuit C_{v,d}, but Theorem 1 only applies to a Grobner basis of the full ideal. There is no proof that the local sub-basis contains the required linear polynomial whenever it exists globally. In fact, it can fail. Take an AIG with independent implementations of the same product: v = x∧y and u = p∧q where p = a∧c, q = b∧d, and x = a∧b, y = c∧d. Both v and u equal abcd, so v−u ∈ I and a full drl-Grobner basis contains a linear polynomial with leading term v. But if you build C_{v,d} around v, it includes x,y,a,b,c,d,p,q but not u, so the local ideal has no linear polynomial with leading term v. Algorithm 4 returns ∅ and Algorithm 2 returns ⊥, a false negative. The paper's statement that 'if we still did not find a linear polynomial at this point, we know that the circuit is incorrect. This follows from Theorem 1' is simply wrong.\n\nWhat the paper does well: the experiments on 15 optimized ABC multipliers are all solved, and it handles 13 aoki benchmarks that DPOO misses. The preprocessing heuristics are sensible, and the artifact is public. But the coverage on the structured aoki set is low (29 of 192), and two thresholds are empirically tuned.\n\nBottom line: the theory is sound and the local extraction idea is a useful heuristic, but the completeness claim is load-bearing and false. The authors should either prove a restricted form of completeness or explicitly present the method as an incomplete simplification. A serious referee will catch this, and the paper would need major revision before acceptance. Still, the theoretical part is worth engaging with and the experiments are informative.\n\nI'd send it to review, but the authors need to fix the overclaim.","headline":"Sound theorem, but the practical completeness claim is false.","tokens_in":19436,"tokens_out":3282,"would_cite":true,"duration_ms":28486,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["13P10","68W30"],"pacs":[],"model":"deepseek-v4-flash","headline":"For a linearized specification, a degree-ordered Gröbner basis needs only its linear polynomials to decide correctness of an and-inverter graph.","keywords":["Algebraic Reasoning","Gröbner Basis","Hardware Verification","And-Inverter Graphs","Multiplier Verification","Degree Reverse Lexicographic Order","Linear Polynomials","Ideal Membership"],"falsifier":"Run the local extraction loop on a known-correct AIG, letting the fragment grow until it contains every gate upstream of the target gate; if at that point no linear polynomial with the needed leading term has appeared, while the full degree-first Gröbner basis of the same circuit does contain one, the practical completeness claim is false. Constructing such an instance, for example a correct multiplier where a linear relation depends on a distant part of the circuit, would settle the question directly.","tokens_in":18384,"feed_emoji":"🧮","tokens_out":8477,"duration_ms":86483,"temperature":0.7,"pith_summary":"This paper tries to establish that, once a circuit's specification is made linear, verifying an and-inverter graph can be done solely by taking constant-coefficient combinations of the linear polynomials inside a degree-first Gröbner basis; every higher-degree basis element can be ignored. The point is to sidestep the monomial blow-up that comes from rewriting a specification against a lexicographic basis. The authors prove the soundness and completeness of this reduction as Theorem 1, then turn it into a practical algorithm by computing small Gröbner bases on local sub-circuits and extracting one linear relation at a time. Their implementation verifies all tested optimized 32-, 64-, and 128-bit multiplier benchmarks and solves instances that a leading comparison tool misses, so the method appears to complement existing algebraic verification approaches.","feed_headline":"Only linear polynomials are needed to verify a multiplier circuit","feed_subtitle":"A degree-first ordering keeps every reduction step linear, so monomial blow-up moves from rewriting to basis generation.","key_machinery":"The load-bearing object is the set $G_1$ of linear polynomials inside a degree reverse lexicographic Gröbner basis, where monomials are ordered by total degree first and ties are broken from the right. Under this order, the leading monomial of any linear polynomial has degree one and its tail also has degree at most one, so reducing a linear polynomial by $G$ stays inside degree one and can only use $G_1$. The companion mechanism is linearization: fresh variables $t_i$ stand for non-linear monomials $\\sigma_i$ of the specification, with extension polynomials $t_i - \\sigma_i$ added to the gate polynomials, so the membership test becomes a linear one. Finally, the local-extraction loop replaces the infeasible full basis computation with repeated small drl computations on sub-circuits defined by the gate whose leading term is currently needed.","core_discovery":"The central claim is Theorem 1: if $p \\in K[X]$ is linear, $I$ is an ideal, $G$ is a Gröbner basis of $I$ for the degree reverse lexicographic order $\\prec_{\\mathrm{drl}}$, and $G_1 = \\{g \\in G \\mid \\deg(g) \\le 1\\}$, then $p \\in I$ if and only if $p \\to_{G_1} 0$, and in that case $p$ is a $K$-linear combination of polynomials in $G_1$. The proof observes that reducing a linear polynomial by a drl-ordered basis never needs to touch a leading monomial of degree above one, so all nonlinear basis elements are irrelevant to the membership test. Because a real specification is usually nonlinear, the paper first linearizes it by replacing each non-linear monomial $\\sigma_i$ with a fresh extension variable $t_i$ and adding the polynomial $t_i - \\sigma_i$ (Lemma 3). The practical algorithm then avoids computing the full drl basis: for each needed leading term $v$, it builds a small sub-circuit around the gate $v$ — its children up to a growing distance, its siblings, and collected parents — computes a drl Gröbner basis for that fragment, and extracts a linear polynomial with leading term $v$. If no such polynomial appears as the fragment grows, the circuit is declared incorrect.","pith_inferences":["The proof of Theorem 1 generalizes to any fixed-degree specification: if $\\deg(p)=d$, reduction under drl only ever consults basis elements of degree at most $d$, so the analogous restricted set $G_{\\le d}$ would decide membership; the paper only states the linear case, but the same argument carries through.","The practical completeness claim rests on a local-to-global sufficiency that the paper asserts rather than proves: the fragment $C_{v,d}$ must witness every linear relation the full ideal implies, so a fallback that escalates to a larger region when local extraction saturates without finding the relation would make the tool's 'incorrect' answer safer.","Since the linear relations produced are cheap, they could be fed back into the lexicographic encoding as rewrite rules, effectively combining the degree-based extraction with the substitution-style reduction used in earlier algebraic verifiers.","The technique should transfer to other acyclic arithmetic circuits whose specifications become linear after extension variables, including adders and datapath components, whenever the local fragment assumption holds."],"forward_implications":["With the theorem, a linearized specification can be verified by linear algebra alone: no intermediate reduction result ever exceeds degree one, so monomial blow-up in the specification rewrite disappears.","Only the linear tail of the drl Gröbner basis needs to be kept for the final membership decision; nonlinear elements matter only insofar as they help generate those linear polynomials.","The local-extraction strategy makes this usable on optimized, synthesis-scripted multipliers, where structure-dependent tools time out because the classical component boundaries are blurred.","The approach complements existing verifiers: it solves instances with carry-lookahead adder chains that cause blow-up in other algebraic tools, while remaining competitive on standard ABC benchmarks.","For an incorrect circuit, failure to find a linear polynomial with the required leading term, once the local fragment covers all topologically smaller gates, certifies that the specification is not implied."],"supporting_citations":[{"why":"Provides the Gröbner basis definitions, the division algorithm, and product criterion used in the proof of Theorem 1.","marker":"[8]"},{"why":"Establishes the lexicographic gate-polynomial encoding as a Gröbner basis and the local-rewriting lemma used in Algorithm 4.","marker":"[19]"},{"why":"Supplies the foundational notion of Gröbner basis and the S-polynomial criterion behind the black-box basis computations.","marker":"[5]"},{"why":"Is the Gröbner basis library used to compute the local drl bases in the implementation.","marker":"[3]"},{"why":"Serves as the algebraic verification baseline whose polynomial arithmetic engine the implementation reuses.","marker":"[18]"},{"why":"Provides the linearization idea of replacing non-linear monomials with fresh variables, adapted in Lemma 3.","marker":"[25]"},{"why":"Is the comparison tool that the experiments show complements the proposed approach on optimized multipliers.","marker":"[21]"}],"fun_headline_variants":["Gröbner basis trick: only linear bits verify circuits","Linear-only Gröbner test verifies multiplier circuits","Degree-first ordering keeps circuit proof linear","Fragmented basis yields linear proof for circuits","Rewriting basis, not spec, keeps verification linear"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The practical algorithm assumes that the small circuit fragment built around each gate is large enough to witness any linear polynomial implied by the whole circuit; if that local-to-global step fails, a correct circuit could be reported as incorrect.","fun_headline_variants_meta":{"raw":{"variants":["Gröbner basis trick: only linear bits verify circuits","Linear-only Gröbner test verifies multiplier circuits","Degree-first ordering keeps circuit proof linear","Fragmented basis yields linear proof for circuits","Rewriting basis, not spec, keeps verification linear"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000578,"raw_usage":{"total_tokens":2752,"prompt_tokens":998,"completion_tokens":1754,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":614,"completion_tokens_details":{"reasoning_tokens":1680}},"tokens_in":614,"tokens_out":1754,"duration_ms":26487,"temperature":1.0,"reasoning_tokens":1680,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:13:31.115687+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the local extraction loop on a known-correct AIG, letting the fragment grow until it contains every gate upstream of the target gate; if at that point no linear polynomial with the needed leading term has appeared, while the full degree-first Gröbner basis of the same circuit does contain one, the practical completeness claim is false. Constructing such an instance, for example a correct multiplier where a linear relation depends on a distant part of the circuit, would settle the question directly.","supporting_citations":[{"cited_title":"Springer-Verlag New York (1997)","cited_arxiv_id":null,"evidence_quote":"Provides the Gröbner basis definitions, the division algorithm, and product criterion used in the proof of Theorem 1."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the foundational notion of Gröbner basis and the S-polynomial criterion behind the black-box basis computations."},{"cited_title":"In: FMCAD 2019","cited_arxiv_id":null,"evidence_quote":"Serves as the algebraic verification baseline whose polynomial arithmetic engine the implementation reuses."},{"cited_title":"In: FMCAD 2020","cited_arxiv_id":null,"evidence_quote":"Provides the linearization idea of replacing non-linear monomials with fresh variables, adapted in Lemma 3."},{"cited_title":"In: FMCAD 2024","cited_arxiv_id":null,"evidence_quote":"Is the comparison tool that the experiments show complements the proposed approach on optimized multipliers."}],"review_version":1}