arXiv · NLP· Jiaxin Yuan, Udari Madhushani Sehwag, Connor Martinez Lockhart, Xiaoyu Liu, Shayan Shabihi, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlassis Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Mohamed, Bilal Aytekin, Jiewen Lang, Zezheng Song, Furong Huang·· 6 小时前AI 评分35
MathAdv 基准揭示定理证明器在形式化与鲁棒性上的瓶颈
MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
AI 导读
MathAdv 是一个涵盖 13 个数学领域的诊断基准，旨在通过 Lean 4 定理证明及三项辅助任务评估模型能力。该基准发现形式化过程是主要瓶颈，且数学等价的命题改写会暴露模型显著的鲁棒性局限。这种组件式评估揭示了聚合准确率所掩盖的具体失败模式，并开源了数据集与脚本。
来源：arXiv · NLP · arxiv.org