{"id":"12cdb64c-5f56-4cec-be16-118c1e862949","arxiv_id":"2505.14998","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A refutation calculus for multimodular integer constraints using lifting and lowering between subsystems, implemented in cvc5, outperforms state-of-the-art solvers on cryptographic verification benchmarks.","lead":"This paper presents a new SMT-solving method that splits integer constraints by modulus and shares lemmas between the parts, which helps verify cryptographic implementations that mix arithmetic over different moduli. The method is implemented in the cvc5 solver and beats existing solvers on benchmarks drawn from Montgomery arithmetic and zero-knowledge proofs.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The reported 'ours' solver's unsat answers on composite-modulus benchmarks depend on Singular's strong Gröbner bases in Z_n[X]; a wrong ideal-membership verdict would make satisfiable instances refute falsely.","rationale":"The reader's weakest assumption correctly identifies Singular's strong-Gröbner-basis computation over Z_n[X] as the main load-bearing assumption for the practical claim. The paper's own theoretical results are well-supported: the derivation rules are individually sound, the soundness proof is a standard local-soundness argument, and termination is argued via a Noetherian ideal-chain measure. The approximate ILP encoding flagged in the reader's rationale is a genuine gap, but it is not the configuration used for Table 2's 'ours' row: that row corresponds to the Weighted GB configuration in Table 3, not the linear-constraint configuration. Thus the ILP concern affects a secondary ablation strategy, not the headline comparison. In contrast, every benchmark solved by the Weighted GB configuration depends on ideal-membership decisions made by Singular, and composite-modulus ideal membership is exactly the setting where strong Gröbner bases require more than ordinary field-based algorithms. The paper provides no artifact-level audit or independent re-check of those decisions. A targeted re-verification of unique solves is the most direct way to test whether this concern actually lands. Since the concern is an unverified implementation risk rather than a demonstrated contradiction, the existing CONDITIONAL verdict remains appropriate.","tokens_in":25415,"tokens_out":24180,"duration_ms":236438,"concrete_test":"Extract the 76 benchmarks that 'ours' solves but no other solver in Table 2 solves, and independently verify each such benchmark's unsatisfiability using a complete decision procedure for the finite domain (e.g., bit-blasting the corresponding QF_BV encoding with a substantially larger timeout, or an exact finite-domain search for the relevant bit-widths). If every unique solve is confirmed unsatisfiable, the Singular GB concern does not materialize and the empirical claim stands; if any unique solve is satisfiable, a false unsat occurred and Table 2's comparison is invalidated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The calculus itself, including Theorem 1, appears sound: the derivation rules are locally sound and the proofs in Appendices A-B support the theoretical claim. The load-bearing risk is in the implementation of the reported 'ours' solver, which uses the Weighted GB lifting strategy (Section 5.4) and Singular v4.4.0 for all algebraic components (Section 6). UnsatOne, UnsatDiseq, and LiftEq all require ideal-membership tests in Z_n[X]. Over composite moduli, which occur in the f/b(s) and f/b(m) families with moduli of the form 2^b and account for 67 of the 255 solves in Table 2, strong Gröbner bases are delicate because coefficients are not invertible and standard Gröbner-basis algorithms are usually defined over fields. The paper gives no independent evidence that Singular computes correct strong reduced Gröbner bases in Z_n[X] for composite n, and no verification that the resulting ideal-membership decisions are correct. If a membership test reports a false positive, the procedure can conclude unsat for a satisfiable system, directly invalidating the empirical central claim. This is an implementation-soundness risk rather than a flaw in the underlying calculus.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces QF_MIA, a fragment of non-linear integer arithmetic with explicit modular equalities and disequalities, and presents a refutation procedure for multimodular systems. The procedure partitions constraints by modulus, maintains variable bounds, and exchanges information across subsystems through lifting and lowering lemmas (Lemmas 1–4). The resulting calculus is proved sound (Theorem 1) and terminating (Theorem 2). Two lemma-generation strategies are described: a weighted Gröbner basis method (Section 5.4, Theorem 3) and an integer linear programming method (Section 5.5, Theorem 4). The procedure is implemented in cvc5 using Singular for Gröbner bases and GLPK for the integer linear constraints, and is evaluated on cryptographic benchmarks from Montgomery arithmetic and zero-knowledge proof implementations. The best configuration reports 255 total unsat solves, compared with 190 for z3 and 166 for cvc5 on the same benchmarks, with 76 unique solves.","tokens_in":25627,"tokens_out":19863,"duration_ms":191484,"significance":"If the empirical claims hold, the paper delivers a genuinely useful new solver architecture for a class of constraints that is important in cryptographic verification and that existing SMT solvers handle poorly. The theoretical core is attractive: the lifting/lowering lemmas are simple yet effective, the calculus is locally sound, the termination measure is natural, and the paper is honest about the incompleteness of its lifting strategies. The use of external benchmark families and a fixed formula for the monomial-order weights avoids circularity in the experimental evaluation. The main reasons for not recommending acceptance now are not in the calculus itself but in the soundness evidence for the implemented system: the reliance on composite-modulus Gröbner bases from Singular and the use of an approximate ILP encoding whose soundness is not established.","major_comments":[{"comment":"The main empirical result depends on Singular computing strong Gröbner bases in Z_n[X] for composite n. The f/b(s) and f/b(m) families use moduli of the form 2^b and account for 67 of the 255 solves in Table 2. The rules UnsatOne, UnsatDiseq, and LiftEq all require exact ideal-membership or ideal-generation checks, so a false positive in Singular's Gröbner basis computation would make the solver return unsat for a satisfiable instance. The paper gives no independent evidence that Singular computes correct strong reduced Gröbner bases over Z_n[X] for composite n, nor any validation strategy. Please add a concrete validation, for example by checking the implementation on composite-modulus instances with independently known satisfiability status, or by restricting the empirical claims to prime moduli, or by providing an independent verification of the ideal-membership results.","section":"Section 6 and Table 2"},{"comment":"The ILP-based lifting used in the experiments is an approximate version in which constants are scaled by slog2, and Appendix E states that all experimental results use this relaxation. Theorem 4 proves the soundness of the exact encoding only. The paper does not state whether the candidate coefficient vectors produced by the approximate encoding are subsequently checked against the exact LiftEq premises before being added to R_∞. If they are not checked, the Lin. Constraints and hybrid rows of Table 3 may include unsound solves. Please specify the filtering mechanism, or prove that the approximation preserves the soundness condition, or remove the unsound configuration from the experimental claims. This does not affect Table 2, whose best configuration uses the weighted Gröbner basis only, but it affects the secondary claim that the ILP method is a viable supplementary lifting strategy.","section":"Section 6 / Appendix E / Table 3"},{"comment":"The weighted monomial order uses weights log(max(|B(x_i)_1|, |B(x_i)_2|) + ε/4). If any variable has both bounds equal to 0, and ε is chosen in the usual small range (0 < ε < 4), the assigned weight is negative. A monomial order is required to satisfy 1 ≤ m for every monomial, and negative weights can violate this condition, so the object computed with Eq. (2) may not be a Gröbner basis in the sense used by the calculus. Since Theorem 3 and the weighted-GB configuration depend on Eq. (2) defining a monomial order, please state the permitted range of ε and prove that the resulting weights are nonnegative, or modify the formula to guarantee that property.","section":"Section 5.4, Eq. (2)"}],"minor_comments":[{"comment":"The ConstrBds rule divides by a but does not state a ≠ 0; the premise should include this condition, and the written premise contains the typo B(x_i)_w instead of a defined bound component.","section":"Figure 4, ConstrBds"},{"comment":"The paper says CalcBds returns the maximum and minimum possible values of an expression, but the rules only require an over-approximation from interval arithmetic; the wording should make clear that CalcBds is an interval-arithmetic over-approximation, since the soundness arguments rely on this over-approximation property.","section":"Section 3.2 / Section 5.1"},{"comment":"The termination proof calls the lexicographic order on ideals 'total', but the ideal-order component is defined by strict inclusion and is only a partial order; this does not affect the well-foundedness argument, but the text should say 'well-founded partial order' rather than 'total well-founded order'.","section":"Appendix B, termination proof"},{"comment":"The indices in the definition of Φ are inconsistent: the sum over monomials is written with index i while i already indexes the expressions e_i; the summation over monomials should use a distinct index, and the number of monomials is t, not k.","section":"Section 5.5"},{"comment":"The proof of Lemma 5 has several transcription errors, including a stray '5' after a displayed equation and an omitted closing parenthesis in the definition of w(JmK); these should be corrected for readability.","section":"Appendix C, Lemma 5 proof"},{"comment":"The text says the weighted Gröbner basis method is 'complete' under the condition in Theorem 3, but the condition is essentially that every generator passing the leading-monomial bound test is liftable; stating this as a 'completeness guarantee' is potentially misleading and should be phrased as a conditional completeness result.","section":"Section 5.4"}],"recommendation":"major_revision","confidential_remarks":"This is a strong and relevant submission for CAV. The calculus appears sound and the benchmark set is well chosen. My recommendation is driven by the lack of validation for the composite-modulus Gröbner basis computations in Singular and by the unproven approximate ILP encoding used in some experiments. If the authors can add artifact-level validation for composite moduli and either prove or explicitly filter the approximate ILP candidates, I would be comfortable with acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my read. The paper delivers a genuinely new refutation procedure for multimodular integer systems, and the core calculus looks sound. The lifting/lowering lemmas, the weighted Groebner basis ordering aimed at near-zero polynomials, and the ILP-based lemma search are real additions, not repackaged known techniques. The benchmarks come from actual cryptographic code (Montgomery, ZKP foreign-field), and the comparison to existing solvers is handled honestly, including the weak spot on f/b(m), which the authors own up to.\n\nThe soft spots are both in the implementation, not the calculus. First, Section 6 says all reported results use an approximate version of the ILP encoding, where constants are scaled with signed log. Theorem 4 is only for the exact encoding. There is no proof that the approximation preserves the liftability conditions from Lemma 1. If the approximate solver returns a candidate e' that does not actually satisfy CalcBds(B,e') ⊆ [1-n,n-1], then applying LiftEq on that e' would be unsound. This is a real gap and needs to be addressed before the empirical claims are taken at face value. Second, the procedure leans on Singular to produce strong reduced Groebner bases in Z_n[X] for composite n. That is a delicate computation and the paper gives no independent check. I see this as a risk worth documenting, not a proven flaw: an incomplete basis would tend to miss refutations rather than produce false ones, but the authors should say what Singular actually guarantees and what the timeout-on-membership fallback does to soundness.\n\nMinor: the 'outperforms on 5 of 7 categories' headline is fine, but the f/b(m) numbers are bad enough that the summary should mention it in the same breath.\n\nThe math of the calculus itself — soundness and termination — checks out in the appendices as far as I can see. I'd send this to review. The ILP approximation and the Singular assumptions need clarification, but the core idea deserves referee time.","headline":"A genuinely new lifting/lowering refutation calculus for multimodular integer systems, with a sound core, but the reported implementation leans on an unproven ILP approximation and unexamined Singular assumptions over composite moduli.","tokens_in":26169,"tokens_out":3704,"would_cite":true,"duration_ms":33336,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","13P10","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes a sound and terminating refutation calculus for systems of integer polynomial equalities and disequalities modulo different constants, and shows experimentally that its implementation outperforms existing solvers on…","keywords":["SMT solving","multimodular arithmetic","Gröbner bases","lifting and lowering","refutation calculus","cryptographic verification","integer arithmetic","unsatisfiability"],"falsifier":"Force the algebra engine to time out on a known-satisfiable system with composite modulus 6, where the relevant equation follows only after a polynomial combination that the timeout misses, and check whether the procedure ever reports unsat; a wrong result would show the fallback set-inclusion test is unsound in practice.","tokens_in":25238,"feed_emoji":"🧩","tokens_out":9568,"duration_ms":88316,"temperature":0.7,"pith_summary":"Systems that mix constraints modulo different constants, such as arithmetic modulo a power of two in an implementation and modulo a large prime in a specification, are hard for existing SMT solvers. This paper proposes a refutation procedure that splits such a system into one subsystem per modulus, uses algebraic ideal-membership tests inside each subsystem, and shares lemmas across subsystems by lifting constraints to integer arithmetic and lowering them back into other moduli. The paper proves the calculus sound and terminating and gives a partial completeness theorem for its weighted Gröbner basis method of finding liftable equalities. On unsatisfiable benchmarks from Montgomery arithmetic and zero-knowledge proof implementations, the procedure solves more instances than existing QF_NIA, QF_BV, and QF_FF solvers, including 76 instances that no other tested solver solves.","feed_headline":"New refutation procedure beats existing solvers on mixed-modulus math","feed_subtitle":"Splits constraints by modulus and shares lemmas via lifting and lowering: 255 of 336 crypto benchmarks proven unsat.","key_machinery":"The object that carries the argument is the refutation calculus over configurations (B, R≈∞, R≠∞, R≈n1, R≠n1, . . .), where each R≈n holds expressions representing equalities modulo n and R≠n holds disequalities. The central mechanism is the lifting/lowering pair: Lemma 1 lifts e mod n ≈ 0 to an integer equality e ≈ 0 when the polynomial e lies in the modulus-n ideal and the interval-arithmetic bound CalcBds(B, e) lies in [1 − n, n − 1]; Lemma 3 lowers any entailed integer equality into every modulus; Lemma 4 lowers disequalities under the same range condition. To find polynomials worth lifting, the paper uses a weighted reverse-lexicographic monomial order with weights log(max(|B(xi)1|, |B(xi)2|) + ε), which makes monomials with small ranges small in the order, biasing Gröbner basis generators toward near-zero, liftable polynomials. A complementary method encodes the search for a liftable linear combination of existing expressions as an integer linear constraint system. The lowering rules use the signed-remainder rewrite simpn(e), which replaces every integer constant in e by its remainder modulo n and thereby simplifies equations inside each modulus-n subsystem.","core_discovery":"The central claim is that multimodular unsatisfiability can be refuted by per-modulus algebra plus lemma exchange rather than by monolithic nonlinear integer reasoning. The calculus keeps, for each modulus n and for the integers themselves, a set of equalities, a set of disequalities, and a variable bound map; it refutes when a modulus-n ideal contains 1, when an active disequality lies in that ideal, or when bounds clash; and it grows the subsystems by lifting, adding e = 0 to the integer subsystem when e mod n = 0 is entailed and the range of e lies within [1 − n, n − 1], and by lowering, adding the simplified remainder of e to a modulus-n subsystem when e = 0 is entailed. The paper proves local soundness of every rule and hence Theorem 1: a closed derivation tree with root C certifies that C is unsatisfiable in integer arithmetic. It also proves termination on finite configurations with bounded variables, and Theorem 3, a partial completeness result: with a weighted reverse-lexicographic Gröbner basis, if every generator whose leading monomial has small range corresponds to a liftable equality, then all liftable equalities in the ideal are found. On the released benchmarks, the weighted-Gröbner configuration solves 255 of 336 unsatisfiable instances, ahead of the next-best solver's 190, and wins 5 of the 7 benchmark categories.","pith_inferences":["Beyond the paper, the same lifting calculus should transfer to satisfiability-oriented search: since lifting adds integer equations only when equisatisfiability is preserved, a model-building version could use the lifted integer system to restrict the search space, a direction the paper explicitly leaves open.","The failure profile on f/b(m), which accounts for 34 of the 81 unsolved instances, suggests a concrete experiment: add the unweighted Gröbner basis to the weighted candidate pool for that family, since the paper's own ablation shows the unweighted method lifts more equalities there.","The bound-dependent weight scheme is a general recipe for any ideal-membership procedure with interval information: it biases basis computation toward low-range witnesses and could be reused outside modular reasoning, for instance in polynomial reasoning over the reals.","A practical engineering consequence, not drawn by the paper, is that the 30-second Gröbner-basis timeout is the most likely place for the practical procedure to lose either completeness or soundness; replacing the black-box engine with an incremental basis computation could remove that fallback entirely."],"forward_implications":["A closed derivation tree in this calculus is a checkable certificate of unsatisfiability in integer arithmetic, independent of the engine that found it.","Weighted Gröbner lifting is complete whenever every generator with a small-range leading monomial lifts; in that case the method provably discovers all liftable equalities hidden in the modulus-n ideal.","The integer-linear-constraint encoding for liftable linear combinations is exact in theory, so the search for liftable equalities of that form is a finite integer programming problem.","The reported experiments support using this procedure as a dedicated theory solver for the multimodular fragment rather than encoding modular constraints with auxiliary variables into general nonlinear integer arithmetic.","On the f/f(s), f/f(m), f/b(s), and b/f(m) families, the procedure solves substantially more instances than the best QF_NIA, QF_BV, and QF_FF baselines, including all determinism benchmarks in f/f(s) and b/f(m)."],"supporting_citations":[{"why":"Defines Gröbner bases as a complete ideal-membership test, the algebraic backbone of the unsat rules.","marker":"[13]"},{"why":"Supplies the ideal-theoretic result that 1 in an ideal means no common zero, used by the UnsatOne rule.","marker":"[22]"},{"why":"Provides the computer-algebra engine that computes strong Gröbner bases over the polynomial rings used by the procedure.","marker":"[23]"},{"why":"Supplies interval arithmetic for CalcBds, the range computation behind every liftability and lowerability guard.","marker":"[45]"},{"why":"Solves the integer linear constraint system of the second lifting algorithm.","marker":"[52]"},{"why":"Gives the Montgomery arithmetic specification that generates the f/b benchmark families.","marker":"[56]"},{"why":"Provides the bit-vector-to-prime-field benchmark family checking RSA signatures.","marker":"[49]"},{"why":"Supplies the multi-limb foreign-field benchmark family for the f/f(m) category.","marker":"[64]"},{"why":"Defines the finite-field theory whose Gröbner-basis solver is the closest prior approach and a baseline.","marker":"[65]"},{"why":"Contributes the split-Gröbner-basis solver and determinism benchmarks used as baselines.","marker":"[66]"}],"fun_headline_variants":["Modular splitting and lifting refute 255 crypto benchmarks","Weighted Gröbner bases beat SOTA on mixed-modulus SMT","Lift, lower, share lemmas: new edge for multimodular proofs","Per-modulus algebra wins on crypto verification benchmarks","From modulus to unsat: 255/336 proven by lemma exchange"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the algebra engine is always correct about which polynomial equations follow from the others, for every modulus, prime or composite; if the engine times out and falls back to a weaker check, the refutation may be wrong.","fun_headline_variants_meta":{"raw":{"variants":["Modular splitting and lifting refute 255 crypto benchmarks","Weighted Gröbner bases beat SOTA on mixed-modulus SMT","Lift, lower, share lemmas: new edge for multimodular proofs","Per-modulus algebra wins on crypto verification benchmarks","From modulus to unsat: 255/336 proven by lemma exchange"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000472,"raw_usage":{"total_tokens":2338,"prompt_tokens":931,"completion_tokens":1407,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":547,"completion_tokens_details":{"reasoning_tokens":1312}},"tokens_in":547,"tokens_out":1407,"duration_ms":15718,"temperature":1.0,"reasoning_tokens":1312,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T15:25:18.116113+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Force the algebra engine to time out on a known-satisfiable system with composite modulus 6, where the relevant equation follows only after a polynomial combination that the timeout misses, and check whether the procedure ever reports unsat; a wrong result would show the fallback set-inclusion test is unsound in practice.","supporting_citations":[{"cited_title":"Buchberger","cited_arxiv_id":null,"evidence_quote":"Defines Gröbner bases as a complete ideal-membership test, the algebraic backbone of the unsat rules."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the ideal-theoretic result that 1 in an ideal means no common zero, used by the UnsatOne rule."},{"cited_title":"Decker, G.-M","cited_arxiv_id":null,"evidence_quote":"Provides the computer-algebra engine that computes strong Gröbner bases over the polynomial rings used by the procedure."},{"cited_title":"Hickey, Q","cited_arxiv_id":null,"evidence_quote":"Supplies interval arithmetic for CalcBds, the range computation behind every liftability and lowerability guard."},{"cited_title":"Liang, A","cited_arxiv_id":null,"evidence_quote":"Solves the integer linear constraint system of the second lifting algorithm."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the Montgomery arithmetic specification that generates the f/b benchmark families."},{"cited_title":"Kosba, C","cited_arxiv_id":null,"evidence_quote":"Provides the bit-vector-to-prime-field benchmark family checking RSA signatures."},{"cited_title":"Niemetz, M","cited_arxiv_id":null,"evidence_quote":"Supplies the multi-limb foreign-field benchmark family for the f/f(m) category."},{"cited_title":"Ozdemir, G","cited_arxiv_id":null,"evidence_quote":"Defines the finite-field theory whose Gröbner-basis solver is the closest prior approach and a baseline."},{"cited_title":"Ozdemir, S","cited_arxiv_id":null,"evidence_quote":"Contributes the split-Gröbner-basis solver and determinism benchmarks used as baselines."}],"review_version":1}