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 短爆发证明循环与三重验收流水线协同通用编码智能体。在点集拓扑语料上的部署与评估显示，它实现了有效的跨章节形式化与可扩展的前提检索。
正文 · 原文
Abstract:General-purpose coding agents equipped with proof-assistant tools have shown strong performance on standalone competition problems, yet cumulative textbook formalization inside a low-resource mathematical library still faces three obstacles: aligning textbook concepts with library declarations, keeping long-horizon search synchronized with live proof states, and integrating locally verified proofs reliably into a growing codebase. We present Megrez, a knowledge-guided formalization agent for Rocq libraries built on Morse--Kelley (MK) set theory. Megrez coordinates a general coding agent through three mechanisms: (1) a source-rebuildable knowledge graph merging formal declarations, compiler references, and curated metadata to support retrieval via Chinese aliases, concept clusters, proof dependencies, and multi-lane full-text ranking; (2) a feedback-driven 1--5 tactic short-burst proving loop paired with a goal-local branch ledger and exponential-interval structured reflection; and (3) a three-check acceptance pipeline (statement fidelity, axiom auditing, and full builds) coupled with a multi-corpus Provider stack and a candidate-bound recoverable batch state machine. Deployment and evaluation on a point-set topology corpus demonstrate effective cross-chapter formalization and scalable premise retrieval.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.13613 [cs.AI] |
| (or arXiv:2611.13613v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2611.13613 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Tiancheng Xu [view email]
[v1]
Tue, 10 Nov 2026 05:42:16 UTC (21 KB)
来源：arXiv cs.AI · arxiv.org