计算机科学逻辑的理论级自动形式化

arXiv cs.LG 论文
auto-formalization formal-verification lean theorem-proving benchmark computer-science logics

摘要

引入LCS-Bench，这是一个基于计算机科学逻辑的理论级自动形式化基准，覆盖327个教科书条目、4,076个Lean声明。对14个模型的评估表明该基准具有挑战性，最先进模型在自动形式化任务上仅达到20.1%。

arXiv:2606.26525v1 公告类型：新 摘要：自动形式化对于可扩展的形式化验证至关重要，但现有进展主要集中于孤立语句，而理论级自动形式化（即连贯地翻译数百个相互依赖的定义、引理和定理）由于在一致性、忠实性、可扩展性和正确性方面存在挑战，仍是一个未解决问题。本文中，我们引入了LCS-Bench，这是一个基于《计算机科学逻辑》的独立理论级基准。LCS-Bench通过一种新颖的半自动化智能体流水线构建，该流水线利用概念图、形式签名规划、问题追踪、通过反例搜索填充待证明项，并辅以人类专家的忠实性审查。生成的成果覆盖327个教科书条目、超过4,076个Lean声明以及超过85,000行Lean代码。该数据集通过一个数据引擎自动衍生出五个评估基准轨道，用于衡量自动形式化和定理证明能力的不同方面，从而支持广泛的评估。我们还引入了一种新颖的评估协议，包含定义等价性检查器，能够进行更细粒度和更忠实的评估。通过对14个模型的广泛评估，我们证明了：(1) LCS-Bench具有高质量、一致性和忠实性；(2) 该基准具有挑战性，最先进模型在自动形式化任务上仅达到20.1%；(3) 我们的分析揭示了关于理论级自动形式化的关键发现，并为未来工作提出了有前景的方向。
查看原文
查看缓存全文

缓存时间: 2026/06/26 05:20 

# 计算机科学逻辑的理论级自动形式化
来源：https://arxiv.org/abs/2606.26525
查看PDF (https://arxiv.org/pdf/2606.26525)

> 摘要：自动形式化对于可扩展的形式验证至关重要，但现有进展主要集中于孤立语句，而理论级自动形式化——即连贯地翻译数百个相互依赖的定义、引理和定理——由于在一致性、忠实性、可扩展性和正确性方面的挑战，仍是一个开放问题。本文提出了LCS-Bench，一个基于计算机科学逻辑的独立理论级基准。LCS-Bench通过一种新颖的半自动化智能体流水线构建，该流水线利用概念图、形式化签名规划、问题追踪、带反例搜索的sorry填充，并辅以人类专家的忠实性审查。生成的成果涵盖了327个教科书条目、超过4,076个Lean声明以及8.5万余行Lean代码。该数据集通过一个数据引擎支持广泛的评估，该引擎自动派生五个评估基准轨道，衡量自动形式化和定理证明能力的不同方面。我们还引入了一种新颖的评估协议，包含定义等价性检查器，能够实现更细粒度且更忠实的评估。通过对14个模型的广泛评估，我们证明了：(1) LCS-Bench质量高、一致且忠实；(2) 该基准具有挑战性，最先进的模型在自动形式化任务上仅达到20.1%；(3) 我们的分析揭示了关于理论级自动形式化的关键发现，并为未来工作指明了有前景的方向。

## 提交历史

来自：Ziyang Li [查看邮件](https://arxiv.org/show-email/44c6f5a4/2606.26525) **\[v1\]** 2026年6月25日星期四 01:59:53 UTC (3,093 KB)

相似文章

理论级别的自动形式化：从孤立陈述到统一形式知识库

arXiv cs.AI

这篇立场论文主张理论级别的自动形式化，即将包括公理、定义和引理在内的整个理论形式化为一致的库，而不是孤立的陈述。它讨论了这种转变的重要性、不同观点、开放挑战，并为形式化研究中的这一转变提出了前进方向。

FaithformBench：数学思维链自动形式化的忠实度基准

arXiv cs.CL

介绍了FaithformBench，一个用于评估数学思维链自动形式化系统忠实度的基准，通过测量扰动步骤上的有效性与无效性保持来评估。应用于八个AF系统后，揭示了普遍的“谄媚”现象，即无效输入被静默纠正。

MathAtlas：野外自动形式化基准测试

arXiv cs.AI

MathAtlas 是一个针对研究生级别数学的自动形式化的大规模基准测试，包含从103本教科书中提取的约5.2万个定理和定义，并附带一个包含约17.8万条关系的数学依赖图。实验表明，最先进的模型正确率最高仅为9.8%，凸显了其难度。