Timezone: »

 
Poster
Learning dynamic polynomial proofs
Alhussein Fawzi · Mateusz Malinowski · Hamza Fawzi · Omar Fawzi

Tue Dec 10 05:30 PM -- 07:30 PM (PST) @ East Exhibition Hall B + C #120
in Optimization -- Non-Convex Optimization »

Polynomial inequalities lie at the heart of many mathematical disciplines. In this paper, we consider the fundamental computational task of automatically searching for proofs of polynomial inequalities. We adopt the framework of semi-algebraic proof systems that manipulate polynomial inequalities via elementary inference rules that infer new inequalities from the premises. These proof systems are known to be very powerful, but searching for proofs remains a major difficulty. In this work, we introduce a machine learning based method to search for a dynamic proof within these proof systems. We propose a deep reinforcement learning framework that learns an embedding of the polynomials and guides the choice of inference rules, taking the inherent symmetries of the problem as an inductive bias. We compare our approach with powerful and widely-studied linear programming hierarchies based on static proof systems, and show that our method reduces the size of the linear program by several orders of magnitude while also improving performance. These results hence pave the way towards augmenting powerful and well-studied semi-algebraic proof systems with machine learning guiding strategies for enhancing the expressivity of such proof systems.

Keywords: Optimization -> Non-Convex Optimization · Neuroscience and Cognitive Science -> Reasoning; Optimization -> Combinatorial Optimization; Reinforcement Learning and Plannin

Author Information

Alhussein Fawzi (DeepMind)
Mateusz Malinowski (DeepMind)

Mateusz Malinowski is a research scientist at DeepMind, where he works at the intersection of computer vision, natural language understanding, and deep learning. He was granted PhD (Dr.-Ing.) with the highest honor (summa cum laude) at Max Planck Institute for Informatics in 2017 in computer vision for his pioneering work on visual question answering, where he proposed the task and developed methods that answer questions about the content of images. Prior to this, he graduated with honors from Saarland University in computer science. Before that, he studied computer science at Wroclaw University in Poland.

Hamza Fawzi (University of Cambridge)
Omar Fawzi (ENS Lyon)

Related Events (a corresponding poster, oral, or spotlight)

More from the Same Authors