LLM 擅长哪类数学？

原文 ↗ Hacker News 讨论 ↗

大型语言模型正开始帮助形式化数学证明和反例搜索，但它们在许多日常推理任务和混乱的现实世界问题上仍然会失败，例如解释招聘广告或处理开放式逻辑谜题。评论者将 LLM 在模式匹配、代码和定理证明方面、尤其是在明确定义系统中的优势，与它们在通用推理基准、空间理解以及可靠遵循细致指令方面的弱点进行对比。这引发了关于当前系统是否能算“通用智能”、有多少进展来自蛮力搜索加验证，以及未来模型是否真能产出全新的、优雅的数学思想，而不是仅仅给出增量式或蛮力式结果的争论。

LLM 能力范围

  • 许多评论者区分：
    • 在形式化、封闭领域任务上的强表现（数学、代码、形式化证明、Lean）。
    • 在开放式“现实世界”任务上的薄弱且不稳定表现（找工作、通用推理、常识）。

现实任务失败 vs. 提示词质量

  • 有评论者报告，前沿模型在一个看似简单的代理任务上失败：在特定国家寻找自由职业 IT 咨询工作，却把以下概念混淆了：
    • 自由职业 vs. 全职岗位。
    • 工作地点 vs. 中介机构所在地。
  • 其他人反驳称：
    • 所描述的提示词很难解析；实际提示词质量未知。
    • 数据质量和抓取歧义（招聘网站、中介）可能也很重要。
  • 更广泛的一点是：面向混乱现实工作流的端到端 LLM 代理仍然脆弱，需要分解为可验证的流水线。

推理基准与局限

  • 引用的基准（General365、ARC‑AGI‑3）显示：
    • 在控制背景知识的情况下，前沿模型在多样化推理任务上的得分远低于人类。
    • 示例谜题对人类来说也极其困难；一些人认为 60% 以上的准确率已经很厉害，另一些人则把这看作反对“AGI”的证据。
  • 另一条批评线是：LLM 很容易被无关上下文分散注意力；更长、更啰嗦的提示词可能适得其反。

数学、证明，以及“蛮力” vs 直觉

  • 关于近期 LLM 辅助数学成果的讨论强调：
    • 大量使用生成并测试、许多子代理、成千上万的脚本/命令。
    • 有些人认为这只是包装得更好看的蛮力搜索；另一些人则把它看作类似进化的迭代式启发搜索。
  • 人们对 LLM 的看法是：
    • 在穷举情况、寻找反例、并在配合验证器/SAT 求解器时生成冗长形式化证明方面非常出色。
    • 但目前还不明显具备提出新的、深层次“优雅”概念的能力（例如傅里叶变换的类比）。

智能、AGI 与信任

  • 一派认为：
    • 广泛的世界知识 + 模拟推理 + 跨领域迁移，已经达到他们个人对“AGI”的标准。
  • 批评者回应：
    • 在儿童级抽象任务上的失败以及实际场景中的脆弱性，与这一说法相矛盾。
    • 真正的 AGI 需要在没有人类安全网的情况下，被信任承担高风险工程（桥梁、飞机、战争），而这与当前现实相差甚远。
  • 几个人指出，人类专家仍然既需要引导 LLM，也需要验证结果；普通用户很少能取得突破。

元观察

  • LLM 被描述为能够生成“看起来像人类的推理轨迹”的强大生成器，从而提升随机搜索，但：
    • 它们在系统性的多步推理上仍然容易出错，尤其是在长链推理或并发/时序逻辑中。
    • 人们担心机器生成的证明和结果会大量涌现，而只有极少数专家社区能够验证。