Guided Tensor Lifting

Alexander Brauckmann; Elizabeth Polgreen; Jos\'e Wesley de Souza Magalh\~aes; Michael F. P. O'Boyle; Yixuan Li

REVIEW 4 major objections 6 minor 40 references

Guided Tensor Lifting

T0 review · 4 major / 6 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read STAGG lifts 76 of 77 dense tensor benchmarks to TACO using only LLM-learned heuristics.

desk verdict 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. read the letter →

arxiv 2504.19705 v1 pith:UHY4OOFK submitted 2025-04-28 cs.SE

Yixuan Li , José Wesley de Souza Magalhães , Alexander Brauckmann , Michael F. P. O'Boyle , Elizabeth Polgreen This is my paper · ORCID

classification cs.SE

keywords programsynthesiscodeliftingtensoralgebraTACOlargelanguagemodelprobabilisticcontext-freegrammarenumerativesearchboundedchecking

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

None 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.

Who 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.

Referee Report

4 major / 6 minor

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.

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 (4)

[7, Verifier] 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.
[7, Verifier] 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.
[Abstract, Conclusion, Section 5.1] 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.
[8, RQ4/RQ5] 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.

minor comments (6)

[8, Figure 10 and Table 1] 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.
[2.1 and 7] 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.
[Table 2] 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.
[4.2.3] The definition of the predicted dimension list, argmax over the filtered set, should specify what is maximized (frequency) and how ties are broken.
[5.2, generated grammar] The production for TENSOR2 lists 'b(i,j)' twice; remove the duplicate.
[Reproducibility] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the synthesized programs are accepted only after independent I/O validation and bounded model checking, so the LLM-derived grammar is a search heuristic rather than a disguised re-statement of the result.

full rationale

STAGG's derivation chain is not circular by construction. The problem statement (Section 2) defines lifting as finding p_t such that forall_x. p_s(x)=p_t(x). The LLM only proposes candidate programs, from which a probabilistic grammar is built (Section 4); the grammar then guides an A* search over templates (Section 5). Crucially, a candidate is not reported as solved merely because it is derivable from the grammar: it must pass random input-output validation (Section 6) and then CBMC bounded model checking (Section 7) before being counted as lifted. The correctness evidence is therefore external to the grammar and to the LLM, so the headline 76/77 result does not reduce to the LLM proposals or to the grammar probabilities by definition. The main caveats are correctness risks rather than circularity: Section 7 verifies equivalence only 'up to a certain bound' and uses rational datatypes instead of IEEE floating point, so the reported 99% accuracy is established only for bounded, rational-idealized equivalence. Similarly, the abstract's claim of doing lifting 'without any pre-wired heuristics' is weakened by the hand-coded penalty functions and depth limit in Section 5.1, but this is an overclaim or evaluation-risk concern, not a circular derivation. The paper also cites the authors' own prior work [24] for the LLM-guided grammar and A* search, but that citation is explicit, the baseline tools (C2TACO, Tenspiler) are external, and the final acceptance test is the verifier, so the self-citation is not load-bearing circularity.

Assumptions & free parameters 8 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new mathematical entities or physical objects. Its load-bearing support is a set of domain assumptions: bounded rational-arithmetic verification is sufficient, static analysis recovers tensor dimensions, and LLM candidates cover the right template neighborhood. The hand-tuned penalty parameters and LLM sampling choices are free parameters that affect the headline success counts.

free parameters (8)

Penalty weights X_a1 and X_a2 = 10 and 100
Hand-chosen weights for syntactic penalties in top-down A* search; performance is sensitive to them (Table 2).
Infinite-penalty criteria a3, a4, a5 and b2 = infinite (excluded from search)
These rules prune entire template classes; if they exclude the correct program, synthesis fails.
Maximum syntax-tree depth limit = 6
Set in Section 5.1; deeper correct programs would be missed.
Number of LLM candidate solutions requested = 10
Prompt asks for 10 solutions; grammar coverage depends on this count.
X_a1 length threshold = 3
Penalty applies when expression length exceeds 3; this threshold affects which multi-tensor expressions are deprioritized.
X_a5 and b2 operation ratio threshold = fewer than half of grammar operations
Complete templates using less than half the available operators are pruned; this assumes correct programs are operator-diverse.
Dimension-list filtering rule for RHS tensors = keep lists with maximum length; choose most frequent
RHS tensor dimensions are predicted from LLM candidates; if the modal dimension list is wrong, the search space excludes the correct program.
LLM sampling temperature = 1.0
Set for GPT-4 when generating candidate solutions; affects diversity and grammar coverage.

assumptions (5)

domain assumption CBMC bounded model checking with a fixed bound is sufficient to establish equivalence for the target programs.
Section 7 says verification holds 'up to a certain bound'; the claim of correct lifting relies on this being adequate for all benchmark inputs.
domain assumption Rational arithmetic exactly models the semantics of the original C programs being lifted.
Section 7 replaces floating point with rational datatypes; this is only valid for integer or rational programs, or if float behavior is irrelevant.
ad hoc to paper The correct TACO program lies in the neighborhood of the LLM's candidate solutions, as captured by the template grammar.
Section 4 states 'we hypothesize that... the correct solution is likely to lie in the neighborhood of the LLM's guesses'; the whole search-space reduction depends on this.
domain assumption Array delinearization and array recovery correctly reconstruct the multi-dimensional structure of the C arrays.
Used in Section 4.2.3 to predict LHS dimensions; if they fail, the grammar fixes the wrong LHS dimension.
standard math Standard CFG, pCFG, and A* search definitions are accepted.
Definitions 4.1 through 4.3 and the search algorithms are standard; no unusual background is introduced.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Guided Tensor Lifting." pith.science (2026). https://pith.science/paper/UHY4OOFK

@misc{pith2026250419705,
  author       = {Pith},
  title        = {Pith review of: Guided Tensor Lifting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UHY4OOFK}},
  note         = {Machine review of arXiv:2504.19705}
}

read the original abstract

Domain-specific languages (DSLs) for machine learning are revolutionizing the speed and efficiency of machine learning workloads as they enable users easy access to high-performance compiler optimizations and accelerators. However, to take advantage of these capabilities, a user must first translate their legacy code from the language it is currently written in, into the new DSL. The process of automatically lifting code into these DSLs has been identified by several recent works, which propose program synthesis as a solution. However, synthesis is expensive and struggles to scale without carefully designed and hard-wired heuristics. In this paper, we present an approach for lifting that combines an enumerative synthesis approach with a Large Language Model used to automatically learn the domain-specific heuristics for program lifting, in the form of a probabilistic grammar. Our approach outperforms the state-of-the-art tools in this area, despite only using learned heuristics.

Figures

Figures reproduced from arXiv: 2504.19705 by the authors.

**Figure 1.** Overview of STAGG. We query the LLM to provide 10 possible solutions in TACO that are equivalent to the input code C. Based on the LLM response, we build a probabilistic grammar and enumerate the space of template programs described by the said grammar. We validate a candidate using I/O examples, and if it passes all tests, we proceed to verification to prove equivalence with the original C implementation. The input… view at source ↗

**Figure 2.** A C implementation of Í𝑁 −1 𝑖=0 Mat1(𝑓 × 𝑁 + 𝑖) · Mat2(𝑖). The result is a dot product between the 𝑓 -th row of Mat1 and vector Mat2. The equivalent synthesized TACO expression is a(i) = b(i,j) ∗ c(j). You are a scientific assistant that knows a lot about transpilation . Translate the following C code to an expression in the TACO tensor index notation . The expression must be valid as input to the taco compiler . Re… view at source ↗

**Figure 3.** A probabilistic context-free grammar template. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Figures from the paper (9 more)

**Figure 4.** Figure 4: Expression standardization. We omit part of the derivation for brevity. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]

**Figure 5.** Figure 5: The grammar for TACO expression in Extended Backus–Naur form, defining the syntax for tensor [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]

**Figure 6.** Figure 6: An example generated template grammar, for the dimension list [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]

**Figure 7.** Figure 7: An example generated template grammar, for the dimension list [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]

**Figure 8.** Figure 8: A set of possible substitutions for the TACO program [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]

**Figure 9.** Figure 9: Cactus plot showing the number of benchmarks solved ( [PITH_FULL_IMAGE:figures/full_fig_p017_9.png]

**Figure 10.** Figure 10: Success rates of different approaches on the set of [PITH_FULL_IMAGE:figures/full_fig_p018_10.png]

**Figure 11.** Figure 11: Impact of different grammar configurations in [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]

**Figure 12.** Figure 12: The performance of difference configurations of [PITH_FULL_IMAGE:figures/full_fig_p020_12.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 25 canonical work pages

[1]

Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dan Mane, Rajat Monga, Sherry Moore, Derek Murray, Chr...

arXiv doi:10.48550/arxiv.1603.04467 2016
[2]

Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023)

arXiv 2023
[3]

Matej Balog, Alexander L Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2016. Deepcoder: Learning to write programs. arXiv preprint arXiv:1611.01989 (2016)

arXiv 2016
[4]

Shraddha Barke, Emmanuel Anaya Gonzalez, Saketh Ram Kasibatla, Taylor Berg-Kirkpatrick, and Nadia Polikarpova

work page
[5]

Rohan Bavishi, Caroline Lemieux, Roy Fox, Koushik Sen, and Ion Stoica. 2019. AutoPandas: neural-backed generators for program synthesis. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1–27

work page 2019
[6]

Sahil Bhatia, Jie Qiu, Sanjit A Seshia, and Alvin Cheung. 2024. Can LLMs Perform Verified Lifting of Code? Technical Report (2024)

work page 2024
[7]

James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http://github.com/google/jax

2018
[8]

Alexander Brauckmann, Elizabeth Polgreen, Tobias Grosser, and Michael FP O’Boyle. 2023. mlirSynth: Automatic, Retargetable Program Raising in Multi-Level IR using Program Synthesis. In 2023 32nd International Conference on Parallel Architectures and Compilation Techniques (PACT). IEEE, 39–50

work page 2023

Show all 40 references

[9]

Xinyun Chen, Chang Liu, and Dawn Song. 2018. Tree-to-Tree Neural Networks for Program Translation. InProceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada) (NIPS’18). Curran Associates Inc., Red Hook, NY, USA, 2552–2562

2018
[10]

Joao PL De Carvalho, Braedy Kuzma, Ivan Korostelev, José Nelson Amaral, Christopher Barton, José Moreira, and Guido Araujo. 2021. KernelFaRer: replacing native-code idioms with high-performance library calls. ACM Transactions On Architecture And Code Optimization (TACO) 18, 3 ...

2021
[11]

Mehdi Drissi, Olivia Watkins, Aditya Khant, Vivaswat Ojha, Pedro Sandoval, Rakia Segev, Eric Weiner, and Robert Keller. 2018. Program Language Translation Using a Grammar-Driven Tree-to-Tree Model. ICML (2018)

2018
[12]

Björn Franke and Michael O’boyle. 2003. Array recovery and high-level transformations for DSP applications. ACM Transactions on Embedded Computing Systems (TECS) 2, 2 (2003), 132–162

2003
[13]

Philip Ginsbach, Bruce Collie, and Michael FP O’Boyle. 2020. Automatically harnessing sparse acceleration. In Proceedings of the 29th International Conference on Compiler Construction . 179–190

2020
[14]

Awni Hannun, Jagrit Digani, Angelos Katharopoulos, and Ronan Collobert. 2023. MLX: Efficient and flexible machine learning on Apple silicon. https://github.com/ml-explore

2023
[15]

Charles R Harris, K Jarrod Millman, Stéfan J Van Der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J Smith, et al. 2020. Array programming with NumPy. Nature 585, 7825 (2020), 357–362

2020
[16]

Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama. 2016. Verified lifting of stencil computations. SIGPLAN Not. 51, 6 (2016), 711–726. doi:10.1145/2980983.2908117

2016
[17]

Fredrik Kjolstad, Stephen Chou, David Lugato, Shoaib Kamil, and Saman Amarasinghe. 2017. Taco: A tool to generate tensor algebra kernels. In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) . 943–948. doi:10.1109/ASE.2017.8115709

2017
[18]

Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, and Saman Amarasinghe. 2017. The Tensor Algebra Compiler. OOPSLA (2017)

2017
[19]

Daniel Kroening and Michael Tautsching. 2014. CBMC — C Bounded Model Checker.TACAS 2014 8413 (2014), 389–391

2014
[20]

Avery Laird, Bangtian Liu, Nikolaj Bjørner, and Maryam Mehri Dehnavi. 2024. SpEQ: Translation of Sparse Codes using Equivalences. Proc. ACM Program. Lang. 8, PLDI, Article 215 (June 2024), 24 pages. doi:10.1145/3656445

2024 doi
[21]

Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2020. MLIR: A compiler infrastructure for the end of Moore’s law. arXiv preprint arXiv:2002.11054 (2020). Proc. AC...

2020 arXiv
[22]

Woosuk Lee, Kihong Heo, Rajeev Alur, and Mayur Naik. 2018. Accelerating search-based program synthesis using learned probabilistic models. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI 2018). A...

2018
[23]

Woosuk Lee, Kihong Heo, Rajeev Alur, and Mayur Naik. 2018. Accelerating search-based program synthesis using learned probabilistic models. ACM SIGPLAN Notices 53, 4 (2018), 436–449

2018
[24]

Yixuan Li, Julian Parsert, and Elizabeth Polgreen. 2024. Guiding Enumerative Program Synthesis with Large Language Models. In Computer Aided Verification (Montreal, Canada) (CA V 2024). Springer Nature Switzerland, Cham, 280–301. doi:10.1007/978-3-031-65630-9_15

2024 doi
[25]

llamacpp

llama 2024. llamacpp. https://github.com/leloykun/llama2.cpp/. Accessed: 2024-01-19

2024
[26]

José Wesley de Souza Magalhães, Jackson Woodruff, Elizabeth Polgreen, and Michael F. P. O’Boyle. 2023. C2TACO: Lifting Tensor Code to TACO. In Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (Cascais, Portugal) (...

2023
[27]

Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig. 2022. Automated transpilation of imperative to functional code using neural-guided program synthesis. Proc. ACM Program. Lang. 6, OOPSLA1, Article 71 (April 2022), 27 pages. doi:10.1145/3527315

2022 doi
[28]

Pablo Antonio Martínez, Jackson Woodruff, Jordi Armengol-Estapé, Gregorio Bernabé, José Manuel García, and Michael FP O’Boyle. 2023. Matching linear algebra and tensor code to specialized hardware accelerators. InProceedings of the 32nd ACM SIGPLAN International Conference on ...

2023
[29]

Daye Nam, Baishakhi Ray, Seohyun Kim, Xianshan Qu, and Satish Chandra. 2022. Predictive synthesis of api-centric code. In Proceedings of the 6th ACM SIGPLAN International Symposium on Machine Programming . 40–49

2022
[30]

Maxwell Nye, Luke Hewitt, Joshua Tenenbaum, and Armando Solar-Lezama. 2019. Learning to infer program sketches. In International Conference on Machine Learning . PMLR, 4861–4870

2019
[31]

Michael FP O’Boyle and Peter MW Knijnenburg. 2002. Integrating loop and data transformations for global optimization. J. Parallel and Distrib. Comput. 62, 4 (2002), 563–590

2002
[32]

Augustus Odena, Kensen Shi, David Bieber, Rishabh Singh, Charles Sutton, and Hanjun Dai. 2020. Bustle: Bottom-up program synthesis through learning-guided exploration. arXiv preprint arXiv:2007.14381 (2020)

2020 arXiv
[33]

Theo X Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. 2023. Is Self-Repair a Silver Bullet for Code Generation?. In The Twelfth International Conference on Learning Representations

2023
[34]

Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu ...

2019
[35]

Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit Seshia, and Alvin Cheung. 2024. Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations. ECOOP (2024)

2024
[36]

Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A Seshia, and Alvin Cheung. 2024. Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations. In 38th European Conference on Object-Oriented Programming (ECOOP 2024)

2024
[37]

Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman Amarasinghe. 2013. Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. Acm Sigplan Notices 48, 6 (2013), 519–530

2013
[38]

Kensen Shi, David Bieber, and Rishabh Singh. 2022. Tf-coder: Program synthesis for tensor manipulations. ACM Transactions on Programming Languages and Systems (TOPLAS) 44, 2 (2022), 1–36

2022
[39]

Kensen Shi, Hanjun Dai, Kevin Ellis, and Charles Sutton. 2022. CrossBeam: Learning to search in bottom-up program synthesis. arXiv preprint arXiv:2203.10452 (2022). Received 2024-11-15; accepted 2025-03-06 Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article 227. Publication da...

2022 arXiv
[2024]

arXiv preprint arXiv:2405.15880 (2024)

HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis. arXiv preprint arXiv:2405.15880 (2024). doi:10.48550/arXiv.2405.15880

2024 doi arXiv

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [1]

Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dan Mane, Rajat Monga, Sherry Moore, Derek Murray, Chr...

arXiv doi:10.48550/arxiv.1603.04467 2016

[2] [2]

Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023)

arXiv 2023

[3] [3]

Matej Balog, Alexander L Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2016. Deepcoder: Learning to write programs. arXiv preprint arXiv:1611.01989 (2016)

arXiv 2016

[4] [4]

Shraddha Barke, Emmanuel Anaya Gonzalez, Saketh Ram Kasibatla, Taylor Berg-Kirkpatrick, and Nadia Polikarpova

work page

[5] [5]

Rohan Bavishi, Caroline Lemieux, Roy Fox, Koushik Sen, and Ion Stoica. 2019. AutoPandas: neural-backed generators for program synthesis. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1–27

work page 2019

[6] [6]

Sahil Bhatia, Jie Qiu, Sanjit A Seshia, and Alvin Cheung. 2024. Can LLMs Perform Verified Lifting of Code? Technical Report (2024)

work page 2024

[7] [7]

James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http://github.com/google/jax

2018

[8] [8]

Alexander Brauckmann, Elizabeth Polgreen, Tobias Grosser, and Michael FP O’Boyle. 2023. mlirSynth: Automatic, Retargetable Program Raising in Multi-Level IR using Program Synthesis. In 2023 32nd International Conference on Parallel Architectures and Compilation Techniques (PACT). IEEE, 39–50

work page 2023