arXiv · cs.AI · Jiaxin Xie, Guowei Dou, Xiang Ji, Wensheng Yu · 12 小时前模型评分36
MFF-Agent：面向多数学领域的数学基础形式化智能体
Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations
导读
研究者提出通用智能体 MFF-Agent，将大语言模型（LLM，Large Language Model）的推理能力与 Rocq 证明助手的验证能力结合，用于数学基础的形式化。该智能体通过任务分类、工具辅助执行、验证反馈和基于状态的任务管理，支持形式化证明的生成、改进与验证，并在 Morse–Kelley 集合论、实数、命题逻辑和选择公理等价性等案例中检验了跨领域适用性。
分类置信度
中 · 待人工复核
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
应用领域：科学研究
事件类型：研究发布
证据摘录
- “This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains.”
来源：arXiv · cs.AI · arxiv.org