TREAT：评测等价数学表示下的形式化知识访问

AI系统日益运行在灵活的输入表示与下游工具所使用的形式化对象之间。一个关键挑战是识别不熟悉的表述何时指代已知的形式化对象。我们通过定理识别来研究这一挑战：给定定理条件的一个保等价变换，模型必须恢复与标准陈述相关联的定理身份。我们提出TREAT，一个评测大语言模型能否从保等价的公式级变换中恢复已知定理身份的基准。TREAT并非改写定理文本，而是改变定理条件本身的数学形式，通过残差方程、见证陈述、优化恒等式、集合关系、算子形式和证明中间刻画来表达已知结果。从抓取的定理页面出发，我们筛选出具有可用数学表达式形式的条目，提取规范定理条件，并生成记录了假设与逆映射的变换变体。最终语料库包含737个定理身份和29,480行变换数据。在测试面板上，最佳模型仅在60.73%的情形中检索到正确的定理身份。其他系统则呈现不同失败模式，包括弃答、误判和格式错误输出。这些表明，定理知识在表示的等价变化下可能很脆弱。因此，TREAT为评测表示稳健的形式化知识访问提供了受控测试床，对需要稳定目标对象、显式等价关系、验证流程和可审计评分的领域具有更广泛的意义。