Jul, 2024
LEAN-GitHub:为多功能LEAN证明器编译GitHub LEAN库
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN
prover
TL;DR本研究解决了形式定理证明数据匮乏的问题,通过从几乎所有Lean 4 GitHub库中提取大规模形式数据,提出了LEAN-GitHub数据集。通过在该数据集上对InternLM-math-plus进行微调,研究发现模型在多个Lean 4基准测试中均取得了优于现有方法的表现,显示出该数据集在广泛数学主题的形式推理中的重要价值。