{"id":"c228cd2f-7147-4c31-b54f-46d51cb2e764","arxiv_id":"2505.23696","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A Transformer oracle that predicts useful expansion steps in border basis computations cuts runtimes up to 3x over the baseline while a fallback cap keeps the output provably correct.","lead":"This paper trains a Transformer to predict which reduction steps in a border basis computation are worth running, skipping wasteful candidates and speeding up the algorithm up to 3x in wall-clock time (3.5x fewer useless reductions) while preserving exact, correct output through a capped fallback to the standard algorithm. It is worth reading as a template for adding learned predictions to exact symbolic computation without sacrificing correctness guarantees.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Correctness proof of Theorem 3.1 omits the early-termination path: Algorithm 2 can exit the while-loop before the k oracle calls are used, so the 'maintains output guarantees' claim is unproven for that case.","rationale":"The reader's weakest assumption concerns the runtime profile and the border-gap heuristic; that is a legitimate speedup concern, but it does not threaten the paper's differentiator—the correctness guarantee. The more fundamental issue is that the guarantee is not proven for the early-exit path. Algorithm 2's loop can terminate before the oracle budget k is exhausted whenever BorderBasisCheck passes after an oracle-guided iteration. The proof in Appendix A only handles the case where all k calls are made and a full expansion follows. Because the oracle learns to predict 'no expansion' with high frequency, and its no-expansion accuracy is below 100%, the early-exit path is not a theoretical curiosity; it is expected in a small fraction of runs. Without a final full expansion before any break, or an independent verification that OBBA's output equals IBBA's output on the test instances, the claim 'without compromising the correctness of results' is not backed by the presented proof or experiments. I recommend keeping the reader's CONDITIONAL verdict, with the primary condition being: close this proof gap (e.g., always perform one full expansion before terminating, or prove that an oracle 'no expansion' implies the full candidate set yields no new generator) and empirically check output equality on all benchmark instances. The runtime-profile concern should remain a secondary revision point.","tokens_in":33308,"tokens_out":19908,"duration_ms":193075,"concrete_test":"Instrument the released implementation of Algorithm 2 and record, for each of the 100 in-distribution runs in Table 2 (n=5, F31, degree 2), the iteration at which the while-loop breaks and the number of oracle calls used. For every run that breaks before the k=5th call, re-run IBBA on the same input and check: (a) whether one full expansion from the break point would add a generator (BasisExtension returns V_{i+1}≠V_i), and (b) whether FinalReduction(V_i,L_i) returns the same border basis as IBBA. If any early-breaking run satisfies (a) or (b), Theorem 3.1's guarantee is violated as stated; if none occurs in-distribution, run the same check on the OOD degree-8 setting of Figure 3 where fallbacks are reported.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim that OBBA 'maintains output guarantees' rests on Theorem 3.1 (Appendix A.1). The proof of Theorem A.1 only covers runs that consume all k oracle calls: 'After the oracle has been invoked k times, we make one more full expansion.' It does not cover the path where the while-loop in Algorithm 2 breaks early. The loop exits as soon as Vi+1 = Vi and BorderBasisCheck passes (Algorithm 2, lines 6, 10, 18). The oracle is allowed to return an empty candidate set—Table 1 reports 'No Expansion Accuracy' of 96.3–99.7%—so a false positive in the no-expansion class (0.3–4% of termination predictions) causes early exit before the post-k full-expansion safety net. On that path, FinalReduction is applied to a V that may not be the full L-stable span, because BasisExtension only saw the oracle's subset of candidates, and the paper reports no comparison of OBBA outputs against IBBA outputs to rule out wrong results. The k-call cap bounds the number of oracle-guided non-full expansions inside the loop, but it does not force a final full expansion when the loop terminates early. Thus the correctness guarantee, as stated, is not established for the early-exit path.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes the Oracle Border Basis Algorithm (OBBA), which integrates a Transformer oracle into the border basis algorithm to select which polynomial expansions to reduce, with a cap of k oracle-guided iterations after which the algorithm reverts to full expansions. The authors introduce a sampling framework for border bases based on vanishing ideals, an ideal-invariant generator transform, and a monomial embedding that reduces token counts. Experiments over F_7, F_31, and F_127 with n = 3, 4, 5 report in-distribution wall-clock speedups of about 3x over IBBA (Table 2) and out-of-distribution speedups up to 1.8x (Figure 3), while Theorem 3.1 claims termination and correctness of the output.","tokens_in":33395,"tokens_out":9814,"duration_ms":96364,"significance":"The proposed combination is interesting and, if the correctness guarantee is fully established, would be a useful contribution: unlike prior learning-based Groebner basis methods, OBBA preserves exactness by construction through the k-call fallback. Strengths include the non-circular data generation (labels come from exact BBA runs), the monomial embedding with measured token reductions, the orthogonal FGE kernel, and the release of code. The out-of-distribution generalization from degree 2 to degree 8, despite increased fallbacks, is a noteworthy empirical result. However, the correctness proof has a gap for early termination, and the headline speedup number is not consistently supported by the wall-clock tables.","major_comments":[{"comment":"The proof of Theorem A.1 only covers runs that exhaust the k oracle calls: 'After the oracle has been invoked k times, we make one more full expansion.' It does not address the early-exit path in Algorithm 2, where the while-loop breaks as soon as V_{i+1} = V_i and BorderBasisCheck passes (lines 6, 10, 18) before k calls are used. Because the oracle can return an empty candidate set (Table 4 reports No Expansion accuracy between 96.3% and 99.7%), a false 'no expansion' prediction can terminate the loop before the safety-net full expansion, and the output then depends on an incomplete V. No experiment compares OBBA outputs against IBBA outputs to rule out wrong results on that path. The correctness guarantee is therefore not established as stated; please either modify the algorithm to force a final full expansion or a border-basis check regardless of the exit path, or extend the proof to cover early exit.","section":"Appendix A.1, Theorem A.1; Algorithm 2"},{"comment":"The pseudocode does not match the described and implemented method. Algorithm 1 (and Algorithm 2) unconditionally executes both C_i <- V_i^+ and C_i <- Oracle(L_i, V_i), with no k-call counter and no relative-border-gap condition; Section 3.2 and Section 5.3.1 state that the oracle is invoked only after |V|/|L| reaches a threshold and then at most k times. Since Theorem A.1's argument relies on the k-call cap, the theorem applies to an algorithm that is not the one written down. Please align the pseudocode, the proof, and the implementation (including the fallback and the gating heuristic).","section":"Section 3, Algorithms 1 and 2; Section 5.3.1"},{"comment":"The abstract and conclusion claim wall-clock 'speedup factors of up to 3.5x', but Table 2 reports a maximum wall-clock speedup of about 3x (n = 5, F31: 7.60/2.58 is approximately 2.95). The 3.5x figure in Table 5 is an improvement in the number of zero reductions, not runtime. Please either report the 3.5x as reduction count, or locate a wall-clock setting that achieves 3.5x and cite it.","section":"Abstract; Conclusion; Table 2; Table 5"},{"comment":"The practical speedup rests on the assumption that the last stage after the final universe enlargement consumes 70-95% of runtime (Table 9) and that the relative border gap |V|/|L| reliably identifies that stage. Lemma A.2 does not establish the heuristic: it assumes |L| - |V| = |O| and then observes that adding an element would contradict the equality; it says nothing about how to detect the final stage from the gap. The paper should state the gap heuristic as an empirical assumption, report sensitivity of the speedup to the invocation threshold (the OOD figures already show threshold dependence), and avoid presenting Lemma A.2 as a theoretical justification for the detection rule.","section":"Section 3.2; Lemma A.2; Table 9; Figures 10-12"}],"minor_comments":[{"comment":"Please clarify whether the 1M training samples are per (n, p, l) configuration or total across all 27 datasets; the text says 'one million training and one thousand evaluation samples' after collecting 'approximately five million samples' from the final five expansions, and the aggregation is ambiguous.","section":"Section 5.2, Dataset"},{"comment":"There is a typo: 'unneccessary' should be 'unnecessary'.","section":"Table 2 caption"},{"comment":"There are typos: 'boder' should be 'border' in Appendix B.2, and 'predesgianated' should be 'predesignated' in Appendix E.1; reference [9] also contains a stray 'V ol'.","section":"Appendix B.2 and Appendix E.1"},{"comment":"The experiments do not specify the monomial order used to determine leading terms in the BBA runs and in the generated data; since the oracle input representation and the training labels depend on it, this should be stated for reproducibility.","section":"Section 5, experimental setup"},{"comment":"The speedup plots are shown as mean lines without error bars or confidence intervals; given the large standard deviations reported in the runtime tables, adding variance information would make the comparisons more informative.","section":"Figure 3 and Figures 8-9"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is in scope and the empirical setup is generally sound, but the correctness-proof gap for the early-exit path is the main technical obstacle. If the authors close it by an algorithmic change or by proving that early exit cannot occur when the oracle is wrong, the paper would be acceptable; the 3.5x versus 3x discrepancy is easy to fix. I also suggest the authors run a direct output-equivalence check between OBBA and IBBA on a sample of in-distribution and OOD instances, since the paper currently reports no such comparison."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a solid, modest algorithms-with-predictions paper that deserves a real referee, but it needs a revision that closes a proof gap, fixes an overstated abstract, and tightens the empirical reporting.\n\nWhat's genuinely new: the OBBA framework—a Transformer oracle that proposes candidate BBA expansions, capped at k calls per run, after which the algorithm reverts to the exact full expansion. The correctness guarantee is real and simple in the k-call case, and it's the first work in this line to preserve exactness rather than just steering with no guarantees. The monomial embedding (Section 4.2) is a clean, reusable idea: one token per monomial instead of n+1, with O(n) token reduction and real gains in memory and predictive accuracy. The data-generation pipeline is also useful: order ideal sampling plus the ideal-invariant generator transform (Theorem 4.5) gives a way to create diverse zero-dimensional systems, and the FGE kernel is a nice orthogonal speedup.\n\nNow the soft spots, in order of size.\n\n1. The early-exit correctness gap. The proof of Theorem A.1 covers only the path where all k oracle calls are used and then a final full expansion is made. But the algorithm's loop can exit earlier, as soon as Vi+1=Vi and BorderBasisCheck passes. All 100-instance runs in Section 5.3.1 terminated without ever reverting to the fallback, so the tested path is the one the proof doesn't cover. This is fixable: BorderBasisCheck is the Buchberger criterion, which is sufficient for V to be a border basis, so the early exit is likely safe. But the paper never states that argument, and a referee should insist on it. The stress-tester's concern here is a proof gap, not a demonstrated counterexample.\n\n2. The abstract's 'up to 3.5x speedup' is misleading. Table 2 reports a 3x wall-clock speedup over IBBA; the 3.5x figure in Table 5 is a reduction count, not runtime. They should report the former prominently and the latter as a secondary metric.\n\n3. Theorem 4.5's r=n case has a proof issue: it assumes pure-power leading terms for the border basis, which general term-order-free border bases need not have. The r>n case is what's used, so the gap shouldn't hold up the paper, but it should be stated with the needed hypothesis or removed.\n\n4. The baseline is the authors' own IBBA implementation, with no comparison to optimized Gröbner solvers. That's acceptable for isolating the oracle's effect, but it limits the headline claim's real-world reach. And the paired 100-run results lack significance tests; for n=3 and 4 the speedups are within noise given the large standard deviations.\n\nWho this is for: people working on ML-steered symbolic computation, algorithms with predictions, and border basis methods. It's a good data point and a reusable representation idea. Give it a serious referee, with the expectation of moderate revision.","headline":"A genuine but modest advance in learning-guided symbolic computation that needs a revision to close the early-exit proof gap and align its claims with its tables.","tokens_in":34145,"tokens_out":6658,"would_cite":false,"duration_ms":61996,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68W30","13P10","68T07"],"pacs":[],"model":"deepseek-v4-flash","headline":"A Transformer trained on border basis runs can predict which reduction steps are unnecessary, letting the Oracle Border Basis Algorithm skip them and achieve up to 3.5x fewer zero reductions and about 3x wall-clock speedup while still…","keywords":["border basis","transformer","polynomial system solving","algorithms with predictions","monomial embedding","zero-dimensional ideals","symbolic computation","deep learning"],"falsifier":"Run OBBA on a family of zero-dimensional systems where reduction cost is spread evenly across all expansions rather than concentrated in the final stage; if wall-clock time does not improve over the improved border basis baseline, or if the relative border gap |V|/|L| is not monotonically related to the remaining number of expansions, the runtime-profile assumption that the method depends on is falsified.","tokens_in":32862,"feed_emoji":"🧮","tokens_out":6357,"duration_ms":64851,"temperature":0.7,"pith_summary":"This paper aims to show that a Transformer trained on labeled border basis runs can act as an oracle inside the algorithm, skipping expensive reduction steps while preserving an exact output. The payoff is that zero-dimensional polynomial systems could be solved faster in practice without the correctness loss that earlier deep-learning polynomial solvers accepted. The authors introduce the Oracle Border Basis Algorithm (OBBA), prove that it terminates and returns a border basis, and report up to 3.5x fewer zero reductions and about 3x wall-clock speedup over the improved border basis algorithm on five-variable systems. The guarantee is preserved by a strict cap: the oracle replaces the full expansion at most k times, after which the standard expansion resumes.","feed_headline":"Learned oracle speeds polynomial solving 3x, still exact","feed_subtitle":"A capped Transformer skips redundant reduction steps in border basis algorithms, keeping outputs provably correct.","key_machinery":"The mechanism is the L-stable-span step of the border basis algorithm, where each iteration multiplies the current basis by variables and reduces the candidates; most candidates reduce to zero. OBBA replaces the candidate set C_i = V_i^+ with a predicted subset C_i = Oracle(L_i,V_i). The Transformer uses a monomial embedding that encodes each monomial as a single token, cutting token count by a factor of n+1. The k-call cap and fallback to full expansion carry the correctness proof. Training data comes from a new border basis sampling construction (order ideals plus vanishing ideals) and an ideal-invariant generator transform that converts basis polynomials into diverse generating sets with the same ideal.","core_discovery":"The central claim is that the wasteful part of border basis computation—reducing candidate polynomials that do not extend the basis—can be predicted and avoided. A Transformer oracle trained on the final five expansions of completed runs selects which variable-times-basis-element products to reduce; the algorithm spends its oracle budget only when the relative border gap |V|/|L| indicates the final stage. Because the oracle is capped at k calls and a full expansion follows, Theorem 3.1 guarantees the output is a border basis regardless of oracle accuracy. Empirically, the oracle eliminates up to 3.5x as many zero reductions and cuts wall-clock time by about 3x versus the improved border basis algorithm on n=5 systems over F31, and generalizes to degree-8 systems with up to 1.8x speedup.","pith_inferences":["The speedup numbers are measured against a specific runtime profile; on problems where the final stage is not dominant, the benefit may shrink or invert because the oracle budget is spent before the expensive phase.","The oracle-plus-cap scheme could be attempted for Gröbner base computation, but the lack of an inherent degree-by-degree decomposition is precisely the obstacle noted for the earlier RL approach; a supervised analogue would need a new way to label successful S-polynomials.","Because the correctness guarantee is independent of oracle quality, even a low-accuracy oracle could be used safely; the observed benefit would then degrade gracefully rather than producing wrong answers.","Training on finite fields may not transfer to characteristic zero, since coefficient arithmetic and the density of polynomials differ; testing on rational or floating-point inputs would delimit the method's scope."],"forward_implications":["If the Transformer oracle generalizes as reported, border basis computation for zero-dimensional systems with up to five variables can be accelerated without the correctness risk that accompanied earlier deep-learning solvers.","The k-call cap provides a general template: any learned oracle that proposes steps in an exact algorithm can be layered on without changing the output, as long as it can be overridden.","The monomial embedding could transfer to other monomial-centric symbolic computations, reducing input length and attention cost.","The border basis sampling and ideal-invariant transform enable supervised data generation for other algebraic computations that have a degree-by-degree structure.","The reported out-of-distribution generalization suggests the oracle may handle harder instances than those seen during training, though this is demonstrated only for moderate degree increases."],"supporting_citations":[{"why":"Supplies the improved border basis algorithm (IBBA) that OBBA is compared against and whose final stage is profiled.","marker":"[26]"},{"why":"Provides the border basis division algorithm and characterization used in the correctness argument and FinalReduction.","marker":"[25]"},{"why":"The ideal-invariant generator transform generalizes this prior work, and it is the prior transformer approach that lacks output guarantees.","marker":"[32]"},{"why":"Defines the encoder-decoder Transformer architecture used for the oracle.","marker":"[58]"},{"why":"Frames the algorithm-with-predictions perspective that motivates preserving correctness while using learned advice.","marker":"[48]"},{"why":"Gives corner terms and border basis background used to compress the input representation.","marker":"[37]"},{"why":"Buchberger's algorithm is the classical target that border bases generalize; the paper contrasts with it to motivate correct acceleration.","marker":"[9]"}],"fun_headline_variants":["Transformer oracle cuts polynomial solving time 3x, proves exact","Oracle Border Basis: 3x faster, still provably correct","AI oracle skips useless steps, speeds polynomial solving 3x","First oracle for border bases: up to 3.5x speedup, exact"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the final stage of the border basis algorithm—after the last enlargement of the computational universe—consumes 70-95% of the runtime and that the relative border gap |V|/|L| reliably marks the start of that stage; if this profile does not hold, the oracle budget is spent where it produces little or no speedup.","fun_headline_variants_meta":{"raw":{"variants":["Transformer oracle cuts polynomial solving time 3x, proves exact","Oracle Border Basis: 3x faster, still provably correct","AI oracle skips useless steps, speeds polynomial solving 3x","First oracle for border bases: up to 3.5x speedup, exact"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000604,"raw_usage":{"total_tokens":2808,"prompt_tokens":926,"completion_tokens":1882,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":542,"completion_tokens_details":{"reasoning_tokens":1804}},"tokens_in":542,"tokens_out":1882,"duration_ms":12802,"temperature":1.0,"reasoning_tokens":1804,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T12:42:21.002566+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run OBBA on a family of zero-dimensional systems where reduction cost is spread evenly across all expansions rather than concentrated in the final stage; if wall-clock time does not improve over the improved border basis baseline, or if the relative border gap |V|/|L| is not monotonically related to the remaining number of expansions, the runtime-profile assumption that the method depends on is falsified.","supporting_citations":[{"cited_title":"Kehrein and M","cited_arxiv_id":null,"evidence_quote":"Supplies the improved border basis algorithm (IBBA) that OBBA is compared against and whose final stage is profiled."},{"cited_title":"Kehrein and M","cited_arxiv_id":null,"evidence_quote":"Provides the border basis division algorithm and characterization used in the correctness argument and FinalReduction."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The ideal-invariant generator transform generalizes this prior work, and it is the prior transformer approach that lacks output guarantees."},{"cited_title":"Vaswani, N","cited_arxiv_id":null,"evidence_quote":"Defines the encoder-decoder Transformer architecture used for the oracle."},{"cited_title":"Mitzenmacher and S","cited_arxiv_id":null,"evidence_quote":"Frames the algorithm-with-predictions perspective that motivates preserving correctness while using learned advice."},{"cited_title":"Kreuzer and L","cited_arxiv_id":null,"evidence_quote":"Gives corner terms and border basis background used to compress the input representation."},{"cited_title":"Buchberger","cited_arxiv_id":null,"evidence_quote":"Buchberger's algorithm is the classical target that border bases generalize; the paper contrasts with it to motivate correct acceleration."}],"review_version":1}