DeepSeekMath-V2、DeepSeek-Prover、DeepSeek-Prover-V2

DeepSeekMath-V2

来自https://arxiv.org/pdf/2511.22570，个人感觉贡献远没有提出GRPO的DeepSeekMath大。简单来说思路就是Reward Model一部分输入从自己整一个meta_verification，一个GRPO过程变成了2个GRPO过程，通过meta_verification验证证明的过程对不对，这非常符合人类证明的过程。

DeepSeek-Prover（DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data）

大规模合成数据：DeepSeek-Prover从广泛的非正式数学问题集合（自然语言数据）出发，生成正式的需要进一步证明的数学陈述（statements），这些陈述使用Lean 4证明语言进行形式化。通过模型评分和假设拒绝方法对自动形式化陈述进行过滤，以选择高质量的陈述。这些陈述由DeepSeek-Prover的模型进行证明，其正确性由Lean 4进行验证，从而生成经过验证的正式陈述和证明。
双重并发证明搜索：针对每个合成语句，DeepSeek-Prover同时搜索其正面陈述（Γ ⊚ P）和否定陈述（Γ ¢ ¬P）的证明。一旦找到有效的证明，搜索就终止，从而加速证明的合成过程。
迭代优化：新生成的经过验证的陈述和证明被用作微调DeepSeek-Prover的合成数据，进一步迭代模型。通过多轮迭代，模型生成的定理证明对的质量越来越高，从而不断提升模型在形式定理证明中的能力。

这是一个例子：

来源

1. https://www.xiaohongshu.com/explore/66a7ca6e000000000600f2b1?xsec_token=ABhuYcPVrRIYgvR8hjVybi_q0OrgNhIUjHxnCzXqk8_UE=&xsec_source=pc_search&source=web_search_result_notes
2. https://arxiv.org/pdf/2405.14333

DeepSeek-Prover-V2（DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition）

还是形式化语言证明：