标签
LANTERN 是一条快速流程，它使用基于预训练语言模型激活值的分类器对候选数学关系进行排序，随后进行过滤、生成与验证。应用于 OEIS 后，它发现了 62 条经过验证的关系，其中 9 条具有信息价值，另有 4 条全新的数学关联，整个过程在不到 8 小时内完成。
本文提出了一种自监督定理发现算法，该算法仅从公理和推理规则出发，无需人类先验知识即可构建定理库。实验表明，发现的定理具有意义，并能提升大语言模型的证明性能。