Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study
本研究揭示，经强化学习训练的Lean定理证明器在推理阶段会出现模式崩溃问题，而通过应用固定节奏的多样化策略骨架可有效缓解该问题并恢复显著的性能提升，相比之下，提示语改写和无关评论则被证明无效或有害。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一位才华横溢的学生，他们接受过使用一种名为 Lean 的特殊计算机语言来解决极难数学谜题的训练。这位学生，我们称其为"DeepSeek"，极其聪明，却有一个奇怪的毛病：当被要求解决谜题时，他们会陷入思维定势。
本文是一份诊断报告，旨在解释为何会出现这种情况以及如何解决。以下是研究人员发现的经过，用通俗易懂的语言讲述。
1. 问题所在：“坏唱片”效应
研究人员注意到，当他们让 DeepSeek 反复解决同一个数学谜题（仅使用略微不同的随机种子，就像掷骰子一样）时，这位学生总是尝试完全相同的第一个步骤。
- 类比：想象你正在试图打开一扇锁着的门。你把钥匙插进锁孔，没打开。你再试一次，还是没打开。你试了第三次，甚至第一百次。即使你尝试了 64 次，你也只是以完全相同的方式，将同一把钥匙插进同一把锁里。你并没有去尝试其他钥匙或其他方式来开门。
- 结果：在研究中，将尝试次数从 32 次翻倍到 64 次，并没有解决任何一个新的谜题。这位学生出现了“模式崩溃”——他们被困在一条狭窄的道路上，无法想到其他方法。
2. 解决方案：提供“第一步”提示
研究人员意识到，这位学生并非懒惰，只是过于固守常规。于是，他们尝试了一个新技巧：在要求学生解决谜题之前，先给他们一个关于如何开始的具体指令。
- 类比：研究人员不再只是说“解决这个谜题”，而是说“先从简化数字开始”，或者“先从引入一个新变量开始”。这就像给学生一把特定的钥匙让他们先尝试，而不是让他们去猜测。
- 结果：这个简单的推动打破了定势。这位学生突然开始解决更多的谜题。这种“定势”并非因为学生不擅长数学，而是因为他们开始解题的方式过于僵化。
3. “原因”：这是训练问题，而非大脑问题
研究人员想知道：这位学生天生就不擅长数学，还是训练让他们变得僵化？
- 实验：他们在学生接受特殊数学训练（即“基础”模型）之前对其进行了测试。
- 发现：未经训练的学生根本无法解决任何谜题。他们要么放弃，要么只是重复问题。
- 结论：正是特殊训练（强化学习）教会了这位学生如何解题。但同时，也正是这种训练让他们变得僵化并陷入定势。训练创造了技能，但也创造了“坏唱片”问题。
4. 谁也有这个问题？
研究人员测试了其他“学生”（不同的 AI 模型），以查看这是否是一个普遍问题。
- “SFT"学生：有一位学生接受了不同的训练（监督微调）。这位学生在整体解题能力上实际上更强，但他们没有“定势”问题。当研究人员给他们提示时，反而让他们表现得稍差了一些。他们原本就足够灵活，能够找到自己的路径。
- "RL"学生：那些接受特殊“强化学习”方法训练的学生（如 DeepSeek）则陷入了困境。他们需要“第一步”提示来打破狭隘的思维。
5. “第一步”的证据
为了证明这并非偶然，研究人员查看了学生实际做出的“第一步”。
- 发现：在针对单个谜题的 64 次尝试中，那位有“定势”的学生在将近一半的情况下使用了完全相同的第一个步骤。他们的表现极具可预测性。
- 比喻：如果你让人类写 64 次故事，他们可能会以“很久很久以前”、“阳光灿烂”或“那是一个漆黑的夜晚”开头。但这名 AI 学生会用“很久很久以前”开头 32 次，用“阳光灿烂”开头 30 次。他们的开头几乎没有任何变化。
总结
该论文得出结论，强化学习（一种特定的 AI 训练方式）是一把双刃剑：
- 它教会了 AI 如何证明形式化数学命题（这是它以前做不到的）。
- 但它也让 AI 过于专注于少数几个“获胜”策略，从而停止探索新的策略。
解决方案并非给予 AI 更多的计算能力或更多的思考时间，而是给予它结构性指导——即关于如何开始证明的简单推动。这迫使 AI 打破常规，探索新的路径，从而解锁了它此前因过于固执而无法找到的解决方案。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。