用符号计算证明信息不等式和恒等式
Proving Information Inequalities and Identities with Symbolic Computation
摘要：
证明Shannon信息测度的线性不等式和恒等式（可能带有线性约束）是信息论中的一个重要问题。为此，ITIP和其他变体算法已经开发和实现，这都是基于解决线性规划（LP）。具体地，通过求解两个LP来验证身份$f = 0$，一个LP用于$f \ge 0$，一个LP用于$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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
