Generating compiler optimizations from proofs

We present an automated technique for generating compiler op-timizations from examples of concrete programs before and after improvements have been made to them. The key technical insight of our technique is that a proof of equivalence between the original and transformed concrete programs informs us which aspects of the programs are important and which can be discarded. Our technique therefore uses these proofs, which can be produced by translation validation or a proof-carrying compiler, as a guide to generalize the original and transformed programs into broadly applicable op-timization rules. We present a category-theoretic formalization of our proof gen-eralization technique. This abstraction makes our technique appli-cable to logics besides our own. In particular, we demonstrate how our technique can also be used to learn query optimizations for re-lational databases or to aid programmers in debugging type errors. Finally, we show experimentally that our technique enables pro-grammers to train a compiler with application-specific optimiza-tions by providing concrete examples of original programs and the desired transformed programs. We also show how it enables a com-piler to learn efficient-to-run optimizations from expensive-to-run super-optimizers