好久没更新了，工作模式有了些变动，从今天开始恢复更新。希望这几周没有错过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数据+运行时蒙特卡洛搜索
