大模型推理能力

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels

FATE：面向多难度层级的前沿代数形式化基准系列

Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailin Guan, Peihao Wu, Chunbo Dai, Liang Xiao, Bin Dong

机构 * Westlake Institute for Advanced Study, Westlake University（西拉丘学院先进研究院，西拉丘大学） ； Peking University（北京大学） ； New Cornerstone Science Laboratory, School of Mathematical Sciences, Peking University（新基石科学实验室，北京大学数学科学学院） ； Center for Machine Learning Research, Peking University（机器学习研究中心，北京大学） ； Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University（智能计算中心，大湾先进研究院，大湾大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.AI、cs.LG

AI总结 FATE是一个面向多难度层级的前沿代数形式化基准系列，旨在评估和推动高级数学推理能力。

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Elenchus：从证人-怀疑者对话生成知识库

Bradley P. Allen

机构 * University of Amsterdam（阿姆斯特丹大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.CL、cs.AI

AI总结 Elenchus通过证人-怀疑者对话与LLM交互，利用非单调多后件逻辑显式化知识库构建，实现从对话到形式推理的端到端整合。

Comments 12 pages, 4 figures, 4 tables

Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

Agent Hunt: 基于奖金的协作自动形式化与LLM代理

Chad E. Brown, Cezary Kaliszyk, Josef Urban

专题命中 代码与定理证明 ：planning(abstract)；分类 cs.AI

AI总结 基于奖金的协作自动形式化方法，利用LLM代理在交互式定理证明环境中进行去中心化证明搜索与理论构建。