一句话：提出结合机器学习与 SMT 求解的具体类型推断，无需类型标注即可优化动态类型 Python 代码。
动态类型语言（如 Python）因缺乏具体类型信息而难以优化，现有 AOT 优化编译器通常依赖程序员提供可选类型标注，但多数程序并未获得优化。本文提出一种面向代码优化的具体类型推断方法，无需程序员提供类型信息，并探索三类算法：基于 GPT-4 等机器学习模型的推断、基于 SMT 求解的约束推断，以及二者结合。推断结果用于为有限的具体类型选项生成多版本代码，同时保留兜底的无类型版本，使类型化版本可被优化。实验表明，结合算法在精度和性能上远优于单独方法；以 Numba 为 AOT 优化后端时，相较标准 Python 的几何平均加速为 26.4×，以 Intrepydd 优化编译器为后端时达 62.2×，显著减少计算与能耗。
Despite the widespread popularity of dynamically typed languages such as Python, it is well known that they pose significant challenges to code optimization due to the lack of concrete type information. To overcome this limitation, many ahead-of-time optimizing compiler approaches for Python rely on programmers to provide optional type information as a prerequisite for extensive code optimization. Since few programmers provide this information, a large majority of Python applications are executed without the benefit of code optimization, thereby contributing collectively to a significant worldwide wastage of compute and energy resources. In this paper, we introduce a new approach to concrete type inference that is shown to be effective in enabling code optimization for dynamically typed languages, without requiring the programmer to provide any type information. We explore three kinds of type inference algorithms in our approach based on: 1) machine learning models including GPT-4, 2) constraint-based inference based on SMT solving, and 3) a combination of 1) and 2). Our approach then uses the output from type inference to generate multi-version code for a bounded number of concrete type options, while also including a catch-all untyped version for the case when no match is found. The typed versions are then amenable to code optimization. Experimental results show that the combined algorithm in 3) delivers far superior precision and performance than the separate algorithms for 1) and 2). The performance improvement due to type inference, in terms of geometric mean speedup across all benchmarks compared to standard Python, when using 3) is 26.4× with Numba as an AOT optimizing back-end and 62.2× with the Intrepydd optimizing compiler as a back-end. These vast performance improvements can have a significant impact on programmers’ productivity, while also reducing their applications’ use of compute and energy resources.
@article{paperbot1849,
title = {Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving},
author = {Fangke Ye and Jisheng Zhao and Jun Shirako and Vivek Sarkar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622825}
}