An Automated Theorem Proving Framework for Information-Theoretic Results

TL;DR

This paper introduces a unified automated theorem proving framework that can discover, simplify, and prove bounds and properties in network information theory, including non-Shannon inequalities, demonstrating success on numerous classical theorems.

Contribution

The paper presents a novel, unified framework based on existential information inequalities for automated theorem proving in information theory, capable of handling diverse problems and discovering new inequalities.

Findings

Successfully proved 32 out of 56 theorems from key information theory chapters.

Able to derive properties of information-theoretic quantities like common information.

Discovered non-Shannon-type inequalities using the framework.

Abstract

We present a versatile automated theorem proving framework capable of automated discovery, simplification and proofs of inner and outer bounds in network information theory, deduction of properties of information-theoretic quantities (e.g. Wyner and G\'acs-K\"orner common information), and discovery of non-Shannon-type inequalities, under a unified framework. Our implementation successfully generated proofs for 32 out of 56 theorems in Chapters 1-14 of the book Network Information Theory by El Gamal and Kim. Our framework is based on the concept of existential information inequalities, which provides an axiomatic framework for a wide range of problems in information theory.