AI 与机器学习2024arxiv.org
DeepSeek：通过大规模合成数据推进 LLM 定理证明
DeepSeek: Advancing theorem proving in LLMs through large-scale synthetic data
进阶 · 约 60 分钟读完前置知识：大语言模型基础、形式化验证/证明助手（如 Lean）、合成数据训练
导读
这篇论文（DeepSeek）研究如何用大规模合成数据提升大语言模型的定理证明能力：借助证明助手的自动验证来生成并筛选合成证明数据，再用于训练模型。据评论者提到的结果，一个 7B 级别的模型在该任务上的成绩约为 GPT-4 的两倍。
HN 关注点：HN 读者的讨论焦点是：定理证明因为可以自动验证，被认为是 LLM 最理想的合成数据应用场景；但同时也有人质疑多步逻辑推理的架构瓶颈和过拟合问题。
HN 评论精选
这几条评论里：支持 2 质疑 1
支持可自动验证的正确性让定理证明成为合成数据训练的天然场景。
这应该是 LLM 最好的应用场景之一：结果总能自动验证，不行就丢弃，对吧？
_flux查看英文原文
This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?
质疑质疑合成数据加验证的路线：多步推理是架构性瓶颈，不是数据量问题。
自动验证加合成数据在从业者中基本是常识。但这些机构也反复探索过各种在这类数据上过拟合的方式，结论都一样：当前模型架构在多步逻辑推理上似乎会停滞。你要么偏离预训练常识太远，要么在巨大的设计空间里永远找不到正确的步骤。想想看，为什么没人能让 LLM 下围棋超过 AlphaZero 同时又保留语言能力？那样的参数量肯定要大几个数量级。
aabhay查看英文原文
The ability to use automatic verification + synthetic data is basically common knowledge among practitioners. But all these organizations have also explored endlessly the different ways to overfit on such data and the conclusion is the same -- the current model architecture seems to plateau when it comes to multi-step logical reasoning. You either drift from your common knowledge pre-training too far or you never come up with the right steps in instances where there's a vast design space. Think -- why has nobody been able to make an LLM play Go better than AlphaZero while still retaining language capabilities? It certainly would have orders of magnitude more parameters.
支持认为评论区的冷淡反应低估了 7B 模型翻倍 GPT-4 成绩的意义。
对这里的负面反应感到惊讶。一个 7B 级别的模型把 GPT-4 的分数差不多翻了一倍，大家却只是“嗯”一声？
Havoc查看英文原文
Surprised by the negativity here. A 7B class model +- doubles gpt4 score and everyone goes “meh”?!?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2024Hacker News 讨论帖186 分 · 54 评
同领域还值得读
DeepSeek-R1：通过强化学习激励 LLM 的推理能力
DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via RL
研究如何用强化学习激励大语言模型的推理能力，提出 DeepSeek-R1，并探讨 RL 训练对模型推理表现的影响。
AI 与机器学习2025 · 1,351 分 · 1,056 评 · 引用 30进阶 · 约 80 分钟编辑精选1-bit LLM 时代：面向低成本计算的三值参数
The Era of 1-bit LLMs: ternary parameters for cost-effective computing
提出用三值参数 {-1, 0, 1} 替代 LLM 中的浮点权重，即所谓“1-bit LLM”。
AI 与机器学习2024 · 1,040 分 · 447 评 · 引用 19进阶 · 约 45 分钟编辑精选DeepSeek-V3.2：推进开放大语言模型的前沿
DeepSeek-v3.2: Pushing the frontier of open large language models
这是 DeepSeek-V3.2 的技术报告，延续了 DeepSeek 开源权重模型的路线，目标是让开放模型继续逼近甚至追平前沿闭源模型。
AI 与机器学习2025 · 982 分 · 465 评进阶 · 约 90 分钟编辑精选通过自我对弈与通用强化学习掌握国际象棋和将棋（AlphaZero）
Mastering Chess and Shogi by Self-Play with General Reinforcement Learning
DeepMind 的 AlphaZero 论文：用通用强化学习算法（自我博弈 + MCTS + 神经网络），从零开始仅数小时训练便在国际象棋和将棋上击败了世界顶级引擎 Stock…
AI 与机器学习2017 · 539 分 · 270 评 · 引用 13进阶 · 约 90 分钟编辑精选用强化学习发现更快的矩阵乘法算法
Discovering faster matrix multiplication algorithms with reinforcement learning
论文提出 AlphaTensor，用强化学习搜索矩阵乘法算法。
AI 与机器学习2022 · 518 分 · 111 评专业 · 约 90 分钟编辑精选