Guided Tensor Lifting

on YouTube ↗19m

" summary

Automatic lifting from C to Taco uses an LLM to generate 10 candidate tensor expressions, extracts a probabilistic grammar from those samples, and drives enumerative synthesis (both a top-down enumerator and a bottom-up variant) with that guidance. Verification runs IO tests and bounded model checking with CBMC/CProver. Results: 99% coverage with the top-down path, up to 12x faster synthesis than prior tools, and example code shows 1.79x multicore and 24.1x GPU speedups over original C.

AI-written summary · about

" chapters (22)

1. 0:00Guided tensor lifting intro
2. 0:23Program lifting & hardware specialization
3. 1:51Automating language lifting
4. 2:56Synthesis challenges & LLM approach
5. 4:21LLM + enumerative search
6. 5:02LLM in pipeline & prompting
7. 6:06Probabilistic grammar & dimensional analysis
8. 7:31Left-hand side tensor determination
9. 8:12Extracting grammar from LLM
10. 9:17Search with star enumeration
11. 10:45Top-down vs bottom-up enumerators
12. 11:47Verification with model checking
13. 12:31Validation step for input-output equivalence
14. 13:15Bounded model checking
15. 14:00Benchmarks & baseline comparisons
16. 15:02Results on coverage & speed
17. 15:46Conclusion & future work
18. 16:07Q&A
19. 16:28Top-down vs bottom-up benefits
20. 17:10Complex examples & limitations
21. 18:17Handling unsolved benchmarks
22. 19:00Closing remarks

" related talks

• 28mC2TACO: Lifting Tensor Code to TACOElizabeth Polgreen, Michael F. P. O'Boyle, Jackson Woodruff · GPCE 2023
• 15mEnabling Tensor Language Model to Assist in Generating High-Performance Tensor...Yu Zhang, Yi Zhai, Sijia Yang, Keyu Pan, Renwei Zhang, Shuo Liu, Chao Liu, Zichun Ye, Jianmin Ji, Jie Zhao, Yanyong Zhang · 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24)
• 24mVerified Tensor-Program Optimization Via High-Level Scheduling RewritesAdam Chlipala, Jonathan Ragan-Kelley, Gilbert Louis Bernstein, Amanda Liu · POPL 2022
• 15mTACCL: Guiding Collective Algorithm Synthesis using Communication SketchesOlli Saarikivi, Rachee Singh, Vijay Chidambaram, Jacob Nelson, Aashaka Shah, Saeed Maleki, Meghan Cowan, Madan Musuvathi, Todd Mytkowicz · NSDI 2023
• 11mQiMeng-Xpiler: Transcompiling Tensor Programs for Deep Learning Systems with a...Qi Guo, Xuehai Zhou, Shouyang Dong, Yuanbo Wen, Jun Bi, Di Huang, Jiaming Guo, Jianxing Xu, Ruibai Xu, Xinkai Song, Yifan Hao, Ling Li, Tianshi Chen, Yunji Chen · OSDI '25
• 28mFunctional Sparse Tensor CompilationAmir Shaikhha, Shideh Hashemian · FProPer 2024
• 22mTileLoom: Automatic Dataflow Planning for Tile-Based Languages on Spatial Dataflow Accel…Wei Li, Cheng Tan, Zhenyu Bai, Heru Wang, Pranav Dangi, Zhiqiang Zhang, Huiying Lan, Weng-Fai Wong, Tulika Mitra · 20th USENIX Symposium on Operating Systems Design and Implementation (OSDI '26)
• 12mCoding Agents for Compiler Construction: Beyond the...Reza Rahimi, Stefan Krassin · PyTorch Conference Europe 2026