Synthesizing Vectorized Code via Verified Lifting
summary
A toolchain translates small, fixed‑size Python loops into vectorized NumPy by unrolling loops, emitting C/C++/LLVM, and using Metalift to synthesize programs from a grammar of NumPy combinators with first‑order specifications checked by an SMT solver. The prototype produces equivalent NumPy code after bounded verification, shows exponential synthesis time with search depth (depth >5 reaches 13 minutes), and finds breadth of supported functions less harmful to performance; scalability and richer tuple sizes remain open.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:39Motivation
- 1:54Goal
- 2:25Problem Definition
- 3:16Approach
- 3:46Why verified lifting?
- 4:17Components
- 5:08Source language fragments
- 6:29Specifications
- 7:21Grammar
- 8:07Implementation workflow
- 9:17Evaluation
- 10:28Future Work
related talks
29mVectorize using linear algebra and NumPy to make your Python code fast
35mVectorization: How slow Python runs fast code
34mNumPy: vectorize your brain
30mHighLoad Python SIMD, GPU, and Horizontal Scaling Looking into Silicon
42mLift your Speed Limits with Cython
37mUsing Numba Effectively Today
25m"Boosting Python Numeric Computations with Dynamic C++ Integration"
27mALPyNA: Acceleration of Loops in Python for Novel Architectures