用微调语言模型+搜索算法自动证明信息论不等式，成功率超85%
Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search
- 用0.6B小模型微调后结合引导式搜索，自动构造证明步骤
- 在10-15个变量的不等式上达到85%成功，远超零样本基线
- 适合对信息论证明自动化感兴趣的研究人员
证明香农型熵不等式是信息论中的基础任务，常需构造复杂的已知约束线性组合，属于随随机变量数增长而急剧恶化的组合搜索问题。我们研究小型大语言模型（0.6B–1.7B参数）经原子证明步骤微调后，结合引导束搜索能否实现自动化。在包含60个不等式的独立测试集（变量数n=10至15）上，0.6B微调模型在树搜索下取得85%的证明成功率。GPT-5.5在零样本提示下仅解决1.7%样本，Psitip解决33.3%。系统性消融实验表明，4096词元、非偏斜数据分布训练效果最佳，扩展上下文或使用偏斜数据无边际提升。进一步识别出两类主要失败模式——格式错误与步骤质量下降，并验证束搜索评分启发式至关重要：随机评分使成功率从83%降至23%。
原文摘要 · Abstract (English)
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\%).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。