基本介紹
- 外文名：Goedel-Prover-V2
- 類型：開源定理證明器
參數性能,技術創新,發展歷史,
參數性能
有 32B 和 8B 兩個參數版本。在多個基準測試中表現卓越，如在 PutnamBench 基準上奪冠，解決 64 道數學難題；在 MathOlympiadBench 基準上刷爆 SOTA，攻克 73 個問題 ，遠超 671B 的 DeepSeek-Prover。在 miniF2F 基準上，32B 模型 Pass@32 成績達 90.4%，擊敗 DeepSeek-Prover-V2-671B（82.4%），8B 模型與之實力相當。
技術創新
以 Qwen3-8B 和 Qwen3-32B 為基座模型，採用 “專家疊代與強化學習” 框架，並融入分層式數據合成、驗證器引導的自我修正、模型平均三大創新技術。分層式數據合成自動生成難度遞增的證明任務訓練模型；驗證器引導的自我修正利用 Lean 編譯反饋修訂證明；模型平均融合模型檢查點提升魯棒性與性能。
發展歷史
2025年7月17日，僅8B參數的Goedel-Prover-V2擊敗671B的DeepSeek-Prover，橫掃三大數學基準，用高校實驗室算力實現形式化證明新突破——普林斯頓、清華等八大頂尖機構聯手打造的開源模型，正以分層訓練、自我修正等創新技術重新定義AI數學推理的極限。
