BriefGPT.xyz
Jul, 2024
TheoremLlama: 通用 LLM 转换为 Lean4 专家
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
HTML
PDF
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao...
TL;DR
使用Lean等计算机可验证形式语言来证明数学定理具有重大影响,本文提出了TheoremLlama框架,通过生成对齐的数据集和训练方法,使大型语言模型成为Lean4专家,实现了高于GPT-4基准的累积准确率。
Abstract
Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal
theorem proving
involves generating complete proofs using
large lan
→