SWE-smith: Scaling Data for Software Engineering Agents
大家都知道 swe-bench，是解决真实世界仓库 issue 的 benchmark。但是，有没有对应的训练集 /sft 数据呢？作者发现，没有。怎么办，作者找了 100 多个仓库，合成了很多的 issue 和解决方案。在大规模训练以后，甚至还没有 rl，仅仅 sft，就刷到了 40 分。
所以，data is all you need
DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
deepseek 新出的 lean4 证明模型。这里面的优化暂且不提，但主图很有意思：作者发现，v3 等强的 ai，用 word-based 的证明方法，实际上已经接近了 lean4 模型的能力。尤其是 reasoning model 以后，可能超越了 lean 语言的证明能力。
如果是这样的话，继续研究 lean 的意义在哪？是因为更方便去验证证明对不对吗？
Phi-4-reasoning Technical Report
phi 系列的 reasoning 产品来了。作者发现根据题目的难度选择蒸馏什么数据对 o1-sft 作用很大，然后通过进一步做一点 rl 效果会更好
用 o3-mini 蒸数据的力量
v1.5.2