Gary Marcus 评 OpenAI 数学新成绩：符号 AI 起了关键作用
Gary Marcus 拆解了 OpenAI 数学成绩背后的门道，说其实靠 Lean 符号验证撑着，顺带回应了关于他的各种争议说法。
Gary Marcus 在 X 上点评 OpenAI 最新数学成绩，指出系统在 LLM 之外还用了 Lean 等符号 AI 工具做验证。他认为这印证了自己多年主张的神经符号结合路线，但不等于实现 AGI，因为符号验证和符号数据增强无法推广到开放的现实世界。他重申 2019 年的观点：神经符号 AI 必要但不充分，世界模型同样关键。
since many people are asking me about the new math results from OpenAI, here is my take. 1. It uses symbolic AI (Lean, etc) in addition to LLMs which is what i said for years we would need to do; this this confirms what I actually said (as opposed to various fictitious misrepresentations that run rampant around here ) 2. It still doesn’t mean they have AGI; the math stuff AFAIK does not generalize broadly, because you can’t use the same symbolic verification (and symbolic data augmentation techniques) in the open-ended real world. So yes I do feel vindicated wrt to neurosymbolic AI but no the G in AGI (general) is not yet solved. What I said in 2019 remains true: neurosymbolic AI is necessary but not sufficient; world models are also key. Hans @hansaFL So what do you think @GaryMarcus , just another brick in the wall? 🔗 View Quoted Tweet 💬 6 🔄 4 ❤️ 20 👀 2146 📊 7 ⚡
