[LG]《Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics》X Zhai, X Chen, Y Wang, R Zhou… [University of Washington] (2026)

在形式化数学中，非形式证明到机器可检验代码的转化是瓶颈。LLM能生成自然语言证明，但现有系统要求直接映射到Lean/Rocq这样的低阶证明器，迫使模型同时处理：符号查询、类型强制、偏函数侧条件、库引理选择。这些非局部决策无法从自然语言表面推断，导致转化失败时返回单一的accept/reject信号，用户无法定位具体障碍。

本文的核心洞见是：将自动形式化分解为两层。不让LLM直接跳到Lean，而是引入Visored——一个中间表示，其表面是数学自然语言（CNL），其核心将隐含决策（类型、强制、侧条件）显式化为可检验的工作项。由此，将单一的全局检验拆分为逐步局部检验，每一步失败都返回具体位置的诊断。

这项工作真正留下的遗产是证明工程的设计模式转变：从"让模型学会目标语言"转向"让中间层吸收语言鸿沟"。它为后来者打开的新门是将CNL作为LLM的第一公民接口——自动形式化、密集奖励信号生成、数据合成——而非仅作UX层。尚未跨过的门槛是透明的大规模Lean排放（当前中位膨胀250倍）和超竞争基准的覆盖（IMO问题仅35%）。

arxiv.org/abs/2606.17581 机器学习 人工智能 论文 AI创造营