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\%).

翻译：证明香农型熵不等式是信息论中的一项基础任务，通常需要构造已知约束的非平凡线性组合，这是一个与随机变量数量成超线性关系的组合搜索问题。我们研究是否可以通过将微调于原子化证明步骤的小规模大语言模型（0.6B至1.7B参数量）与引导式束搜索相结合，实现该过程的自动化。在包含n=10至15个变量的60个不等式的留存测试集上，我们的0.6B微调模型结合树搜索实现了85%的证明成功率。零样本提示下的GPT-5.5仅能解决1.7%的样本，而Psitip解决了33.3%的样本。针对训练上下文长度（4096 vs. 8192 tokens）与数据分布（n=9偏斜 vs. 非偏斜）的系统消融实验表明，采用非偏斜训练分布且上下文长度为4096 tokens的设置表现最佳，而延长上下文与使用偏斜数据均未带来边际收益。我们进一步识别出两类主要失败模式——格式失配与证明步骤质量退化，并通过控制消融实验证实了束评分启发式方法的必要性（随机评分使成功率从83%降至23%）。