D

Deepseek Prover V2 671B

由deepseek-ai開發
專為Lean 4形式化定理證明設計的開源大語言模型,通過遞歸定理證明流程收集數據,結合非正式和形式化的數學推理。
下載量 9,693
發布時間 : 4/30/2025

模型概述

DeepSeek-Prover-V2是一個專為Lean 4形式化定理證明設計的開源大語言模型,其初始化數據通過由DeepSeek-V3驅動的遞歸定理證明流程收集。該模型能夠將非正式和形式化的數學推理統一到一個模型中,並在神經定理證明中達到最先進的性能。

模型特點

遞歸定理證明流程
通過遞歸定理證明流程收集數據,利用DeepSeek-V3作為子目標分解和形式化的統一工具,生成冷啟動推理數據。
強化學習
在合成冷啟動數據上微調證明模型後,進行強化學習階段,進一步增強其將非正式推理與形式化證明構建連接的能力。
高性能
在MiniF2F測試中達到88.9%的通過率,並解決了PutnamBench中的49個問題。

模型能力

形式化定理證明
數學推理
子目標分解
Lean 4代碼生成

使用案例

數學形式化
MiniF2F問題求解
使用DeepSeek-Prover-V2解決MiniF2F數據集中的形式化數學問題。
在MiniF2F測試中達到88.9%的通過率。
PutnamBench問題求解
使用DeepSeek-Prover-V2解決PutnamBench中的數學問題。
解決了PutnamBench中的49個問題。
教育
教科書問題形式化
使用DeepSeek-Prover-V2將教科書中的數學問題形式化為Lean 4代碼。
ProverBench數據集包含325個形式化問題。
AIbase
智啟未來,您的人工智能解決方案智庫
© 2025AIbase