Gary Marcus 评 OpenAI 数学新成绩：符号 AI 起了关键作用

Gary Marcus 在 X 上点评 OpenAI 最新数学成绩，指出系统在 LLM 之外还用了 Lean 等符号 AI 工具做验证。他认为这印证了自己多年主张的神经符号结合路线，但不等于实现 AGI，因为符号验证和符号数据增强无法推广到开放的现实世界。他重申 2019 年的观点：神经符号 AI 必要但不充分，世界模型同样关键。