大模型为何难成为「数学家」？斯坦福等揭示严谨证明中的结构性弱点

另一方面，当前主流的大语言模型是在海量自然语言上训练出来的。它们虽然无法直接生成可被形式系统接受的机器检查证明，却在 "非形式化推理" 方面表现出色 —— 也就是说，它们往往能给出看似合理、直觉对路的答案，并模仿人类在解决问题初期的思维方 式。这种能力虽然不符合传统意义上的形式证明要求，但在探索性的数学过程中具有重要价值。 为此，斯坦福大学、加州大学伯克利分校与麻省理工学院的研究团队提出了一种创新方法：将不等式证明任务拆解为两个 "非形式化但 可验证" 的子任务，即 "界限估计" 和 "关系预测"，并基于此构建了第一个奥林匹克级不等式证明基准数据集 ——IneqMath。这一框 架提供了一种介于完全形式化验证与自然语言生成之间的 "中间层"，可以逐步审查模型的推理链条，从而判断其是否真正掌握了推理 结构，而不仅仅是在猜测答案。 这正是当前形式化数学所试图解决的问题。近年来，Lean、Coq 等系统为数学提供了严格可验证的推理机制，每一步推导都必须符合 逻辑规则，可被计算机检验。然而，这类系统对语句的表达精度要求极高，建模成本大、自动化程度有限，尤其在面对中学到奥数级别 的不等式问题时，很难做到规模化应用。 使 ...