**超越编译：评估自然语言到 Lean 声明形式化的忠实度**

_Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization_

> 研究指出仅依赖 Lean 编译无法准确验证声明形式化的忠实度。通过引入双 LLM 裁判与人类审计，发现编译通过率与实际语义正确率存在显著差距，且现有单轮系统的大部分“未通过”实为裁判误判。工具增强型智能体虽提升了编译成功率，但仍有近半数增益因语义不符而被否决。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-10-21 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2606.31002)