发布MathAdv诊断性数学推理基准

1. 12:00
   arXiv · NLP

   MathAdv 基准揭示定理证明器在形式化与鲁棒性上的瓶颈

   MathAdv 是一个涵盖 13 个数学领域的诊断基准，旨在通过 Lean 4 定理证明及三项辅助任务评估模型能力。该基准发现形式化过程是主要瓶颈，且数学等价的命题改写会暴露模型显著的鲁棒性局限。这种组件式评估揭示了聚合准确率所掩盖的具体失败模式，并开源了数据集与脚本。

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。