Solving System Problems with Machine Learning

Over the past decade, Machine Learning (ML) has achieved tremendous successes and has seen wide-scale adoption for human-facing tasks, such as visual recognition, speech recognition, language translation and medical diagnosis. However, going forward, we contend that ML has an even higher potential for impact by solving hard systems problems, such as improving industrial processes, supply chain optimization, and automatic program generation. One challenge is that solving many of these problems require solutions that are provably correct, which is at odds with the ML techniques which are stochastic in nature. In this paper, we consider this challenge and propose two approaches of using ML to solve system problems. The first approach, called correct by construction, is to generate provably correct solutions, for example, by starting from a correct solution, and applying ML-guided transformations that preserve the solution's correctness. The second approach, called trust but verify, is to generate solutions whose correctness can be (efficiently) verified, and then keep generating solutions until we find a correct one. To illustrate these approaches, we present several examples in the area of software systems, and show how using ML can provide significant improvements over state-of-the-art solutions which were refined over decades.