TY - GEN
T1 - Automated Reasoning by Convex Optimization
T2 - 54th Annual Conference on Information Sciences and Systems, CISS 2020
AU - Tan, Chee Wei
AU - Ling, Lin
N1 - Full text of this publication does not contain sufficient affiliation information. With consent from the author(s) concerned, the Research Unit(s) information for this record is based on the existing academic department affiliation of the author(s).
PY - 2020/3
Y1 - 2020/3
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85085247742
UR - https://www.scopus.com/record/pubmetrics.uri?eid=2-s2.0-85085247742&origin=recordpage
U2 - 10.1109/CISS48834.2020.1570627814
DO - 10.1109/CISS48834.2020.1570627814
M3 - RGC 32 - Refereed conference paper (with host publication)
SN - 9781728140841
T3 - Annual Conference on Information Sciences and Systems
BT - 2020 54th Annual Conference on Information Sciences and Systems (CISS)
PB - IEEE
Y2 - 18 March 2020 through 20 March 2020
ER -