{"id":"dda0234b-63a7-4a0a-a156-e9dfb195cd47","arxiv_id":"2504.19705","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":8,"one_line_summary":"STAGG combines LLM-generated candidate programs, a learned probabilistic grammar, and enumerative search to lift dense tensor C code into TACO, solving 76 of 77 benchmarks.","lead":"This paper describes STAGG, a tool that uses GPT-4 to guess candidate TACO tensor programs from C code, then searches those guesses systematically to find a program that is provably equivalent to the original. It reports lifting 76 of 77 benchmarks, more than existing tools, potentially automating a tedious step in moving machine learning code to high-performance DSLs.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 99% lifting-accuracy claim depends on a bounded, rational-arithmetic equivalence check whose bound is never specified; without further evidence, 'solved' benchmarks are not shown to be fully equivalent.","rationale":"I agree with the reader's weakest assumption: the correctness gate for every solved benchmark is the CBMC check, so the unstated bound and the rational abstraction are the most load-bearing limitation. If the bound is smaller than the relevant input space, or if a benchmark's real semantics are IEEE floating point, then 'solved' does not imply equivalent, and the 99% figure could be inflated. This concern is more fundamental than the secondary issues: the hand-designed penalty functions in Section 5.1 do contradict the 'no pre-wired heuristics' summary, and the absence of an artifact makes numbers hard to audit, but those affect the framing and reproducibility rather than the truth of individual solutions. The paper deserves credit for using bounded verification instead of I/O tests alone and for a broad comparison against C2TACO and Tenspiler, but the verification bound and data-type semantics must be reported and stress-tested before the central correctness claim can be accepted. Since the reader already returned CONDITIONAL, my read does not change the verdict; it sharpens the condition.","tokens_in":21684,"tokens_out":8525,"duration_ms":92365,"concrete_test":"Select the solved benchmarks that use dynamic loop bounds and floating-point arithmetic. Re-run the verification pipeline with (i) a doubled and quadrupled CBMC unwind bound and (ii) IEEE floating-point semantics instead of rational datatypes, comparing original and lifted programs on inputs at and beyond the original bound. If any benchmark that previously passed now fails or produces different outputs, the headline accuracy is an overstatement and the paper must report the bound and data-type coverage before the claim can be accepted.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2 defines the problem as finding p_t with ∀x. p_s(x)=p_t(x), but Section 7 only checks this with CBMC 'for all possible inputs up to a certain bound' and over rational datatypes. The paper never states the bound, how it relates to each benchmark's input sizes, or whether any benchmark uses floating-point arithmetic. For loop-based C code, bounded model checking unwinds loops a finite number of times; a program that passes at bound k can fail at bound k+1, so a 'solved' benchmark may only be equivalent on a finite prefix of its input space. Replacing IEEE floats with rationals is likewise a semantic change: equality under rational arithmetic does not imply equality under IEEE rounding, and TACO-generated code may reorder operations. Since every benchmark is counted as solved only after this verification step, an unsound or incomplete check would overstate the 76/77 result. The concern is not that the method is wrong, but that the reported evidence establishes only bounded, idealized equivalence, not the full equivalence promised in the problem statement.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"STAGG is a hybrid lifting system that translates legacy C tensor code into TACO programs. Given a C program, it prompts an LLM (GPT-4) for ten candidate TACO expressions, normalizes these candidates into templates, and learns a probabilistic context-free grammar from them. A weighted A*-style search (top-down and bottom-up variants) enumerates templates, guided by grammar probabilities and hand-set penalty rules. Candidate instantiations are first filtered by randomized input/output tests and then checked with CBMC for bounded equivalence against the original C program. The paper reports that STAGG-TD solves 76 of 77 benchmarks (98.7%) and outperforms C2TACO (67/77) and Tenspiler (52/67), with an average time of 3.19 s on the C2TACO-solvable subset. Ablations study the contributions of grammar refinement, learned probabilities, and penalty functions.","tokens_in":21922,"tokens_out":7401,"duration_ms":70716,"significance":"If the correctness evidence is accepted, this is a significant contribution to verified lifting: it replaces hand-crafted search heuristics with an LLM-derived probabilistic grammar, and the component ablations (grammar refinement, probabilities, penalties) are a genuine strength of the evaluation. The paper also describes the synthesis algorithms in enough detail to be reimplemented, and the use of bounded model checking after I/O validation is an improvement over approaches that rely on I/O testing alone. However, the headline claims currently outrun the evidence in two load-bearing places: the verification step is bounded and uses rational arithmetic as a substitute for the original semantics, and the assertion that the system works 'without any pre-wired heuristics' is contradicted by the hand-set penalty constants and search limits. Both are fixable in revision, which is why I do not recommend rejection, but they must be addressed before the claims can be taken at face value.","major_comments":[{"comment":"The problem statement in Section 2 requires full equivalence (∀x. p_s(x)=p_t(x)), but the verification described in Section 7 only establishes that the generated assertion 'holds for all possible inputs up to a certain bound.' The bound is never stated, and no explanation is given of how it relates to each benchmark's input sizes or loop structure. For loop-based C programs, bounded model checking unwinds loops finitely, so a program that passes at bound k can fail at a larger bound. Because every solved benchmark is reported as solved only after this check, the 76/77 (99%) success claim is currently supported only as bounded, not universal, equivalence. Please specify the bound(s) used, justify that they cover the input space of each benchmark, or state the results as bounded-equivalence results.","section":"7, Verifier"},{"comment":"The use of rational datatypes changes the semantics of the programs being verified. Section 7 says CBMC is extended 'to support rational datatypes, and verify equivalence using rational datatypes.' If the benchmark C programs contain integer arithmetic that can overflow, or floating-point arithmetic, rational-arithmetic equivalence does not imply equivalence under the original C semantics: integer wrap-around, floating-point rounding, and reassociation are not modeled. The paper does not state which of the 77 benchmarks use floating-point datatypes or whether the correctness claim is intended to hold under rational arithmetic only. This needs to be clarified and, if any benchmark uses non-rational semantics, the verification pipeline must be adapted or the claim qualified.","section":"7, Verifier"},{"comment":"The central claim that the approach works 'without any pre-wired heuristics' is contradicted by the design in Section 5.1 and the evaluation. The penalty criteria a1–a5 with hand-set weights (10, 100, infinite), the length and depth limits, the fixed number of 10 LLM solutions, the temperature 1.0, and the dimension-list filtering rule are all manually chosen, and Table 2 shows that they materially change the number of benchmarks solved. These are pre-wired heuristics. Please revise the claim to reflect that the LLM learns the grammar/probabilities while the search parameters and penalty rules are manually configured, or provide an ablation showing that the exact values of these constants are not important to the results.","section":"Abstract, Conclusion, Section 5.1"},{"comment":"The text reporting the equal-probability ablation contradicts Table 3. The paragraph on RQ4/RQ5 states that 'using equal probabilities on the refined grammar results in an increase in the number of benchmarks solved for STAGGTD,' but Table 3 reports STAGGTD solving 76 benchmarks and STAGGTD.EqualProbability solving 73, a decrease. Similarly, for STAGGBU, EqualProbability (74 benchmarks, 180.31 s) is not faster than STAGG (73 benchmarks, 98.81 s) as claimed. The prose should be corrected to match the table, and the discussion of whether probabilities have a positive or negative effect should be rewritten.","section":"8, RQ4/RQ5"}],"minor_comments":[{"comment":"The '99%' success rate is for the 77-benchmark set (76/77 ≈ 98.7%), not for the 67-benchmark real-world set (66/67 ≈ 98.5%); please state the base set wherever a percentage is given. Similarly, the 3.19 s average in the conclusion refers only to the C2TACO-solvable subset, not to the full 77-benchmark suite, where the average is 106.13 s.","section":"8, Figure 10 and Table 1"},{"comment":"Section 2.1 describes verification as compiling the TACO program with the TACO compiler into C and then running bounded model checking, whereas Section 7 describes creating NumPy code from the indexing expression, lowering it to MLIR via JAX, and then generating C. Please reconcile these descriptions and state whether the TACO compiler itself is used in the verified path.","section":"2.1 and 7"},{"comment":"Table 2 refers to 'Drop(A)' without defining which penalty criteria are in group A; the individual a1–a5 rows are clear, but the grouped row should be specified.","section":"Table 2"},{"comment":"The definition of the predicted dimension list, argmax over the filtered set, should specify what is maximized (frequency) and how ties are broken.","section":"4.2.3"},{"comment":"The production for TENSOR2 lists 'b(i,j)' twice; remove the duplicate.","section":"5.2, generated grammar"},{"comment":"The paper provides no artifact URL or data/code release statement; given the sensitivity of the verification bound and the hand-tuned constants, an artifact (including per-benchmark CBMC bounds and penalty configurations) would substantially strengthen reproducibility.","section":"Reproducibility"}],"recommendation":"major_revision","confidential_remarks":"The paper is likely to be acceptable if the authors supply the verification details (CBMC bounds, datatype handling per benchmark) and revise the 'no pre-wired heuristics' claim. Without those changes, the 99% lifting-accuracy result is not yet supported. I would encourage the editor to request an artifact that includes the exact CBMC configuration used for each benchmark."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague, quick take on arXiv:2504.19705. STAGG applies the LLM-learned probabilistic grammar plus enumerative search recipe from Li et al. CAV 2024 and HYSYNTH to the tensor-lifting problem, and does it well enough to solve 76/77 benchmarks versus 67 for C2TACO and 52 for Tenspiler. The new content is the adaptation to TACO, the static analysis for LHS tensor dimensionality, the penalty machinery, and a careful ablation study. Credit where due: the ablations actually support the claims that grammar refinement, learned probabilities, and penalties each help, and the coverage gains are substantial.\n\nThe soft spots are real but manageable. First, the verification step is bounded model checking over rational datatypes, and the paper never states the bound. The problem statement promises forall x equivalence; Section 7 only checks 'up to a certain bound'. So 'solved' is best read as 'equivalent for all inputs within the verified bound', not full equivalence. If any benchmark uses floats, the rational-arithmetic check is also a semantic change. This undercuts the 99% lifting accuracy claim as literally stated. Second, the abstract says 'without any pre-wired heuristics', but Section 5.1 is full of hand-picked penalties: weights 10 and 100, length thresholds, 'fewer than half operations', depth limit 6. Those are heuristics, just not written as grammar rules. Third, minor: no artifact or benchmark list in the arXiv version, so the numbers are not independently checkable yet, and the penalties look in-sample.\n\nNone of this makes the approach wrong. The central idea, using LLM guesses to define a neighborhood worth enumerating, clearly works, and the evaluation is strong enough to take seriously. The paper is also honest about prior work and doesn't oversell the novelty relative to CAV 2024/HYSYNTH beyond the adaptation.\n\nWho is this for? People working on program synthesis, DSL lifting, and LLM-guided search will want to read it. It deserves a serious peer review; the fixes are mostly about reporting (state the bound, describe the penalty tuning, release the artifact) rather than redoing the work.","headline":"STAGG is a credible, well-engineered adaptation of LLM-guided grammar enumeration to tensor lifting with strong benchmark results, but the correctness evidence is bounded and the 'no pre-wired heuristics' claim is overstated.","tokens_in":22534,"tokens_out":3336,"would_cite":true,"duration_ms":32281,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"STAGG lifts 76 of 77 dense tensor benchmarks to TACO using only LLM-learned heuristics.","keywords":["program synthesis","code lifting","tensor algebra","TACO","large language model","probabilistic context-free grammar","enumerative search","bounded model checking"],"falsifier":"Take a benchmark that STAGG reports as solved, run both the original C program and the lifted TACO program on inputs larger than the bounded-model-check bound or on floating-point values engineered to expose rounding, and check whether any output differs; a single mismatch would refute the claimed equivalence for that benchmark.","tokens_in":21452,"feed_emoji":"🧮","tokens_out":8497,"duration_ms":79197,"temperature":0.7,"pith_summary":"STAGG combines a large language model with enumerative program synthesis to translate legacy C tensor code into the TACO tensor DSL, and the paper's central claim is that this combination reaches 99% lifting accuracy (76 of 77 benchmarks) without any pre-wired search heuristics. The LLM is asked for ten candidate TACO expressions; even when those candidates are imperfect, their templates define a probabilistic grammar that focuses the search on the neighborhood where the correct program lies. Two weighted A* search algorithms enumerate this grammar, candidates are filtered by input-output tests, and bounded model checking verifies equivalence with the original code. If the claim holds, automatically porting legacy code to high-performance tensor DSLs becomes practical without hand-crafting domain-specific search guidance for each new target.","feed_headline":"LLM guesses guide tensor-code lifting to 99% accuracy","feed_subtitle":"STAGG turns a few imperfect LLM suggestions into a grammar search that beats C2TACO and Tenspiler on 77 benchmarks.","key_machinery":"The central mechanism is a probabilistic context-free grammar of TACO templates inferred from LLM responses: each candidate program is abstracted into a template with symbolic tensor variables, standardized index names, and templatized constants, and the grammar is built to cover exactly those templates while pruning the full TACO grammar down to the predicted tensor dimensions. The grammar focuses enumeration on the neighborhood of the LLM's guesses, and its production-rule probabilities, computed from left-most derivation frequencies, act as the learned search heuristic. Two enumerators use this grammar: a top-down weighted A* search with five penalty criteria and a bottom-up A* search that builds expressions by appending operators and tensors, both producing complete templates that are instantiated, checked against input-output examples, and verified for equivalence with the original code by bounded model checking.","core_discovery":"On its own terms, the paper's discovery is that a large language model, used only as a source of rough guesses, can supply the entire heuristic content that an enumerative synthesizer needs to lift dense tensor programs into TACO. STAGG parses the LLM's candidate solutions, replaces tensor names, indices, and constants with symbolic forms, and builds a small probabilistic context-free grammar over templates; the grammar constrains the number of tensors and their dimensions, and its rule probabilities come from the frequency of rules in the LLM derivations. A weighted A* search over this grammar, with penalties for syntactically implausible templates, generates candidate programs that are then tested on concrete inputs and finally checked for equivalence with the original C code by bounded model checking on rational datatypes. The reported result is 76 of 77 benchmarks solved, including every benchmark solved by C2TACO or Tenspiler, with an average 3.19 seconds on the C2TACO-solvable subset, and the paper concludes that learned heuristics alone suffice for the task.","pith_inferences":["Because the search space comes solely from LLM guesses, the approach implicitly assumes the LLM's candidate set contains the correct syntactic structure at least in template form; a benchmark whose correct TACO expression is structurally far from every LLM guess would fall outside the grammar.","The verification step checks equivalence under bounded model checking with rational datatypes, so a 'solved' result is rigorously a claim of bounded, rational-arithmetic equivalence; extending the pipeline to IEEE floating-point semantics would require a different or additional correctness argument.","A natural testable extension is to apply the same prompt-to-grammar pipeline to other restrained DSLs, such as Halide or PyTorch einsum, where the check would be whether the LLM's neighborhood assumption holds as strongly outside dense tensor code.","The paper's contrast between the full-grammar and learned-probability configurations suggests that learned probabilities can hurt when the grammar is too broad; a practical deployment might learn grammar refinement and probabilities jointly rather than separately."],"forward_implications":["LLM proposals can replace hand-written heuristics as the search guide: STAGG solves 76 of 77 benchmarks with no pre-wired heuristics, covering every benchmark that C2TACO or Tenspiler solves.","The same architecture should transfer to other DSLs or non-tensor domains wherever a grammar and an equivalence checker exist, since no domain-specific search guidance is hard-wired in.","Learned grammar refinement contributes more to accuracy than the learned probabilities alone: replacing the refined grammar with the full TACO grammar drops solved benchmarks from 76 to 69, while equal probabilities on the refined grammar still solve 73.","The bottom-up variant is faster on commonly solved benchmarks (2.11 seconds average on the C2TACO-solvable set) but solves fewer overall (73 vs 76), because it can only append to the right end of an expression and misses balanced or parenthesized forms."],"supporting_citations":[{"why":"C2TACO is the state-of-the-art enumerative baseline it must beat and supplies 61 of the 67 real-world benchmarks.","marker":"[26]"},{"why":"Tenspiler is the template-based verified-lifting baseline compared on the 67 real-world benchmarks.","marker":"[36]"},{"why":"TACO is the target DSL whose compiler turns synthesized einsum expressions into C for verification.","marker":"[18]"},{"why":"Supplies the top-down weighted A* search over a probabilistic grammar used by the first enumerator.","marker":"[24]"},{"why":"Supplies the guided bottom-up enumeration approach adapted for the second enumerator.","marker":"[4]"},{"why":"Supplies the bounded model checker that verifies equivalence between original and lifted code.","marker":"[19]"},{"why":"Supplies the common intermediate representation into which the original and lifted programs are lowered for comparison.","marker":"[21]"},{"why":"Lowers the NumPy formulation of the candidate TACO program to the common intermediate representation.","marker":"[7]"},{"why":"Array delinearization recovers multi-dimensional access structure used to predict left-hand-side tensor dimensions.","marker":"[31]"},{"why":"Array recovery from pointer arithmetic supports the static analysis that predicts left-hand-side dimensionality.","marker":"[12]"}],"fun_headline_variants":["LLM guesses alone beat hand-coded lifting heuristics","LLM-derived grammar lifts tensor code beyond prior art","Learned grammar from LLM guesses outperforms manual heuristics","LLM guesses guide search to lift tensor code, outperform C2TACO"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that for every benchmark reported as solved, the bounded model check with rational datatypes really does certify equivalence on all inputs that matter, including any floating-point behavior in the original code; if the bound or the rational idealization misses a real divergence, the benchmark is not actually lifted correctly.","fun_headline_variants_meta":{"raw":{"variants":["LLM guesses alone beat hand-coded lifting heuristics","LLM-derived grammar lifts tensor code beyond prior art","Learned grammar from LLM guesses outperforms manual heuristics","LLM guesses guide search to lift tensor code, outperform C2TACO"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000611,"raw_usage":{"total_tokens":2825,"prompt_tokens":909,"completion_tokens":1916,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":525,"completion_tokens_details":{"reasoning_tokens":1844}},"tokens_in":525,"tokens_out":1916,"duration_ms":14783,"temperature":1.0,"reasoning_tokens":1844,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:45:49.092232+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a benchmark that STAGG reports as solved, run both the original C program and the lifted TACO program on inputs larger than the bounded-model-check bound or on floating-point values engineered to expose rounding, and check whether any output differs; a single mismatch would refute the claimed equivalence for that benchmark.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Tenspiler is the template-based verified-lifting baseline compared on the 67 real-world benchmarks."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"TACO is the target DSL whose compiler turns synthesized einsum expressions into C for verification."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the guided bottom-up enumeration approach adapted for the second enumerator."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the bounded model checker that verifies equivalence between original and lifted code."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Array delinearization recovers multi-dimensional access structure used to predict left-hand-side tensor dimensions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Array recovery from pointer arithmetic supports the static analysis that predicts left-hand-side dimensionality."}],"review_version":1}