arXiv · NLP· Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao·· 4 小时前AI 评分20
MechAlign：评估数学形式化中项目级语义对齐的框架
MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization
AI 导读
MechAlign 提出项目级语义对齐审查框架，结合形式依赖提取工具 LeanTrace 与基于大语言模型（LLM）的评估机制。 LeanTrace 从 elaborated declarations 构建语句依赖图，保留定义体与结构约束，排除证明体并在显式库边界处停止。 该框架在 201 个主结果上进行了初步审查，并构建了包含 501 个三元组的 LeanReviewBench 数据集。
来源：arXiv · NLP · arxiv.org