DeepSeek-Prover-V1.5:用 RL 和搜索做 Lean 证明
DeepSeek-Prover-V1.5 把 Lean 反馈、强化学习和 RMaxTS 搜索结合起来,miniF2F 达 63.5%,ProofNet 达 25.3%。
机构
以强力开源权重语言与推理模型著称的中国 AI 实验室。
DeepSeek-Prover-V1.5 把 Lean 反馈、强化学习和 RMaxTS 搜索结合起来,miniF2F 达 63.5%,ProofNet 达 25.3%。
DeepSeek-V3 是 6710 亿参数混合专家模型,每 token 仅激活 370 亿,全程训练只用 278.8 万 H800 GPU 时,比肩头部闭源模型且开源权重。
只奖励答案对错、不喂人工推理过程,DeepSeek-R1 让大模型自发学会逐步推理,数学基准比肩 OpenAI o1,且开源 MIT 权重。