Concrete Type Inference for Code Optimization using Machine Learning with SMT S...
summary
Introduces a hybrid pipeline that feeds GPT-4 style ML predictions into an SMT solver (CVC5) with a lexicographic scoring constraint to produce a bounded set of concrete type assignments; ML alone makes many inconsistent combos and SMT alone yields too many solutions, so the combination reduces candidates to a manageable set (up to 186 versions for a benchmark, with fallback to untyped). Uses multiversion code generation and dispatch; reports geometric-mean speedups of 26.4× with Numba and 62.2× with Intrepydd.
AI-written summary · about
chapters (9)
- 0:00Concrete type inference intro
- 1:45Python perf for domain experts
- 3:17Concrete types in optimization
- 5:51Limitations of prior approaches
- 8:00ML predictions with SMT solvers
- 10:31Refining type predictions
- 13:20Performance gains from inference
- 14:26Summary and future work
- 15:29Q&A
related talks
35mThe Mastermind behind Refinement Types
30mConstrained generation of well-typed programs
33mSolving constraints during type inference
56mOn Type-Based Techniques for Program Manipulation
23mA Type Inferencer for ML in 200 Lines of Scala
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
22mMulti-level Machine Learning-Guided Autotuning for Efficient Code Generation on a Deep(…)
15mTaming Type Annotations in Gradual Typing