Alhussein Fawzi, PhD: Proving inequalities with deep learning

I will consider in this talk the fundamental problem of searching for proofs of polynomial inequalities, which has applications in control theory, robotics, geometry, combinatorics, and program verification to name a few. While existing proof systems manipulating polynomial inequalities via elementary inference rules are known to be very powerful, searching for proofs remains a major difficulty. I will introduce a deep reinforcement learning framework to search for a dynamic proof within these proof systems, paying particular attention to incorporating inherent symmetries of the problem as an inductive bias. By comparing our approach with powerful and widely-studied linear programming hierarchies based on static proof systems, I will show that the proposed method reduces the size of the linear program by several orders of magnitude while also improving performance. I will finally conclude with general remarks on the emerging field of using machine learning to solve mathematical problems.