批评者拆解 OpenAI IMO 路线:LLM 引擎为主,harness 谈不上符号方法
IonelChiosa · x · 2026-10-07
@IonelChiosa 回应 Gary Marcus 的「神经符号」论断,给出详细反驳:
- harness 并非必需:几乎每次生成完整解答后,一个简单 harness(如 fable 在简单循环里)就能不用 Lean 抓住错误
- 流程只有一次生成:一条自然语言最终解答,之后自动形式化——不是基于过滤的证明搜索,只是健全性检查式翻译
- 「符号」标签名不副实:形式化步骤只有几行 harness 代码,引擎显然是 LLM
他打赌 Claude 现在就能不用 harness 解出今年全部 IMO 题,未来 AI 无需任何人类设计的 harness 也能复现 OpenAI 这类成果。