arXiv cs.CL· Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao·· 12 小时前AI 评分31
MechAlign：评估数学形式化中项目级语义对齐的框架
MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
AI 导读
MechAlign 是一个结合形式化依赖提取与 LLM 评估的项目级语义对齐审查框架，其提取工具 LeanTrace 从已展开声明构建陈述依赖图，保留定义体与结构约束、排除证明体并在显式库边界处停止。
正文
Abstract:Lean verifies that a formal proof establishes its stated proposition under declared assumptions, but does not check whether that proposition faithfully expresses the mathematical claim in a manuscript. Assessing this correspondence requires interpreting the main theorem through its project dependencies, which may be scattered throughout a large development. We introduce MechAlign, a framework for project-level semantic alignment review that combines formal dependency extraction with LLM-based assessment. Its extraction tool, LeanTrace, constructs a statement dependency graph from elaborated declarations, retaining definition bodies and structure constraints while excluding proof bodies and stopping at an explicit library boundary. The reviewer uses this context to investigate alignment and report discrepancies with localized evidence. We conduct a preliminary review of 201 main results from 173 OpenAI Math projects, using supplied informal descriptions and available paper context. A hyperbolic-group case illustrates how dependency inspection localizes a missing dimensional constraint relative to the manuscript, consistent with the upstream declaration of formalization scope. We also construct LeanReviewBench, comprising 501 fixed claim-statement-context triples from OpenAI Math, Fermat's Last Theorem, and Kakeya, with description provenance recorded. The resource supports controlled comparisons of more project-level semantic alignment evaluations.
| Subjects: | Computation and Language (cs.CL) |
| Cite as: | arXiv:2610.35269 [cs.CL] |
| (or arXiv:2610.35269v1 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2610.35269 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Ruichen Qiu [view email]
[v1]
Mon, 26 Oct 2026 11:44:26 UTC (2,385 KB)
来源：arXiv cs.CL · arxiv.org