-
题名基于预训练语言模型和合一算法的自动定理证明
- 1
-
-
作者
陈红休
曾霞
刘志明
赵恒军
-
机构
西南大学计算机与信息科学学院软件学院
-
出处
《计算机科学》
北大核心
2026年第4期40-47,共8页
-
基金
国家自然科学基金(62272397,62472362,92582113)
重庆市自然科学基金(CSTB2025NSCQ-LZX0019)。
-
文摘
预训练语言模型在Metamath等形式化环境中,在证明定理方面展现出显著潜力。然而,这种潜力尚难以稳定转化为可靠的推理能力。现有方法通常要求语言模型直接预测替换项,而这些替换项来自一个开放且潜在无限的表达式空间,缺乏逻辑约束,导致模型泛化能力受限。为此,提出一种新的证明范式:在推理过程中引入工作变量以临时替代具体项,并通过合一算法推导出其具体实例。该设计使得模型能够聚焦于定理选择,而无需生成缺乏逻辑指导的替换。基于这一范式,从Metamath数学库中提取数据并构建UnProver(Unification-Driven Prover),并在此数据上对其进行训练。此外,设计多种数据增强策略,进一步提升UnProver的性能。实验结果表明,UnProver在测试集上整体优于包括GPT-4o在内的基线方法,在证明能力与效率方面均取得更优表现。此外,UnProver还发现了6个新的、更简洁的证明,这些证明已被正式收录至Metamath官方数学库。
-
关键词
语言模型
定理证明
metamath
合一
工作变量
-
Keywords
Language models
Theorem proving
metamath
Unification
Work variables
-
分类号
TP181
[自动化与计算机技术—控制理论与控制工程]
-
