An Automated Theorem Proving Framework for Information-Theoretic Results

We present a versatile automated theorem proving framework capable of automated proofs of outer bounds in network information theory, automated discovery of inner bounds in network information theory (in conjunction with the method by Lee and Chung), simplification of capacity regions involving auxiliary random variables, automated deduction of properties of information-theoretic quantities (e.g. Wyner and Gács-Körner common information), and automated discovery of non-Shannon-type inequalities, under a unified framework. Our method is based on the linear programming approach for proving Shannon-type information inequalities by Yeung and Zhang, together with a novel pruning method for searching auxiliary random variables. We introduce the concept of existential information inequalities, which provides an axiomatic framework for a wide range of problems in information theory. A full version of this paper is accessible at: https://arxiv.org/pdf/2101.12370.pdf