学习发现有趣的数学
一项新研究探索了大型语言模型如何发现不仅能够证明，而且有趣且有用的数学定理。研究人员将定理的内在趣味性定义为证明长度与命题长度之比，并发现这一指标与定理后续的实际效用高度相关。他们训练了一个拥有270亿参数的模型，其预测证明难度的准确率超过了前沿通用模型。按照该指标进行优化后，与 Mathlib 的大幅或完全重叠率从91.9%降至30.6%，生成了更多分布外数学内容。该系统能够生成定理候选、筛选最有趣的结果，并逐步构建可由机器验证的自扩展数学库。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。