阅读了论文 DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data。
论文中用构造条件冲突导出 False，以及使用结论的否定让模型尝试证明来排除错误的 theorems，这个是一个很不错的idea，值得借鉴。
- 论文大致思路是：在给定数据集中，先保留初始模型成功生成的 theorems的证明结果用于加强模型，再使用更新后的模型重新处理此前失败的 theorems或者生成新的theorems，由此形成循环并进行多轮迭代。
- 反思：进行单一数据集，进行iterations也有缺点，数据集生成了正确的theorems总归是有限的，因此需要扩大数据集的范围。对于数学命题，证明题的数据增强比较难处理，计算题相对好处理但是路径比较单一，如果能够对于题目同步做数据增强，或许能够在一定程度上处理数据集有限问题。