arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1707.01656cs.ITmath.IT
收藏

从数值求解的Shannon型不等式中提取解析证明

Extracting analytic proofs from numerically solved Shannon-type Inequalities

Ido B. Gattegno, Haim H. Permuter

摘要:

一类信息不等式,称为香农型不等式(STI),可以通过一个名为ITIP的计算机软件证明。在以前的工作中,我们已经展示了如何利用这种技术,傅立叶-Motzkin消除算法的信息论不等式。在这里,我们提供了一个算法提取信息不等式的\emph{analytic}证明。通过求解一个最优化问题证明了Shannon型不等式。我们将展示如何提取数字解决信息不等式的\emph{formal}证明。这种证明可能会变得有用时,不等式是隐含的几个约束,由于PMF,证明是不容易的。更复杂的情况是,由于PMF的约束和统计模型产生的其他约束,不等式成立。这种情况包括信息理论容量区域、率失真函数和无损压缩率。首先给出了Shannon型信息不等式的形式定义。然后,我们审查的优化问题的最佳解决方案,以及如何提取的证明,是可读的用户。

英文摘要:

A class of information inequalities, called Shannon-type inequalities (STIs), can be proven via a computer software called ITIP. In previous work, we have shown how this technique can be utilized to Fourier-Motzkin elimination algorithm for Information Theoretic Inequalities. Here, we provide an algorithm for extracting \emph{analytic} proofs of information inequalities. Shannon-type inequalities are proven by solving an optimization problem. We will show how to extract a \emph{formal} proof of numerically solved information inequality. Such proof may become useful when an inequality is implied by several constraints due to the PMF, and the proof is not apparent easily. More complicated are cases where an inequality holds due to both constraints from the PMF and due to other constraints that arise from the statistical model. Such cases include information theoretic capacity regions, rate-distortion functions and lossless compression rates. We begin with formal definition of Shannon-type information inequalities. We then review the optimal solution of the optimization problem and how to extract a proof that is readable to the user.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑