Tag DeepSeek-Prover

DeepSeek-Prover V1（arXiv:2405.14333）与 V1.5（arXiv:2408.08152）详解：autoformalization 合成数据 + RLPAF + RMaxTS 蒙特卡洛树搜索，把 7B 模型在 Lean 4 形式化证明 benchmark miniF2F 上推到 63.5%，并为后续 R1 reasoning 训练提供方法论起点。