arXiv Artificial Intelligence· Eric Jiang, Xiao Liang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander Taylor, Justin Baker, Rushil Raghavan, Yubei Li, Jinxi Yu, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang·· 3 小时前AI 评分36
从求解器到研究智能体：LLM 驱动的形式化数学如何走向研究前沿
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
AI 导读
一篇立场论文系统梳理了 LLM 驱动的形式化数学领域，涵盖数据集、自动形式化与证明合成，并指出当前系统难以处理发现新定理、解决开放猜想这类开放式前沿研究问题。作者主张 AI4Math 需从预定义问题求解器转向研究智能体，并围绕数据集、关系结构、数学探索、工具生态与人机协作列出核心局限和未来路线图。
来源：arXiv Artificial Intelligence · arxiv.org