TheoremSmith：批量生成高难度证明题训练LLM
TheoremSmith 尝试用自动化批量生成高难度证明题，破解 LLM 数学推理训练的数据瓶颈。
TheoremSmith 是 Hacker News Show HN 上的一个项目，主张让系统自动、大批量地生产高难度数学证明题，用于训练大语言模型的推理与证明能力。文章指出，证明题因缺乏唯一答案、评判复杂、人工编写成本高而成为稀缺资源，而合成数据在代码和指令遵循领域的成功为这一思路提供了依据。难度可控的题目池可支撑课程式训练，并为自动求解、验证和强化学习提供原料；批量生成的难题还可作为评测基准的补充。但核心挑战在于保证题目陈述的正确性与意义，而非单纯生成，且该项目社区讨论度有限，实际效果仍待验证。
从「刷题」到「造题」：LLM 证明能力训练的新思路
在 Hacker News 的 Show HN 板块，一个名为 TheoremSmith 的项目提出了一个有趣的方向：与其等待人类数学家出题，不如让系统自动、大批量地生产高难度证明题，用来训练大语言模型的推理与证明能力。该帖获得了 7 个点数，虽然讨论量不大，但它触及了当前 LLM 数学推理训练中的一个核心瓶颈——高质量、高难度的证明题太稀缺。
为什么证明题是稀缺资源
数学推理一直是衡量 LLM 能力的重要标尺，但多数公开数据集集中在有确定答案的计算题或选择题上。证明题不同：它没有唯一答案，需要多步逻辑推演，评判标准也更复杂。人工编写一道严谨的证明题成本很高，而模型要真正提升证明能力，又需要大量、多样、难度分布合理的题目。TheoremSmith 试图用自动化生产的方式填补这个缺口，思路与「合成数据」在代码、指令遵循领域的成功经验一脉相承。
合成数据（Synthetic Data） 指由程序或模型自动生成、而非从真实世界采集的训练数据。在代码领域，GitHub Copilot 等系统大量使用模型自己生成的代码片段做微调；在指令遵循领域，Self-Instruct 用强模型生成指令-回答对，已证明其效果可媲美人工标注数据。合成数据的优势是规模大、成本低、可控制分布，但风险在于生成器本身的偏差会被放大。TheoremSmith 把这一范式移植到数学证明题上，本质上是用自动化方式「制造」训练语料，其成败取决于生成内容能否通过严格的正确性检验。
TheoremSmith 要解决什么
批量生产与难度控制
从项目标题可以看出，TheoremSmith 的关键词是「Mass-Producing」和「Hard Proof Problems」。这意味着它不只是随机生成一些数学陈述，而是希望系统性地产出有难度、可供训练使用的证明题。对于训练流程而言，难度可控的题目池意味着可以构造课程式（curriculum）的训练数据：从较易的引理组合逐步过渡到需要创造性洞察的难题，帮助模型建立更稳健的推理链条。
课程式训练（Curriculum Learning） 源自 Bengio 等人 2009 年的工作，核心思想是让模型先学简单样本、再逐步过渡到困难样本，从而更稳定地收敛。在 LLM 推理训练中，这意味着需要一条难度连续可调的题目谱系。TheoremSmith 强调「难度可控」，正是为了支撑这种训练策略：如果生成器只能产出固定难度的题目，模型要么在过易的题上浪费算力，要么在过难的题上得不到有效梯度。难度可按证明步数、所需引理数量、概念组合的跨领域程度等维度量化，但如何自动标注难度本身仍是一个开放问题。
从题目到训练信号的闭环
仅有题目还不够，训练需要可用的信号。一个合理的自动化出题系统通常还需要配套的验证或筛选机制，否则生成的内容可能包含错误陈述或无意义的问题。TheoremSmith 的价值在于把「出题」这一步规模化，为后续的自动求解、验证和强化学习提供原料——这与近年来用可验证奖励训练推理模型的方向相呼应。
可验证奖励（Verifiable Reward） 是近期推理模型训练中的关键概念，代表工作是 OpenAI 的 o1 系列和 DeepSeek广告-R1。其核心思路是：对于数学、代码等有客观判定标准的任务，用自动检查器（如答案比对、单元测试、形式化证明检查器）给出 0/1 或连续奖励，再配合强化学习（如 PPO、GRPO）优化模型。这类方法绕开了昂贵且不稳定的奖励模型（reward model），但前提是存在可靠的验证器。对证明题而言，验证器可以是 Lean、Coq 等形式化证明助手，也可以是另一个能力更强的 LLM 做评审——前者严谨但覆盖有限，后者灵活但可能误判。TheoremSmith 产出的题目要真正进入训练闭环，必须与其中一种验证机制对接。
对 LLM 训练生态的潜在影响
缓解数据瓶颈
公开的高质量数学语料增长缓慢，而模型规模与训练需求持续上升，合成数据因此成为重要补充。自动生成的证明题如果能保证一定的严谨性，就能显著扩充训练集，并覆盖人类出题者较少涉足的领域组合。
评测与训练的双重用途
批量生成的难题也可以作为评测基准的补充。现有基准容易被模型「见过」，而新生成的题目在分布上更陌生，能更真实地反映模型的泛化推理能力。当然，这要求生成机制本身足够多样，避免形成新的模式化偏差。
数据污染（Data Contamination） 指评测集题目在训练语料中出现过，导致模型「背答案」而非真正推理。数学领域已有实证：GSM8K、MATH 等基准的部分题目被发现存在于 Common Crawl 中，模型在其中的高分可能被高估。缓解手段包括动态更新基准、使用私有留出集、以及像 TheoremSmith 这样按需生成新题。但生成式评测也有自身隐患：如果生成器与训练数据同源，新题可能只是换皮，无法真正测出泛化能力；此外，生成题目的正确性若无人复核，评测结论本身就不可靠。
需要冷静看待的问题
自动化出题的难点不在于「生成」，而在于「保证正确与有意义」。证明题的陈述若存在隐蔽错误，训练信号就会被污染；难度若只靠表面复杂度堆砌，也可能产出大量重复或无关紧要的变体。此外，该帖目前仅有 7 个点数、暂无评论，社区验证和实际效果的数据都还很有限。TheoremSmith 能否在规模和严谨性之间取得平衡，还需要更多公开的实验结果来回答。
对于关注 LLM 推理训练的研究者和工程师来说，这类「造题工具」值得持续跟踪——它代表了一种把数据生产本身工程化的思路。
相关推荐
Pi Agent凭什么爆火？极简内核+可扩展的AI编程新思路
Pi Agent 为何在 AI 编程工具赛道脱颖而出？本文解析其极简内核、按需扩展的设计哲学，对比 Cloud Code、Codex 等主流工具的功能膨胀困境，探讨开发者自主控制 agent 的价值与轻量路线的取舍。
Claude Code用量总提前耗尽？7个技巧让额度撑更久
Claude Code额度总提前耗尽？本文整理七个实用技巧：切换到新任务时使用 slash clear、按任务选择Sonnet或Opus、调低effort等级、精简CLAUDE.md、关闭不用的MCP服务器、plan mode先规划、用slash usage定位消耗源头，帮助你延长用量额度的使用时间。
Cursor多智能体协作：浏览器扩展里看AI设计网站
YouTube短视频展示了多光标AI智能体在浏览器中协作设计网站的画面，其载体为浏览器扩展而非独立平台。本文梳理该演示的关键细节、信息缺口及其反映的多智能体协作趋势。