arXiv cs.AI· Tiancheng Xu, Wensheng Yu·· 10 小时前AI 评分34
Megrez：面向 MK 集合论形式数学的知识引导智能体
Megrez: A Knowledge-Guided Agent for Formal Mathematics over MK Set Theory
AI 导读
Megrez 是面向基于 Morse–Kelley（MK）集合论的 Rocq 库的知识引导形式化智能体，通过知识图谱、1–5 步 tactic 短爆发证明循环与三重验收流水线协同通用编码智能体。在点集拓扑语料上的部署与评估显示，它实现了有效的跨章节形式化与可扩展的前提检索。
正文 · AI 翻译
摘要：配备证明助手工具的通用编程智能体在独立的竞赛问题上已展现出强劲性能，但在低资源数学库内进行累积式教材形式化仍面临三大障碍：将教材概念与库中声明对齐、使长程搜索与实时证明状态保持同步，以及将本地验证的证明可靠地集成到不断增长的代码库中。我们提出 Megrez，一个面向基于 Morse--Kelley（MK）集合论的 Rocq 库的知识引导形式化智能体。Megrez 通过三种机制协调通用编程智能体：（1）一个可溯源重建的知识图谱，融合形式声明、编译器引用与精选元数据，以支持通过中文别名、概念簇、证明依赖和多通道全文排序进行检索；（2）一个反馈驱动的 1--5 步策略短促证明循环，配合目标局部支路账本与指数间隔结构化反思；（3）一个三重检查验收流水线（陈述保真度、公理审计与完整构建），并搭配多语料 Provider 栈与候选绑定的可恢复批处理状态机。在点集拓扑语料上的部署与评估表明，其能够有效进行跨章节形式化并实现可扩展的前提检索。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2611.13613 [cs.AI] |
| （或 arXiv:2611.13613v1 [cs.AI] 为本版本） | |
| https://doi.org/10.48550/arXiv.2611.13613 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Tiancheng Xu [查看邮箱]
[v1]
2026年11月10日星期二 05:42:16 UTC（21 KB）
来源：arXiv cs.AI · arxiv.org