陶哲轩对 AI 的抱怨
看来陶哲轩对当前 AI 并不满意 😅
- 写 Lean（一种机器证明语言） 时 copilot 补全的有一半是不可用的 （他用的 rubbish）
- 用 AI 查找数学文献经常幻觉，甚至完全捏造文献（他说 Nonsense，Garbage）
- 他想让 AI 按他的思路证明数学问题，AI 听不懂他的证明思路，还跟他辩论（他用了 exhausting）
- AI 越聪明它的证明的错误越难发现，这些证明初看起来都是对的，但是仔细看会发现犯的错误却都非常愚蠢，而且 AI 还没有自我反思和纠错的能力。 (他用的 “Annoying，Stupid ”）
- 他还说之前谷歌的 AlphaProof 银牌也有“吹嘘”的成分， 它是多个 SOTA 模型的混合系统， 一道题需要 3 天谷歌服务器时间（应该是类似 AlphaGo 的 MCTS 搜索）这让 AlphaProof 无法拓展。
AI 需解决的关键挑战
- 学会规划能力，模型需要学会将大问题分解成小问题，先证明关键引理，再完成主定理证明。
- 解决复杂的数学问题需要不断试错，现在 AI 能接触到的更多是成功案例，人类也没有积累数学家的解体试错数据，这让 AI 不能像数学家一样试错，也就无法通过试错找到解题方法。
- 现在的 AI 没有 数学嗅觉（Mathematical Smell），数学家的数学嗅觉可以用来快速判断一个证明思路是否有前途，减少不必要探索。 他用 AlphaGo 对局势评估能力类比数学嗅觉。
- 解决复杂数学问题往往需要开辟一个新领域，AI 需要在解题的过程中学会 归纳，抽象，发明新概念，并且还要坚信使用这些新概念能解决问题。
后记：人类智力最后的堡垒
陶哲轩说的这些确实暴露了目前 AI 的一些局限性。 尽管 AI 也在日新月异的进化，诸如“研究生级”、“博士级”、“诺贝尔级”AI的概念不断涌现，这些多少有吹嘘的成本，即使是真的，数学作为人类最复杂的智力活动，要被突破可能还很遥远， 甚至，数学可能可以做为人类智力最后的堡垒。
人类的形式科学发展至今，大部分知识其实只靠人类自己只要给足够的时间，任何“短描述”的知识都有机会被发现或者已经被发现过了，剩下的问题其推理链会越来越长。。 也就是说对人类来说真正有难度的是那些需要经过漫长推理的知识，这些知识的发现往往还需要大量的创新技巧，这些才是我们最希望 AI 解决的，也是 AI 能发挥最大价值的地方，但现在AI处理起来似乎也最力不从心，一点也没有能解决的迹象。
数学新发现需要创新的方法，有着超长的推理链，可能只有当数学完全被突破了，人类智力的“计算搜索功能”才能算正式退出历史舞台。倒是并不一定要解决陶哲轩说的所有问题，能解决 长链推理 或者能自主发现创新方法就很有用了，也是通往 AGI 的必经之路。