Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

VeriLocc: End-to-End Cross-Architecture Register Allocation via LLM

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read A fine-tuned 7B LLM turns GPU register allocation into a verifiable translation task, hitting 85-99% single-shot pass rates across NVIDIA and AMD and beating a vendor BLAS library by 11.6% in one case.

desk verdict VeriLocc is a genuinely new integration of LLM translation, static normalization, and a verifier loop for register allocation, but its correctness claims rest on a verifier whose soundness is taken on faith. read the letter →

arxiv 2506.17506 v1 pith:C4U6LMZS submitted 2025-06-20 cs.CL cs.OS

Lesheng Jin , Zhenyuan Ruan , Haohui Mai , Jingbo Shang This is my paper
classification cs.CLcs.OS
keywords registerallocationlargelanguagemodelsGPUcompilersSMTverificationMIRnormalizationcross-architecturegeneralizationGEMMkernelsmulti-headattention
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

This paper tries to establish that register allocation, an NP-complete compiler step that maps virtual values to physical registers, can be recast as a sequence-to-sequence translation task for a fine-tuned LLM. It argues that combining static normalization of machine IR with a formal SMT verifier makes LLM-generated allocations both correct and generalizable across GPU vendors. A 7B model reaches 85-99% single-shot correctness and near-100% correctness within 100 attempts on GEMM and attention kernels, with the verifier resampling on failures. The paper claims this approach can even discover register assignments that outperform expert-tuned vendor libraries, reporting an 11.6% runtime gain over rocBLAS on an AMD MI250x GPU.

What carries the argument

The core mechanism is a three-stage pipeline. First, static analysis normalizes vendor MIR and ISA into a compact shared dialect, cutting token counts by 80-90% (from roughly 1,200-51,000 tokens down to 113-8,955), and reconstructs NVIDIA training labels by matching SSA-form basic blocks between MIR and assembled code. Second, an autoregressive decoder-only LLM (Qwen2.5-Coder-7B-Instruct) generates register mappings as structured JSON dictionaries. Third, a Z3 SMT verifier checks consistency, liveness safety, and hardware realizability, and the model resamples until the verifier accepts a candidate, making the output sound enough for compiler integration.

What would settle it

Feed the Z3 verifier a deliberately wrong allocation that it accepts (for example, two values with overlapping lifetimes sharing a register across a control-flow join), then assemble and run the kernel: if the toolchain emits the binary and the kernel writes incorrect results, the soundness premise is false and all reported metrics rest on an unsound base.

Watch

Extended reading notes

Core claim

The paper claims that LLMs can learn register allocation as an end-to-end mapping from normalized machine IR to JSON-style physical-register assignments, and that pairing this learned mapping with a Z3-based verifier yields both correctness and cross-architecture generalization. On GEMM and MHA kernels from the NVIDIA RTX 4090 and AMD MI250x, the fine-tuned 7B model attains 85-99% single-shot pass rates and near-100% pass@100, with an average of under 10 attempts before a valid allocation is found. In a case study, VeriLocc discovers an allocation that uses the CDNA2 Accumulation VGPRs more aggressively than rocBLAS and runs 11.6% faster.

Load-bearing premise

The central claim collapses if the SMT encoding does not fully model every register-allocation constraint for both ISAs; the paper adopts this soundness property from prior work rather than proving or empirically validating it here, so one accepted-but-invalid assignment would invalidate every pass-rate and speedup conclusion.

Editorial extensions

If this is right

  • Register allocation can be treated as a data-driven translation problem rather than a hand-tuned heuristic, so retargeting to a new GPU generation becomes a matter of retraining on normalized data instead of re-engineering allocation passes.
  • The verifier-guided resampling loop filters invalid LLM outputs before code emission, which is what makes learned allocations safe enough to feed into production compiler toolchains.
  • Normalization lets one model train on heterogeneous toolchains simultaneously; the Mixed-setting results (98% GEMM and 85.8% MHA single-shot pass rates) show transferable allocation patterns across ISAs.
  • The 11.6% improvement over rocBLAS on MI250x suggests learned allocators can find microarchitecturally better assignments than expert-written libraries, not merely match them.
  • The failure of a 3B model on MHA kernels indicates a capability threshold: harder, longer kernels with complex dependencies require the larger 7B scale.

Reading between the lines

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

  • If the verifier's soundness holds, the same learned-proposal-plus-formal-check recipe could extend to other NP-hard compiler phases such as instruction scheduling or bank-conflict avoidance, provided a certifying checker exists for those problems.
  • The AccVGPR result is a testable hypothesis: a microbenchmark measuring access latency of Accumulation VGPRs versus general VGPRs on CDNA2 would settle whether the documented 'no performance difference' is wrong at the microarchitecture level.
  • Feeding verifier outcomes back into training (for example, as a reinforcement-learning reward) could push single-shot accuracy well above 99%, shrinking the resampling latency that the paper identifies as the main deployment cost.
  • The NVIDIA training labels are reconstructed by SSA matching rather than read from the toolchain itself; auditing those labels against the actual allocator would determine whether any silently wrong assignments are being taught to the model.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper proposes VeriLocc, a framework that fine-tunes a 7B LLM to perform GPU register allocation as a sequence-to-sequence translation from a normalized machine intermediate representation (MIR) to JSON-style virtual-to-physical register mappings. A static-analysis component normalizes MIRs from NVIDIA and AMD toolchains, and a Z3-based verifier validates generated allocations for consistency, safety, and hardware realizability, with a resampling loop on failure. The authors evaluate on GEMM and MHA kernels for RTX 4090 and MI250x, reporting 85–99% single-shot pass rates and near-100% pass@100 in most settings, and present a case study where the generated GEMM kernel outperforms rocBLAS by 11.6% on MI250x.

Significance. If the results hold, the paper makes a useful empirical contribution: it demonstrates that a reasonably sized LLM, combined with MIR normalization and verifier-guided resampling, can produce correct register allocations across two GPU ISA families, and it ships reproducible code (public GitHub) and a clearly defined pass-rate metric with an external SMT-based correctness check. The normalization technique and the error analysis are also informative for the compiler+ML community. The significance is tempered by the fact that all correctness claims depend on the precision of the Z3 encoding, which is cited from prior work rather than validated here, and the headline performance claim rests on a single benchmark without statistical detail.

major comments (3)
  1. [§3.4 and §5] The correctness guarantee of the entire framework rests on the Z3 verifier of §3.4, yet the paper neither proves nor tests the precision of the encoding. The related-work sentence in §5 defines 'sound static analysis' as 'no false negative,' but the required property is the absence of false accepts: an invalid allocation that Z3 approves would make every pass rate in Table 2 and the runtime advantage in §4.7 meaningless. Please specify the exact SMT encoding for ISA-specific constraints (e.g., CDNA2 AccVGPR access restrictions, 64-bit VGPR alignment), provide a validation suite of deliberately invalid allocations that the verifier must reject for both NVIDIA and AMD, and add an end-to-end numerical correctness check for at least the case-study kernel.
  2. [§3.2.1] The NVIDIA training labels are reconstructed by the heuristic SSA-based analysis described in §3.2.1, but the paper provides no validation that these reconstructions are correct. If the reconstruction heuristic misidentifies mappings because of instruction-lowering differences, the model is trained on incorrect supervision. Pass rates are measured against the verifier rather than the labels, but the quality of the fine-tuned model and the case-study performance depend on this data. Please report a validation of reconstruction accuracy, for example by comparing reconstructed mappings against compiler-internal allocation results where available or by executing the reconstructed allocations.
  3. [§4.7 and Table 2] The 11.6% runtime improvement over rocBLAS is presented as a key result but is based on a single GEMM shape, with no confidence intervals or repeated-run variance reported, and the paper itself states that the performance difference is unexpected from the ISA documentation. The claim would be much stronger if the authors reported multiple independent runs, hardware variability, and a numerical equivalence check for the generated kernel to rule out a timing artifact of a functionally incorrect allocation.
minor comments (5)
  1. [§1] The phrase 'sequence-to-sequence (seq2seq) translation task (Sutskever et al., 2014) task' contains a duplicated word; please fix.
  2. [Abstract and §4.3] The abstract claims 'near-100% pass@100,' but Table 2 reports Mixed MHA pass@100 of 89.76%; please qualify the claim to avoid overstatement.
  3. [§4.2] The sentence 'One server with equipped with 500GB SSD...' has a grammatical error, and the description of 'the average of 100 runs' should state whether these are 100 independent kernel launches or 100 repetitions of the same launch.
  4. [Figure 1] Figure 1 is very dense; the normalized MIR and mapping examples are not legible at normal print size. Consider enlarging the example panels or moving them to an appendix.
  5. [Appendix B] The footnote marker after 'ChatGPT’s behavior' has no corresponding footnote text.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: pass rates are checked by an external Z3 verifier and runtime by rocBLAS; the sole self-citation is not load-bearing.

full rationale

The paper's central claims do not reduce to their inputs by construction. Training labels are reconstructed from toolchain outputs, but single-shot and pass@100 rates are measured on held-out test cases against a Z3 SMT verifier described in Section 3.4 (consistency, safety, realizability), and the runtime case study is an external comparison against rocBLAS on MI250x hardware. The 11.6% speedup is an empirical measurement, not a fitted prediction. The only self-citation is the Related Work statement that VeriLocc "uses sound static analysis (Mai et al., 2023)", where Mai is a co-author; that citation is not used to derive the verifier's encoding, which is presented as a constructed SMT problem, so it is a minor dependency rather than a circular reduction. One correctness risk (not circularity) should be weighed: the paper calls the analysis "sound ... i.e., no false negative" (Section 5) while the required guarantee for a verifier is no false accepts, and no negative tests or end-to-end numerical execution checks of accepted kernels are reported; this affects confidence in the verifier's precision but does not make the LLM pass-rate or rocBLAS comparison circular.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

No hand-fitted constants appear in the method; the central dependencies are the pretrained LLM backbone and the assumption that the Z3 encoding is a sound model of register allocation constraints. The fine-tuning weights are learned from data, so they are not ledger entries in the same sense as fitted physical constants.

assumptions (2)
  • domain assumption The Z3-based SMT encoding correctly models register allocation constraints (consistency, liveness safety, hardware realizability) for both NVIDIA and AMD ISAs.
    Section 3.4 states the verifier validates these properties but does not prove the encoding; the paper cites Mai et al. (2023) for soundness, which is an external dependency.
  • domain assumption The pretrained Qwen2.5-Coder-7B-Instruct model provides sufficient base reasoning ability that fine-tuning on normalized MIR-to-mapping pairs yields a useful allocator.
    The paper uses this backbone without exploring alternatives or ablating the pretrained component; the 3B model's failure on MHA shows scale matters.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VeriLocc: End-to-End Cross-Architecture Register Allocation via LLM." pith.science (2026). https://pith.science/paper/C4U6LMZS

@misc{pith2026250617506,
  author       = {Pith},
  title        = {Pith review of: VeriLocc: End-to-End Cross-Architecture Register Allocation via LLM},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/C4U6LMZS}},
  note         = {Machine review of arXiv:2506.17506}
}
read the original abstract

Modern GPUs evolve rapidly, yet production compilers still rely on hand-crafted register allocation heuristics that require substantial re-tuning for each hardware generation. We introduce VeriLocc, a framework that combines large language models (LLMs) with formal compiler techniques to enable generalizable and verifiable register allocation across GPU architectures. VeriLocc fine-tunes an LLM to translate intermediate representations (MIRs) into target-specific register assignments, aided by static analysis for cross-architecture normalization and generalization and a verifier-guided regeneration loop to ensure correctness. Evaluated on matrix multiplication (GEMM) and multi-head attention (MHA), VeriLocc achieves 85-99% single-shot accuracy and near-100% pass@100. Case study shows that VeriLocc discovers more performant assignments than expert-tuned libraries, outperforming rocBLAS by over 10% in runtime.

Figures

Figures reproduced from arXiv: 2506.17506 by the authors.

Figure 1
Figure 1. Overall training and inference workflow of [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Error Distributions of VERILOCC on MHA under Different Settings. imum attempts typically falling within 100 to 200. Overall, VERILOCC works very well in the both the Same-NV / Same-AMD settings. While the Mixed setting is more challenging, VERILOCC still generalizes well. This indicates that LLMs can learn transferable patterns in register allocation across different ISAs. 4.4 Ablation on MIR Normalization The MIR n… view at source ↗
Figure 3
Figure 3. Allocation Result from ChatGPT 1 https://chatgpt.com/share/682a07f9-bf50-8006- a7ac-f07b439439e4 11 [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. PreScience: A Dataset and Benchmark for Scientific Forecasting

    cs.AI 2026-02 conditional novelty 6.0 of 10

    A new benchmark tests whether AI can forecast future scientific papers; frontier LLMs score ~5.6/10 on matching real abstracts, and simulated corpora are measurably less diverse and novel than human science.

Reference graph

Works this paper leans on

43 extracted references · 24 canonical work pages · cited by 1 Pith paper

  1. [1]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block STRING...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    V Aho Alfred, S Lam Monica, and D Ullman Jeffrey. 2007. Compilers principles, techniques & tools. pearson Education

    2007

  4. [4]

    AMD Inc. 2022. Amd instinct mi200 instruction set architecture. https://www.amd.com/content/dam/amd/en/documents/instinct-tech-docs/instruction-set-architectures/instinct-mi200-cdna2-instruction-set-architecture.pdf

    work page 2022

  5. [5]

    AMD Inc. 2024 a . rocBLAS : Rocm basic linear algebra subprograms (blas) library. https://github.com/ROCm/rocBLAS. Accessed: 2024-05-01

    work page 2024

  6. [6]

    AMD Inc. 2024 b . Rocm compiler and programming model documentation. https://rocm.docs.amd.com

    work page 2024

  7. [7]

    Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. 2015. Neural machine translation by jointly learning to align and translate. In International Conference on Learning Representations (ICLR)

    work page 2015

  8. [8]

    Gianfranco Bilardi and Keshav Pingali. 2003. https://doi.org/10.1145/765568.765573 Algorithms for computing the static single assignment form . J. ACM, 50(3):375--425

    work page arXiv 2003

Show all 43 references
  1. [9]

    Chaitin, Marc A

    Gregory J. Chaitin, Marc A. Auslander, Ashok K. Chandra, John Cocke, Martin E. Hopkins, and Peter W. Markstein. 1981. Register allocation via coloring. Comput. Lang., 6(1):47--57

    1981

  2. [10]

    Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Haichen Shen, Meghan Cowan, Leyuan Wang, Yuwei Hu, Luis Ceze, and 1 others. 2018. TVM : An automated End-to-End optimizing compiler for deep learning. In 13th USENIX Symposium on Operating Systems Design and ...

    2018

  3. [11]

    Yundi Chen, Hanrui Wei, William Yu, Haonan Zhao, Yao Zhao, and Hanjun Yang. 2021. Mlgo: a machine learning guided compiler optimization framework. In NeurIPS

    2021

  4. [12]

    Fu, Stefano Ermon, Atri Rudra, and Christopher R\' e

    Tri Dao, Daniel Y. Fu, Stefano Ermon, Atri Rudra, and Christopher R\' e . 2022. Flashattention: fast and memory-efficient exact attention with io-awareness. In Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS '22, Red Hook, NY, US...

    2022

  5. [13]

    Leonardo De Moura and Nikolaj Bj rner. 2008. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, pages 337--340, Berlin, Heide...

    2008

  6. [14]

    Xiaofeng Guan, Hao Zhou, Guoqing Bao, Handong Li, Liang Zhu, and Jianguo Yao. 2024. https://doi.org/10.1109/CGO57630.2024.10444841 Prescount: Effective register allocation for bank conflict reduction . In 2024 IEEE/ACM International Symposium on Code Generation and Optimizatio...

    2024

  7. [15]

    Cheng-Ping Hsieh, Simeng Sun, Samuel Kriman, Shantanu Acharya, Dima Rekesh, Fei Jia, and Boris Ginsburg. 2024. https://openreview.net/forum?id=kIoBbc76Sy RULER : What s the real context size of your long-context language models? In First Conference on Language Modeling

    2024

  8. [16]

    Norman P. Jouppi, Cliff Young, Nishant Patil, David Patterson, Gaurav Agrawal, Raminder Bajwa, Sarah Bates, Suresh Bhatia, Nan Boden, Al Borchers, Rick Boyle, Pierre-luc Cantin, Clifford Chao, Chris Clark, Jeremy Coriell, Mike Daley, Matt Dau, Jeffrey Dean, Ben Gelb, and 57 ot...

    2017

  9. [17]

    Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, and Saman Amarasinghe. 2017. https://doi.org/10.1145/3133901 The tensor algebra compiler . Proc. ACM Program. Lang., 1(OOPSLA)

    2017 doi

  10. [18]

    Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. 2012. Imagenet classification with deep convolutional neural networks. Advances in neural information processing systems, 25

    2012

  11. [19]

    Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica. 2023. https://doi.org/10.1145/3600006.3613165 Efficient memory management for large language model serving with pagedattention . In Proceedings of the 29...

    2023

  12. [20]

    Chris Lattner and Vikram Adve. 2004. Llvm: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization, CGO '04, page 75, USA. IEEE Compute...

    2004

  13. [21]

    Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2021. https://doi.org/10.1109/CGO51591.2021.9370308 MLIR : Scaling compiler infrastructure for domain specific com...

    2021

  14. [22]

    Chris Lattner, Andrew Lenharth, and Vikram Adve. 2007. https://doi.org/10.1145/1250734.1250766 Making context-sensitive points-to analysis with heap cloning practical for the real world . In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Impl...

    2007

  15. [23]

    Yijin Li, Jiacheng Zhao, Sun Qianqi, Haohui Mai, Lei Chen, Wanlu Cao, Yanfan Chen, Li zhicheng, YING LIU, Xinyuan Zhang, Xiyu Shi, Jie Zhao, Jingling Xue, Huimin Cui, and XiaoBing Feng. 2023. https://proceedings.mlsys.org/paper_files/paper/2023/file/3e4e24f7e055320fa54c03f6e81...

    2023

  16. [24]

    Liang Liu, Marc Brockschmidt, Vivek Murali, and et al. 2024. The meta llm compiler: A suite of open-source models for code optimization. arXiv preprint arXiv:2407.02524

    2024 arXiv

  17. [25]

    Roberto Casta \ n eda Lozano, Mats Carlsson, Gabriel Hjort Blindell, and Christian Schulte. 2019. Combinatorial register allocation and instruction scheduling. ACM Transactions on Programming Languages and Systems (TOPLAS), 41(3):1--53

    2019

  18. [26]

    Lingxiao Ma, Zhiqiang Xie, Zhi Yang, Jilong Xue, Youshan Miao, Wei Cui, Wenxiang Hu, Fan Yang, Lintao Zhang, and Lidong Zhou. 2020. https://www.usenix.org/conference/osdi20/presentation/ma Rammer: Enabling holistic deep learning compiler optimizations with rTasks . In 14th USE...

    2020

  19. [27]

    HaoHui Mai, Jiacheng Zhao, Hongren Zheng, Yiyang Zhao, Zibin Liu, Mingyu Gao, Cong Wang, Huimin Cui, Xiaobing Feng, and Christos Kozyrakis. 2023. https://www.usenix.org/conference/osdi23/presentation/mai Honeycomb: Secure and efficient GPU executions via static validation . In...

    2023

  20. [28]

    NVIDIA Corporation . 2024. https://docs.nvidia.com/cuda/cuda-compiler-driver-nvcc/ CUDA Toolkit Documentation: Compiler

    2024

  21. [29]

    OpenAI. 2023. Gpt-4 technical report. https://cdn.openai.com/papers/gpt-4.pdf

    2023

  22. [30]

    Massimiliano Poletto and Vivek Sarkar. 1999. https://doi.org/10.1145/330249.330250 Linear scan register allocation . ACM Trans. Program. Lang. Syst., 21(5):895--913

    1999

  23. [31]

    Fernando Magno Quint\ a o Pereira and Jens Palsberg. 2008. https://doi.org/10.1145/1375581.1375609 Register allocation by puzzle solving . In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '08, pages 216--226, New York, N...

    2008

  24. [32]

    Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Fr\' e do Durand, and Saman Amarasinghe. 2013. https://doi.org/10.1145/2491956.2462176 Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines . I...

    2013

  25. [33]

    Ilya Sutskever, Oriol Vinyals, and Quoc V Le. 2014. Sequence to sequence learning with neural networks. In Advances in neural information processing systems, pages 3104--3112

    2014

  26. [34]

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, ukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Advances in neural information processing systems, pages 5998--6008

    2017

  27. [35]

    S VenkataKeerthy, Siddharth Jain, Anilava Kundu, Rohit Aggarwal, Albert Cohen, and Ramakrishna Upadrasta. 2023. Rl4real: Reinforcement learning for register allocation. In Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction, pages 133--144

    2023

  28. [36]

    Yang Wang, Chen Zhang, Zhiqiang Xie, Cong Guo, Yunxin Liu, and Jingwen Leng. 2021. https://doi.org/10.1109/ISCA52012.2021.00088 Dual-side sparse tensor core . In Proceedings of the 48th Annual International Symposium on Computer Architecture, ISCA '21, pages 1083--1095. IEEE Press

    2021

  29. [37]

    Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, and Alex Aiken. 2025. https://arxiv.org/abs/2505.14615 Satbench: Benchmarking llms' logical reasoning via automated puzzle generation from sat formulas . Preprint, arXiv:2505.14615

    2025

  30. [38]

    Mengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi, Jianan Ji, Kit Ao, Praveen Velliengiri, Xupeng Miao, Oded Padon, and Zhihao Jia. 2025. Mirage: A multi-level superoptimizer for tensor programs. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25)

    2025

  31. [39]

    Yichen Xie and Alex Aiken. 2007. https://doi.org/10.1145/1232420.1232423 Saturn: A scalable framework for error detection using boolean satisfiability . ACM Trans. Program. Lang. Syst., 29(3):16--es

    2007

  32. [40]

    An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, Huan Lin, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jingren Zhou, Junyang Lin, Kai Dang, and 23 others. 2025. https://arxiv.org/abs/...

    2025 arXiv

  33. [41]

    Chenggang Zhao, Chengqi Deng, Chong Ruan, Damai Dai, Huazuo Gao, Jiashi Li, Liyue Zhang, Panpan Huang, Shangyan Zhou, Shirong Ma, Wenfeng Liang, Ying He, Yuqing Wang, Yuxuan Liu, and Y. X. Wei. 2025. https://arxiv.org/abs/2505.09343 Insights into deepseek-v3: Scaling challenge...

    2025

  34. [42]

    Gonzalez, and Ion Stoica

    Lianmin Zheng, Chengfan Jia, Minmin Sun, Zhao Wu, Cody Hao Yu, Ameer Haj-Ali, Yida Wang, Jun Yang, Danyang Zhuo, Koushik Sen, Joseph E. Gonzalez, and Ion Stoica. 2020. https://www.usenix.org/conference/osdi20/presentation/zheng Ansor: Generating High-Performance tensor program...

    2020

  35. [43]

    Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph Gonzalez, Clark Barrett, and Ying Sheng. 2024. Sglang: Efficient execution of structured language model programs. In Advances in Neural Informati...

    2024

Pith tools

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