Automated Reasoning by Convex Optimization: Proof Simplicity, Duality and Sparsity

摘要

Hilbert's 24th problem was about a criterion for the simplicity of mathematical proofs, but there can be a variety of plausible criterion for proof simplicity, each leading to a different way to search for proofs. Possibly, the right kind of proof simplicity criterion may even enable computers to prove theorems in the field of artificial intelligence. The premise of this paper is automated reasoning by convex optimization in which optimization-theoretic tools, when viewed in the context of interactive theorem proving, can automate the task of generating insights and reasoning by computers solving specially-crafted convex optimization problems. Optimization-theoretic notions such as duality and recent advances in convex relaxation and regularization methods for sparsity constraints can be exploited to automate proof search in large-scale problems, pushing the limits of knowledge-discovery via mathematical optimization. We summarize the current status of its application to proving or disproving linear inequalities in information theory, and present some open issues in this area.