好久没更新了，工作模式有了些变动，从今天开始恢复更新。希望这几周没有错过 AGI 关键论文……
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
deepseek 最新出的数学模型，和之前的 - math 不同，这个模型 focus 在用 lean 4 做数学证明。之前有一些相关的工作，但好像这个领域一直没有 math word problem 自然语言解题火。这篇工作感觉还挺好的，SFT 数据 + 运行时蒙特卡洛搜索
v1.5.2