论文标题
通过符号计算证明信息不平等和身份
Proving Information Inequalities and Identities with Symbolic Computation
论文作者
论文摘要
在信息理论中，证明了香农信息度量的线性不平等和身份，可能对信息度量的线性限制是一个重要的问题。为此，已经开发和实施了ITIP和其他变体算法，这些算法都是基于求解线性程序（LP）的。特别是，通过求解两个lps来验证一个身份$ f = 0 $，一个用于$ f \ ge 0 $，另一个用于$ f \ le 0 $。在本文中，我们开发了一组可以通过符号计算实现的算法。基于这些算法，设计了验证线性信息不等式和身份的程序。与基于LP的算法相比，我们的程序可以产生可验证且无数值错误的分析证明。我们的程序在计算上也更有效。对于受约束的不平等，通过利用问题的代数结构，可以大大减少需要解决的LP的大小。对于身份，而不是解决两个LP，而是可以在很少的计算中直接验证身份。
Proving linear inequalities and identities of Shannon's information measures, possibly with linear constraints on the information measures, is an important problem in information theory. For this purpose, ITIP and other variant algorithms have been developed and implemented, which are all based on solving a linear program (LP). In particular, an identity $f = 0$ is verified by solving two LPs, one for $f \ge 0$ and one for $f \le 0$. In this paper, we develop a set of algorithms that can be implemented by symbolic computation. Based on these algorithms, procedures for verifying linear information inequalities and identities are devised. Compared with LP-based algorithms, our procedures can produce analytical proofs that are both human-verifiable and free of numerical errors. Our procedures are also more efficient computationally. For constrained inequalities, by taking advantage of the algebraic structure of the problem, the size of the LP that needs to be solved can be significantly reduced. For identities, instead of solving two LPs, the identity can be verified directly with very little computation.
