Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search

📄 arXiv: 2606.05729v1 📥 PDF

作者: Shing Yin Wong, Shaocheng Liu, Linqi Song, Amin Gohari, Cheuk Ting Li

分类: cs.IT, cs.LG

发布日期: 2026-06-04

💡 一句话要点

提出基于微调语言模型的自动化香农熵不等式证明方法

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 熵不等式 自动证明 语言模型 引导树搜索 信息论 组合搜索 微调技术

📋 核心要点

  1. 现有方法在证明香农熵不等式时面临组合搜索问题，随着随机变量数量增加，效率显著降低。
  2. 论文提出通过微调小规模语言模型并结合引导树搜索的方法，旨在自动化熵不等式的证明过程。
  3. 实验结果显示，微调后的0.6B模型在树搜索中达到了85%的成功率，显著优于其他基线模型。

📝 摘要（中文）

证明香农类型的熵不等式是信息论中的一项基本任务，通常需要构造已知约束的非平凡线性组合，这是一种随着随机变量数量增加而扩展困难的组合搜索问题。本文探讨了小规模的大型语言模型（参数量为0.6B至1.7B），通过微调原子证明步骤并结合引导树搜索，能否自动化这一过程。在一个包含60个不等式的测试集上，微调后的0.6B模型在树搜索中实现了85%的证明成功率，而GPT-5.5在零-shot提示下仅解决了1.7%的样本，Psitip解决了33.3%的样本。系统的消融研究表明，4096-token的非偏态训练分布表现最佳，扩展上下文和偏态数据未带来边际收益。我们还识别了两种主要的失败模式——格式失败和步骤质量下降，并通过控制消融验证了束评分启发式的重要性。

🔬 方法详解

问题定义：本文旨在解决香农类型熵不等式的自动证明问题。现有方法在处理随机变量数量增加时，组合搜索效率低下，难以应对复杂的证明任务。

核心思路：通过微调小规模的语言模型，使其能够理解和生成原子证明步骤，并结合引导树搜索策略，以提高证明的自动化程度和成功率。

技术框架：整体架构包括数据准备、模型微调和引导树搜索三个主要模块。首先，收集并标注原子证明步骤数据；其次，微调语言模型以适应特定的证明任务；最后，利用引导树搜索策略进行有效的组合搜索。

关键创新：最重要的技术创新在于将微调语言模型与引导树搜索相结合，显著提升了证明成功率，与传统方法相比，能够更有效地处理复杂的组合搜索问题。

关键设计：在模型微调过程中，采用了4096-token的非偏态训练分布，并通过消融实验验证了束评分启发式的重要性，确保了模型在实际应用中的高效性。

📊 实验亮点

实验结果显示，微调后的0.6B模型在树搜索中实现了85%的证明成功率，而对比基线模型如GPT-5.5仅为1.7%，Psitip为33.3%。此外，消融实验表明，束评分启发式对成功率至关重要，随机评分导致成功率从83%降至23%。

🎯 应用场景

该研究的潜在应用领域包括信息论、密码学和机器学习等领域，能够为复杂的数学证明提供自动化工具，降低人力成本，提高效率。未来，该方法可能在其他需要组合搜索的领域中得到推广，推动相关研究的发展。

📄 摘要（原文）

Proving Shannon-type entropy inequalities is a fundamental task in information theory that often requires constructing non-trivial linear combinations of known constraints, which is a combinatorial search problem that scales poorly with the number of random variables. We investigate whether small-scale large language models (0.6B--1.7B parameters), fine-tuned on atomic proof steps and combined with guided beam search, can automate this process. On a held-out test set of 60 inequalities spanning n=10 to 15 variables, our 0.6B fine-tuned model achieves an 85\% proof success rate with tree search. GPT-5.5 solves 1.7\% samples under zero-shot prompting while Psitip solves 33.3\% samples. A systematic ablation study across training context length (4096 vs.\ 8192 tokens) and data distribution (n=9-skewed vs not skewed) reveals that a 4096-token not skewed training distribution yields the best performance, with extended context and skewed data providing no marginal benefit. We further identify two dominant failure modes -- format failures and step quality degradation -- and verify that the beam-scoring heuristic is essential via a controlled ablation (random scoring reduces success from 83\% to 23\%).