To Prove or To Disprove: Information Inequalities Prover, Computational Algorithms and Cloud Computing Software

Project: Research

Description

Information theory (Shannon theory) is important to engineered networks as it tells us aset of "physical laws" that all communication or storage systems must obey regardless ofthe design of the system. Information inequalities (Shannon-type inequalities) areimportant to derive these physical laws. They are fundamental in information theory aswell as in other related mathematical subjects, e.g., probability theory. The basis ofsystematically verifying valid information inequalities was crystalized and laid down in a1997 seminal work by R. W. Yeung, in which he developed a linear programmingframework to verify linear information inequalities. This leads to a computer-aidedapproach to verify information inequalities using the Information Theoretic InequalityProver (ITIP), which is a widely-used state-of-the-art software package. Recently, wediscovered that, beyond merely verification of inequalities, this linear programmingframework can be used to explicitly construct an analytic proof of an informationinequality or an analytic counterexample to disprove it if the inequality is not true ingeneral.Unfortunately, there are severe limitations in the ITIP software. Firstly, it cannot handlemany of the large problem settings arising in information theory and network codingproblems (the size of the linear program grows exponentially with the problem size). Forexample, ITIP is not fast enough to solve a problem involving more than 10 randomvariables that is very common in network coding for distributed storage. Secondly, theITIP only verifies an inequality but it does not provide a mathematical proof. A proof orcounterexample is important because it can provide engineers insights to designing anoptimal system. Thirdly, it cannot handle a broader class of information inequalitiesknown as the non-Shannon-type inequalities. Our recent discovery and work thus openthe door to new computational approaches to automate the search for new informationinequalities that are useful to network information theory.We will be leveraging the modern theories and tools of convex optimization anddistributed computation to develop the next-generation ITIP software that can solvelarge-scale problems. To scale up computing, we will exploit optimization decompositiontheory and cloud computing resource allocation optimization to automate the search foran analytic proof or counterexample. We expect the software developed in the project tobe widely used in the information theory community for a long time. The impact of thisproject is even larger on its novelty in Automated Theorem Proving in computer scienceas well as solving challenging practical network applications.

Detail(s)

Project number 9042196 GRF Finished 1/07/15 → 16/12/19

Research areas

• Information Theory,Network Coding,Linear Programming,Algorithms,