#超强数学定理证明器##8B数学模型超越DeepSeek满血版# 超强数学定理证明器Goedel-Prover，不仅能自动写数学证明，在准确率上已刷新当前SOTA。 Goedel-Prover由普林斯顿大学牵头，想用大语言模型解决中高难度的数学问题，无论是奥数、大学课程，甚至是Putnam数学竞赛（美国大学生数学竞赛）都能做。 其训练流程相当独特： - 首先，用两个LLM将自然语言题转为Lean语言（形式化数学语言），一个模仿人类风格，另一个模仿Claude风格； - 接着，再来一个模型对这些“翻译”进行验证，只保留准确的版本； - 最后，让模型尝试独立完成证明，并将新解的版本不断加入训练集中，逐步优化能力。 V1版本于2025年初发布时，就已带来显著进展： - 在miniF2F数学基准上，Pass@ 32准确率达到57.6%，领先此前最强的RL微调模型7.6%； - 在Lean-workbook中生成了2.97万条正式证明，远超此前表现最好的定理模型； 而V2版本的发布，则将这一切推向新高度： 1. 模型能力大幅提升：32B主力模型在miniF2F上准确率达到88.1%（标准模式）和90.4%（自我纠错模式）； 2. 小模型表现惊艳：8B模型的表现已经接近DeepSeek-Prover-671B，仅用其1%的参数量； 3. PutnamBench创历史最好成绩：在自我纠错模式下解决64道题（Pass@ 64），使用的计算资源更少； 目前，Goedel-Prover V2系列已实现完全开源，涵盖8B与32B两个版本及全新奥数级数据集，论文也即将公开发布。 对许多人来说，“数学证明”听起来很遥远，但它代表的是大语言模型在逻辑推理能力上的实质性突破。而Goedel-Prover正用开源方式，让这项前沿技术变得触手可及。 感兴趣的小伙伴可以点击：-prover.com/
