Megrez：基于 MK 集合论的知识引导形式化数学智能体
Megrez: A Knowledge-Guided Agent for Formal Mathematics over MK Set Theory
AI 导读
研究者提出 Megrez，一个面向 Rocq 库、基于 Morse--Kelley（MK）集合论的知识引导形式化智能体。它通过三个机制协调通用编码智能体：可源码重建的知识图谱（支持中文别名、概念簇、证明依赖检索和多路全文排序）、反馈驱动的 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