主要来源arXiv: OpenAI
查看原文事件专题 ·官方一手
MechAlign：用 LLM 审查 Lean 数学形式化的项目级语义对齐
Lean 只能验证形式化证明在其声明假设下成立，无法判断命题是否忠实表达了论文中的数学断言。MechAlign 框架结合其提取工具 LeanTrace 构建语句依赖图，再由 LLM 在该上下文中检查对齐并给出带定位证据的差异报告。团队对来自 173 个 OpenAI Math 项目的 201 个主要结果做了初步审查，并以双曲群案例展示了依赖检查如何定位缺失的维度约束。论文同时发布了 LeanReviewBench，包含来自 OpenAI Math、Fermat's Last Theorem 和 Kakeya 的 501 个固定 claim-statement-context 三元组。
当前结论
有人给 Lean 形式化做了个语义对齐检查器，用依赖图让 LLM 找形式化定理和论文原文的出入，还放了个 501 条的基准。
11 个信源34° AI 热度最后更新 2026/10/26 11:44:26
证据链
11 个信源冲突核查
现有去重数据只说明这些来源讨论同一事件，不代表立场相同。当前没有结构化的支持或反驳证据，不自动推断冲突。