10 月 6 日 OpenAI 放出数百份数学手稿的当天，并没有回避一个尴尬事实：它撤回了 3 份因符号错误出问题的手稿，并修订了 14 份。Implicator 在报道中直接引用官方说法——未形式化的结果「可能有问题」。这个当天纠错的动作，比成果本身更值得停下来想一想：它揭示了一条正在成型的训练路线，即让模型在「可被验证」的压力下，长出机器层面的自我批评。
奖励信号决定模型成为谁
强化学习的基本逻辑是：什么行为被奖励，模型就重复什么。过去模型被奖励「看起来像对的」——语言流畅、论证像模像样，于是它学会了一本正经地胡说。这就是幻觉的训练学根源。
可验证奖励换了一套打分规则：在数学这类领域，答案对不对不看像不像，而看 Lean 类型检查通不通过。模型发现，与其写一段漂亮但不可验的论证，不如写一段哪怕朴素但能被编译器确认的推导。奖励信号一变，行为就跟着变。
自我批评是被结构逼出来的
这背后发生了一件有意思的事：模型开始在产出前自我校验。因为它知道，交上去过不了检查，奖励就是零。于是它学会在内部先跑一遍「审稿」，先自己抓符号错误，再交卷。
这不是模型突然有了良心，而是一种被训练出来的德性：
- 谦卑：它不再对自己的第一版结论深信不疑，而是默认它可能有错。
- 严谨：它偏好可被检验的表述，而不是含糊其辞。
- 可纠错：错了就改，因为改正的成本远低于硬扛。
有意思的是，这些品质在人类科学家身上，我们称之为「学术美德」。
保留与边界
必须说清：可验证奖励只在「有客观判据」的领域成立。伦理、审美、政策判断没有 Lean 式的编译器，模型在这些地方仍然会嘴硬。但数学领域的这个样本至少证明了一件事——求真不是靠叮嘱模型「你要诚实」训出来的，而是靠一个它无法欺骗的打分器，结构性地逼出来的。 道德教诲没用，制度设计有用。