MechAlign：评估数学形式化中的项目级语义对齐

MechAlign 用依赖图加 LLM 审查形式化陈述与论文原意是否对齐。

资讯摘要

论文提出 MechAlign 框架，用于项目级语义对齐审查，结合形式依赖提取与基于 LLM 的评估。其提取工具 LeanTrace 从已展开声明构建陈述依赖图，保留定义体与结构约束，排除证明体并在显式库边界处停止。作者对 OpenAI Math 的 173 个项目中的 201 个主要结果做了初步审查，并构建含 501 条固定三元组的 LeanReviewBench。

要点速读

1. LeanTrace 从已展开声明构建陈述依赖图，保留定义体与结构约束，排除证明体并在显式库边界处停止。
2. 作者对 173 个 OpenAI Math 项目的 201 个主要结果进行初步审查，使用提供的非形式描述与可用论文上下文。
3. 作者构建 LeanReviewBench，包含来自 OpenAI Math、费马大定理与 Kakeya 的 501 条固定 claim-statement-context 三元组，并记录描述来源。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/28 08:00:17（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。