DeepSeek-Prover-V1.5: Lean Proofs with RL and Search
DeepSeek-Prover-V1.5 combines Lean feedback, reinforcement learning, and RMaxTS search, reaching 63.5% on miniF2F and 25.3% on ProofNet.
Institution
DeepSeek
A Chinese AI lab known for strong open-weight language and reasoning models.
DeepSeek-V3 Explained: A 671B MoE Trained for 2.788M GPU Hours
DeepSeek-V3 is a 671B-parameter MoE model that activates only 37B params per token, matches leading closed models on many benchmarks, and was pre-trained on 14.8T tokens for just 2.788M H800 GPU hours with open weights.
DeepSeek-R1: How Pure Reinforcement Learning Taught an LLM to Reason
DeepSeek-R1 learns to reason from reinforcement learning on whether its answer is correct — with no human reasoning examples — matches OpenAI o1 on AIME and MATH-500, and ships open MIT-licensed weights.