There’s a new ecosystem of applications that integrates machine learning into a variety of tasks. Typical domains have included image recognition and natural language processing. However, these techniques have also spread to computer systems domains, such as program compilation, resource scheduling, and database query optimization, yielding new computer systems that learn from data to achieve their goals.

With the success of these systems, we must grapple with the reality that they model and compute with objects that are inherently approximate — real numbers (only computable up to a given precision), neural networks (only validated on a given dataset), and probabilistic computations (results only computable up to a given probability). This reality presents many engineering questions about interpreting, debugging, validating, verifying, and optimizing these systems.

As an illustrative example of such a system, I’ll present Ithemal, our deep learning system for performance modeling of modern computer processors. Using data and simple models, our system predicts the performance of assembly code on modern Intel CPUs better than state-of-the-art, handcrafted techniques from LLVM and Intel.

Guided by Ithemal’s engineering challenges, I’ll present our work on reasoning about the semantics and performance of such a system.

In particular, I’ll present our results on the semantics of sound real-valued, differentiable, probabilistic computation, which is the core computational model behind this new class of systems.  I’ll also present our work on the Lottery Ticket Hypothesis, a set of techniques for producing small trainable neural networks that are 10-20% of the size of standard architectures. The promise of this latter work is not only faster inference and training, but also smaller neural networks that are more amenable to reasoning, such as verifying their robustness