arXiv · cs.AI · Eric Jiang, Xiao Liang, Junyi Zhang, Justin Baker, Zhi Zhang, Yingjia Wan, Yubei Li, Jinxi Yu, Mengting Li, Haikang Deng, Alexander Taylor, Rushil Raghavan, Michael Simon, Hyunsik Chae, Jia-Chen Gu, Xinjie He, Kyle Hess, Ethan Ji, Yiwen Kou, Tzu-Han Lin, Jiachen Lu, Jack Mauro, Vigyan Sahai, Zheng Tan, Alexander Taylor, Junkai Zhang, Kyle Zheng, Lunji Zhu, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang · 6 小时前模型评分38
从解题器到研究智能体：大语言模型驱动的形式化数学如何走向研究前沿
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
导读
一篇立场论文系统梳理了大语言模型驱动的定理证明器在形式化数学中的进展，指出当前系统仍难以发现新定理或解决开放猜想，主张下一步应从预设问题求解器转向能处理前沿数学挑战的研究智能体。论文从数据集、自动形式化、证明合成等方面回顾该领域，并分析了现有系统在研究级任务上的核心局限，给出未来路线图。
分类置信度
中 · 待人工复核
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
应用领域：科学研究
事件类型：研究发布
证据摘录
- “In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.”
来源：arXiv · cs.AI · arxiv.org