Goedel-Prover:专为自动化数学问题的形式证明生成而设计的 LLM,快速解决形式化数学问题

本文涉及的产品
模型训练 PAI-DLC,100CU*H 3个月
交互式建模 PAI-DSW,每月250计算时 3个月
模型在线服务 PAI-EAS,A10/V100等 500元 1个月
简介: Goedel-Prover 是一款由普林斯顿大学和清华大学等机构联合推出的开源模型,专注于自动化数学问题的形式证明生成。它通过将自然语言数学问题翻译成形式语言(如 Lean 4),显著提升了数学问题的证明效率。

❤️ 如果你也关注 AI 的发展现状,且对 AI 应用开发感兴趣,我会每日分享大模型与 AI 领域的开源项目和应用,提供运行实例和实用教程,帮助你快速上手AI技术!

🥦 微信公众号|搜一搜:蚝油菜花 🥦


大家好,我是蚝油菜花,今天跟大家分享一下 Goedel-Prover 这个由普林斯顿大学、清华大学等机构联合推出的开源自动化数学问题的形式证明生成模型。

🚀 快速阅读

Goedel-Prover 是一款专注于自动化数学问题的形式证明生成的开源模型。

  1. 核心功能:将自然语言数学问题翻译成形式语言,并自动生成完整的证明。
  2. 技术原理:基于专家迭代方法,逐步提升证明能力,处理大规模形式化陈述和证明数据集。

Goedel-Prover 是什么

Goedel-Prover

Goedel-Prover(哥德尔证明器)是由普林斯顿大学、清华大学等机构联合推出的开源大型语言模型(LLM),专为自动化数学问题的形式证明生成而设计。该模型通过将自然语言数学问题翻译成形式语言(如 Lean 4),解决了形式化数学陈述和证明稀缺的问题。Goedel-Prover 使用专家迭代方法进行训练,基于不断扩展的形式证明数据集,逐步提升其证明能力。

在多个基准测试中,Goedel-Prover 表现出色。例如,在 miniF2F 基准测试中,Goedel-Prover 达到了 57.6% 的成功率,显著优于之前的开源模型。此外,它成功解决了 PutnamBench 中的 7 个问题,并为 Lean Workbook 生成了近 3 万个形式证明,为自动化定理证明领域带来了重大突破。

Goedel-Prover 的主要功能

  • 形式化翻译:将自然语言数学问题转换为形式语言,确保翻译的准确性和完整性。
  • 证明生成:自动生成完整的证明,支持复杂的数学推理。
  • 性能优化:基于专家迭代方法不断优化证明能力,提升证明成功率。
  • 大规模数据处理:处理和生成大规模的形式化陈述和证明数据集,提升模型的泛化能力。

Goedel-Prover 的技术原理

  • 形式化翻译:使用两个形式化器(Formalizer A 和 Formalizer B)将自然语言数学问题翻译成 Lean 4 的形式语言。两个形式化器分别基于不同的数据集进行训练,增加形式化风格的多样性。通过编译正确性(CC)测试和忠实性与完整性(FC)测试评估形式化陈述的质量,确保其符合 Lean 语法且准确捕捉原始问题的含义。
  • 专家迭代(Expert Iteration):初始阶段,用现有的证明器(如 DeepSeek-Prover-V1.5-RL)为每个形式化陈述生成多个证明候选,基于 Lean 编译器验证证明的正确性。将验证通过的证明收集起来,作为训练数据,对基础模型(如 DeepSeek-Prover-V1.5-Base)进行监督微调,生成新的证明器。重复上述过程,每次迭代都用新的证明器生成更多的证明,并将其加入训练数据,逐步提升模型的证明能力。
  • 数据集扩展:除使用公开的 Numina 数据集外,Goedel-Prover 形式化大量私人收集的数学问题,与 Lean Workbook 中的现有陈述合并,形成大规模的形式化陈述数据集。在训练过程中,逐步加入 Mathlib4 等外部数据集,增强模型对不同数学领域的适应能力。

如何运行 Goedel-Prover

1. 安装依赖环境

  1. 安装 Lean 4

    按照 Lean 4 安装页面 的说明设置 Lean 4。

  2. 克隆仓库

    git clone --recurse-submodules https://github.com/Goedel-LM/Goedel-Prover.git
    cd Goedel-Prover
    
    AI 代码解读
  3. 安装依赖项

    pip install -r requirements.txt
    
    AI 代码解读
  4. 构建 mathlib4

    cd mathlib4
    lake build
    
    AI 代码解读
  5. 测试 Lean 4 和 mathlib4 安装

    cd ..
    python prover/lean/verifier.py
    
    AI 代码解读

    如果出现任何错误,请重新安装 Lean 4 并重新构建 mathlib4。

2. 快速启动

要运行推理并重现 miniF2F 上的性能,可以使用以下命令:

sh eval/eval.sh -i datasets/minif2f.jsonl -s test -m Goedel-LM/Goedel-Prover-SFT -o results/minif2f/Godel-Prover-SFT -n 32 -g 2 -c 128
AI 代码解读

结果将总结在 results/minif2f/Godel-Prover-SFT/compilation_summarize.json 文件中。

指定参数如下:

  • -i:要评估的数据集路径
  • -s:要评估的数据集分割,通常设置为 "test"
  • -m:模型名称或路径
  • -o:输出目录
  • -n:Pass 数量
  • -g:用于推理的 GPU 数量
  • -c:用于编译的 CPU 数量

资源

- GitHub 仓库https://github.com/Goedel-LM/Goedel-Prover

❤️ 如果你也关注 AI 的发展现状,且对 AI 应用开发感兴趣,我会每日分享大模型与 AI 领域的开源项目和应用,提供运行实例和实用教程,帮助你快速上手AI技术!

🥦 微信公众号|搜一搜:蚝油菜花 🥦

相关实践学习
使用PAI-EAS一键部署ChatGLM及LangChain应用
本场景中主要介绍如何使用模型在线服务(PAI-EAS)部署ChatGLM的AI-Web应用以及启动WebUI进行模型推理,并通过LangChain集成自己的业务数据。
机器学习概览及常见算法
机器学习(Machine Learning, ML)是人工智能的核心,专门研究计算机怎样模拟或实现人类的学习行为,以获取新的知识或技能,重新组织已有的知识结构使之不断改善自身的性能,它是使计算机具有智能的根本途径,其应用遍及人工智能的各个领域。 本课程将带你入门机器学习,掌握机器学习的概念和常用的算法。
目录
打赏
0
4
4
0
334
分享
相关文章
仅7B的模型数学推理能力完虐70B?MIT哈佛推出行动思维链COAT让LLM实现自我反思并探索新策略
Satori 是由 MIT 和哈佛大学等机构联合推出的 7B 参数大型语言模型,专注于提升推理能力,具备强大的自回归搜索和自我纠错功能。
104 6
仅7B的模型数学推理能力完虐70B?MIT哈佛推出行动思维链COAT让LLM实现自我反思并探索新策略
AI做数学学会动脑子! UCL等发现LLM程序性知识,推理绝不是背答案
大型语言模型(LLM)在数学推理中的表现一直备受争议。伦敦大学学院等机构的研究发现,LLM可能通过综合程序性知识而非简单检索来解决数学问题。研究分析了7B和35B参数模型在三个简单数学任务中的数据依赖,表明模型更关注解决问题的过程和方法,而非答案本身。这一发现为改进AI系统提供了新思路,但也指出LLM在复杂问题处理上仍存在局限。论文地址:https://arxiv.org/abs/2411.12580
37 2
LLM群体智能崛起,数学性能暴增11.6%!谷歌DeepMind四大机构联手新作
【10月更文挑战第17天】近日,谷歌、DeepMind等四大机构联合发布论文,展示大型语言模型(LLMs)在数学问题解决上的显著进步。通过引入元认知知识,研究人员开发了提示引导的交互程序,使LLMs能为数学问题分配合理技能标签并进行语义聚类。实验结果显示,GPT-4在GSM8K和MATH数据集上的准确性分别提升了11.6%和7.52%,展现出巨大潜力。这一成果不仅为AI领域提供了新思路,也为数学教育带来了启示。
60 4
CoT神话破灭,并非LLM标配!三大学府机构联手证实,CoT仅在数学符号推理有用
【10月更文挑战第17天】链式思维(CoT)曾被认为是大型语言模型(LLM)激发推理能力的关键方法,但最新研究显示,CoT仅在数学和符号推理任务中有效,其他任务中效果不明显。加州大学伯克利分校、斯坦福大学和卡内基梅隆大学的联合研究打破了CoT作为LLM标配的神话,为重新评估LLM的推理能力提供了新视角。
94 1
AI长脑子了?LLM惊现人类脑叶结构并有数学代码分区,MIT大牛新作震惊学界!
麻省理工学院的一项新研究揭示了大型语言模型(LLM)内部概念空间的几何结构,与人脑类似。研究通过分析稀疏自编码器生成的高维向量,发现了概念空间在原子、大脑和星系三个层次上的独特结构,为理解LLM的内部机制提供了新视角。论文地址:https://arxiv.org/abs/2410.19750
100 12
LLM群体智能崛起,数学性能暴增11.6%!谷歌DeepMind四大机构联手新作
【10月更文挑战第16天】最新研究显示,大型语言模型(LLMs)在数学问题解决上取得显著进展。谷歌、DeepMind等机构的研究人员通过引入元认知知识,使LLMs能更好地理解和解决数学问题,其在GSM8K和MATH数据集上的准确率分别提升了11.6%和7.52%。这一成果不仅为AI领域开辟了新路径,也为数学教育带来了新的可能性。
73 3
CoT神话破灭,并非LLM标配!三大学府机构联手证实,CoT仅在数学符号推理有用
【10月更文挑战第16天】近期,加州大学伯克利分校、斯坦福大学和卡内基梅隆大学联合研究发现,链式思维(CoT)方法在数学和符号推理任务中表现优异,但在其他类型任务中效果不明显。这一研究打破了CoT作为大型语言模型(LLM)标配的神话,为重新审视LLM的推理能力提供了新视角。
78 2
杨笛一团队最新百页论文:首次统计学上证明,LLM生成的idea新颖性优于人类
【10月更文挑战第12天】斯坦福大学杨笛一团队发布百页论文,首次通过统计学方法证明大型语言模型(LLMs)在生成研究想法的新颖性上优于人类专家。研究招募100多名NLP专家进行盲评,结果显示LLM在新颖性方面显著胜出,但在可行性上稍逊。研究揭示了LLM在科研创新中的潜力与局限。
126 2
|
6月前
|
LLM数学性能暴涨168%,微软14人团队力作!合成数据2.0秘诀曝光,智能体生成教学
【9月更文挑战第14天】微软研究团队发布了一篇介绍新型框架"AgentInstruct"的论文,该框架旨在通过自动生成高质量合成数据,推动语言模型发展。AgentInstruct仅需原始数据源即可创建多样化的合成数据,减少人工工作量。研究团队基于此框架构建了含2500万训练对的数据集,展示了其在多种技能教学中的潜力。经微调后的Mistral-7b模型演进为Orca-3,在多个基准测试中显著超越同类模型。尽管如此,AgentInstruct仍面临创建流程耗时及合成数据复杂性不足等问题。论文详情见:https://arxiv.org/pdf/2407.03502
129 2
CMU清华教LLM练成数学高手,LeanSTaR训练模型边思考边证明,登顶新SOTA
【9月更文挑战第2天】卡内基梅隆大学与清华大学的研究团队开发出名为LeanSTaR的语言模型,该模型结合形式化验证与机器学习技术,在数学证明上取得了重大突破,实现了类似人类数学家的思考和证明能力。这一成果不仅提升了数学证明任务的性能,尤其在复杂推理方面表现突出,还为数学研究和教育提供了有力支持。论文详细内容可访问 https://arxiv.org/abs/2407.10040。
95 12

热门文章

最新文章

AI助理

你好,我是AI助理

可以解答问题、推荐解决方案等