TREAT 基准：大模型在等价数学变换下识别定理能力不足

arXiv 近日发布一项面向大模型数学推理能力的研究，提出 TREAT（Theorem Recognition Evaluation Across Transformations）基准，用于衡量大模型在「等价数学变换」下识别定理的能力。研究指出，当前 AI 系统常需要在灵活的输入表示与下游工具所使用的形式化对象之间转换，能否识别一个「陌生表述」背后指向同一已知定理，构成了一项关键挑战。

核心思路：从文本改写到形式变换

与多数依赖自然语言改写的定理理解评测不同，TREAT 直接改变定理条件本身的数学形式，包括残余方程、见证语句、优化恒等式、集合关系、算子形式以及证明中间刻画等多种变换方式。研究从抓取的定理页面出发，筛选具有可用数学表达式的条目，提取规范的定理条件，并生成保留假设与逆映射的变换变体。

数据规模与评测结果

最终构建的语料包含 737 个定理身份与 29,480 行变换样本。测试结果显示，表现最好的模型仅在 60.73% 的情况下能正确检索到对应定理身份，其余系统则暴露出弃答、错误检出以及输出格式异常等不同失败模式。作者据此指出，大模型对定理知识的掌握在等价变换下呈现明显脆弱性。

意义与适用范围

TREAT 提供了一个受控的测试环境，可用于评估模型在「表征层面保持稳定」的前提下访问形式化知识的能力。该基准的应用场景涵盖需要稳定目标对象、显式等价关系、校验流程与可复核打分机制的领域，例如自动定理证明、形式化数学工具链以及数学检索增强系统等。