Smoothing a program soundly and robustly

Abstract. We study the foundations of smooth interpretation, a recently-proposed program approximation scheme that facilitates the use of local numerical search techniques (e.g., gradient descent) in program analy-sis and synthesis. While the popular techniques for local optimization works well only on relatively smooth functions, functions encoded by real-world programs are infested with discontinuities and local irregular features. Smooth interpretation attenuates such features by taking the convolution of the program with a Gaussian function, effectively replac-ing discontinuous switches in the program by continuous transitions. In doing so, it extends to programs the notion of Gaussian smoothing, a popular signal-processing technique used to filter noise and discontinu-ities from signals. Exact Gaussian smoothing of programs is undecidable, so algorithmic im-plementations of smooth interpretation must necessarily be approximate. In this paper, we characterize the approximations carried out by such algorithms. First, we identify three correctness properties—soundness, robustness, and β-robustness—that an approximate smooth interpreter should satisfy. In particular, a smooth interpreter is sound if it computes an abstraction of a program’s “smoothed ” semantics, and robust if it has arbitrary-order derivatives in the input variables at every point in its input space. Second, we describe the design of an approximate smooth interpreter that provably satisfies these properties. The interpreter com-bines program abstraction using a new domain with symbolic calculation of convolution.