{"id":"4c440ee4-53e1-423e-ad31-fdc23d6fc328","arxiv_id":"2504.12465","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Under an unproved irreducibility heuristic, the outputs of the proposed generator-sampling algorithm are Zariski dense in the space of generator sets of a fixed ideal, supplying a conditional geometric notion of dataset generality for transformer training.","lead":"This paper gives a conditional proof that a transformer training dataset for Gröbner basis computation is Zariski dense, meaning generic rather than special, under an unproved irreducibility heuristic. It is worth reading because it attempts to put a rigorous geometric foundation under the empirical idea that training data should be diverse or representative for symbolic mathematics.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2.3 covers Algorithm 2's output set, not KIK+24's restricted Bruhat-like output set; the paper never proves the latter is Zariski dense, so the abstract's claim about the previous dataset method is unsupported.","rationale":"The reader's weakest_assumption names Heuristic 2.2 as the main gap, and separately notes that the KIK+24 application assumes density of its Bruhat-like output set without proof. I agree that Heuristic 2.2 is unresolved, but I regard the Bruhat-like bridge as the more load-bearing issue for the central advertised claim. The theorem's conditional content for Algorithm 2 is plausible and clearly stated, so the reader's CONDITIONAL verdict remains appropriate; however, the abstract and introduction currently attribute to [KIK+24] a density result that the paper does not prove. A revision should either prove density for the restricted Bruhat-like family or explicitly restrict the geometric-generality claim to Algorithm 2. Because the existing CONDITIONAL verdict already captures the need for such revision, I do not move the verdict; I only shift the emphasis from the heuristic to the application gap.","tokens_in":16375,"tokens_out":21653,"duration_ms":228872,"concrete_test":"For K=Q, r=n=2, m=4, D=2, fix a generic shape-position G. In Macaulay2, compute the Zariski closure inside F~≤2 of the image of the KIK+24 Bruhat-like map (U1, U2, S) -> U1 S (U2;0)^T G, with U1, U2 upper triangular unipotent of degree ≤2 and S ranging over all permutations. Compare the dimension of this closure with the dimension of F0 ∩ F~≤2, obtained from the dominant map X≤2 -> F~≤2. If the Bruhat-like closure has strictly smaller dimension, the KIK+24 output set is not Zariski dense in F, confirming that Theorem 2.3 does not transfer to the advertised dataset generator.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central advertised claim is that datasets generated by the KIK+24 algorithm are shown to be sufficiently general. What Theorem 2.3 / Corollary 4.12 actually proves is that F0 = {U[En;0]G | U in E(m)} is dense in F, under Heuristic 2.2 and m >= 2n >= 3. This F0 is the output set of the paper's new Algorithm 2, not of the specific KIK+24 construction. In [KIK+24], A is built via the restricted Bruhat-like form A = U1 S (U2;0)^T with U1, U2 upper triangular unipotent and S a permutation. Those A do lie in F0, so the proved set is a superset of the KIK+24 output set; but Zariski density of a superset does not imply density of the subset. The paper contains no statement or proof that the restricted Bruhat-like family is itself dense in F, and it is not a formal consequence of Proposition 4.2. There is also a parameter-regime gap: the theorem assumes m >= 2n, whereas the KIK+24 experiments use m <= n+2 (Remark 2.6), leaving only n=2, m=4 as overlap. Thus even if Heuristic 2.2 were fully verified, the advertised geometric justification for the actual KIK+24 training data would not follow. A parameter count for the minimal overlap case (7ND Bruhat-like parameters vs 8ND for the full left-regular locus) strengthens the suspicion that the restricted family has smaller dimension and is not dense, but the decisive point is the missing logical bridge.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper studies the geometric generality of training data for Transformer-based Gröbner basis computation. It formulates Problem 2.1: an algorithm that, for a fixed tuple G of polynomials, randomly outputs generators F of the ideal ⟨G⟩, such that the set F0 of all possible outputs is Zariski dense in the set F of all generator tuples of ⟨G⟩. The authors propose Algorithm 2, which outputs F = A G where A = U (En;0)^T and U is a finite product of elementary matrices over the polynomial ring R. They prove (Theorem 2.3/Corollary 4.12) that, over a Hilbertian field, for m ≥ 2n ≥ 3 and under Heuristic 2.2 (irreducibility of X≤D), the set F0 ∩ \tilde F≤D is dense in \tilde F≤D; Corollary 2.4 upgrades this to density of F0 in F when the heuristic holds for all sufficiently large D. The proof uses Quillen–Suslin, Suslin's stability theorem, and Hilbert's irreducibility theorem. The introduction and abstract further claim that this justifies the earlier dataset generation method of [KIK+24].","tokens_in":16742,"tokens_out":17453,"duration_ms":182087,"significance":"If the conditional theorem is correct, it provides a genuine geometric statement about a class of generator-construction algorithms: the possible outputs are Zariski dense rather than confined to a special subvariety. The use of Quillen–Suslin to replace left-regular matrices by an elementary-matrix action is elegant, and the section construction in Corollary 4.12 is a good idea. The paper is also honest in labelling Heuristic 2.2 as an assumption, and the proof is mostly self-contained. However, the significance as stated in the abstract is not achieved: the theorem concerns the new generalized Algorithm 2, not the specific Bruhat-like construction of [KIK+24], and it applies in a parameter regime (m≥2n) that is disjoint from the experiments except for n=2,m=4. The unproven Heuristic 2.2 and the flat-locus proof gap further limit the current version.","major_comments":[{"comment":"The advertised claim that the dataset generation algorithm of [KIK+24] is shown to be sufficiently general is not supported by the theorems. Theorem 2.3 and Corollary 4.12 prove that F0 = {U(En;0)^T G | U ∈ E(m)} is dense in F, and Proposition 4.2 identifies this set with all outputs F=AG for left-regular A over R. The construction of [KIK+24] recalled in §3.1 uses the restricted Bruhat-like family A = U1 S (U2;0)^T. Since F0 is a superset of the KIK output set, density of F0 says nothing about density of the restricted family. No statement or proof in the paper establishes that the Bruhat-like family is itself Zariski dense in F, and the missing logical bridge is not repaired by Proposition 4.2, which only characterizes the larger class.","section":"Abstract, §2.2, §3.1"},{"comment":"There is a parameter-regime mismatch: the main theorem assumes m ≥ 2n ≥ 3, whereas Remark 2.6 states that the experiments in [KIK+24] impose m ≤ n+2. For n ≥ 3 these conditions are incompatible; the only overlapping case is (m,n) = (4,2). Thus even if Heuristic 2.2 were fully justified, the theorem would not cover the experimental regime used in the prior work. The authors should prove a version for m < 2n or explicitly restrict their claims to the new setting.","section":"Remark 2.6 / Theorem 2.3"},{"comment":"The core density theorem is conditional on Heuristic 2.2, the irreducibility of X≤D, for which the paper offers no proof, no evidence, and no discussion of regimes where it might fail. Since this assumption is load-bearing for Lemma 4.10 and Theorem 4.11, and hence for Theorem 2.3, the paper's central conclusion is only an implication from an unverified algebraic-geometric statement. At minimum, the authors should prove or test irreducibility in nontrivial cases such as n=2, m=4, or give a structural argument based on the equations (BA−En)G=0.","section":"Heuristic 2.2"},{"comment":"The proof that the flat locus Y is nonempty contains a gap. The sentence 'Let L be the field of fractions ... Then Spec L is isomorphic to a non-empty open subscheme V in R^{n×n}_{≤D}' is not correct: Spec L is the generic point and is not an open subscheme of a positive-dimensional affine space. Consequently the claim Y ≠ ∅ is not established as written. The gap appears repairable by invoking generic flatness for finite-type morphisms to a reduced Noetherian scheme, which gives a nonempty open V over which p is flat, but the current text does not supply that argument.","section":"Corollary 4.12 / Theorem 4.11"},{"comment":"Problem 2.1 and the abstract formulate the result in terms of datasets being dense, but a finite training dataset is never Zariski dense in an infinite variety. What the proof actually establishes is that the set of all possible outputs of Algorithm 2 is dense in the set of all generators of ⟨G⟩. This distinction matters for the claimed learning guarantee: density of the generator's support is only a necessary condition for a finite sample to be representative, not a sufficient one. The paper should state this limitation explicitly.","section":"Problem 2.1 / Abstract"}],"minor_comments":[{"comment":"In the displayed definition of \tilde F≤D before Lemma 4.10, the notation X_{≤D}^{m×n} is inconsistent with the definition of X_{≤D} in Heuristic 2.2; this appears to be a typo.","section":"§4.2"},{"comment":"In the proof, the displayed factorization uses the symbol u3 twice in the second factor; this is presumably a typo and should involve two distinct coefficients.","section":"Lemma 4.8"},{"comment":"There is a typo: 'basss' should be 'bases'.","section":"§3.1"},{"comment":"The notation F = {F ∈ R^m | ⟨F⟩ = ⟨G⟩} treats G as fixed, while Problem 2.1 presents G as an input; please make the dependence on G explicit in the notation throughout.","section":"§2.1"}],"recommendation":"major_revision","confidential_remarks":"The gap between the abstract and the proven theorem is substantial. If the authors cannot prove density of the specific Bruhat-like family used in [KIK+24], the title, abstract, and Remark 2.5 should be revised so that the claim concerns the generalized Algorithm 2 under Heuristic 2.2. The flat-locus gap in Corollary 4.12 is likely repairable with generic flatness, but the KIK-family issue is a logical bridge that the current manuscript does not supply. I would not recommend acceptance before this is resolved."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a look if you care about ML-for-symbolic-math theory, but read it with the abstract flagged. The paper's real contribution is a conditional Zariski-density theorem for a broad class of generator tuples: for m≥2n≥3 and a Hilbertian field, and assuming Heuristic 2.2, the outputs of their Algorithm 2 are dense in the set of all generator tuples of a given ideal. The proof is built from standard but non-obvious ingredients—Quillen-Suslin, Suslin's stability theorem, and Hilbert's irreducibility—and the treatment of the determinant as an irreducible polynomial in Lemma 4.8 is credible. That is genuinely new.\n\nThe soft spots are in the packaging. The abstract and Remark 2.5 claim the density result applies to the dataset generation algorithm of KIK+24. It doesn't, as far as the paper shows. Theorem 2.3 concerns F0 = {U[En;0]G | U ∈ E(m)}, the output set of the new Algorithm 2. The KIK+24 construction restricts to a Bruhat-like family U1 S (U2;0) with triangular unipotent blocks, which is a proper subset of that F0. Zariski density of a superset says nothing about the subset, and the paper contains no proof that the restricted family is itself dense. The parameter mismatch makes the gap concrete: the theorem needs m≥2n, while the experiments in KIK+24 use m≤n+2, so the overlap is only n=2, m=4. Remark 2.6 admits this but still leans on the theorem for support.\n\nSecond, the result is conditional on Heuristic 2.2, an irreducibility statement about X≤D that is substantial and unproven. The paper gives no evidence. That is fine for a theorem if the statement is honest, but the abstract omits the condition entirely. The introduction does say 'assuming a heuristic,' so the authors are not hiding it from a careful reader.\n\nNet: the conditional theorem is a meaningful step, and the algebraic machinery is used seriously. But the advertised geometric justification for the actual KIK+24 training data is not established. This deserves a real referee, not a desk reject, because the core proof is plausibly correct and the overclaim is fixable. I would ask the authors to either prove density for the restricted Bruhat-like family or rewrite the claims to match what Theorem 2.3 actually shows. The heuristic also needs at least a discussion of plausibility, ideally a proof for relevant G.","headline":"A solid conditional density theorem for a generalized generator construction, but the abstract overclaims: the result does not cover the restricted output set of the KIK+24 dataset, and the key heuristic is unproven.","tokens_in":17236,"tokens_out":3453,"would_cite":false,"duration_ms":33037,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-16T12:33:13.669666+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}