🤖 AI

Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

本文介绍了 Visored，这是一个基于依赖类型的证明器，它通过使用类自然语言的接口和规则驱动的自动化技术将证明转换为经过检查的 Lean 文件，从而在大型语言模型生成的数学内容与形式化验证之间搭建桥梁，并在无需专门训练的情况下在 miniF2F 基准测试中展示了有效的性能。

原作者： Xiyu Zhai, Xinyi Chen, Yiping Wang, Runlong Zhou, Liao Zhang, Simon S. Du

发布于 2026-06-17

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Xiyu Zhai, Xinyi Chen, Yiping Wang, Runlong Zhou, Liao Zhang, Simon S. Du

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在试图教导一名才华横溢但略带“幻觉”倾向的学生（一个 AI）如何编写数学证明。这个学生擅长用直白的英语讲述证明的“故事”，但他们经常会跳过那些严谨的数学老师认为必须看到的、微小且枯燥的细节。

目前，如果你要求这个学生用一种严格的、计算机可读的语言（如 Lean）来编写证明，他们往往会陷入困境。他们不知道该选择哪一个具体的“库规则”，或者会搞错像“不能除以零”这样微小的细节。

Visored 是一个旨在解决这一问题的全新工具。它作为一个翻译器和安全网，位于学生的自然语言与严格的计算机语言之间。

以下是它的工作原理，通过几个类比来解释：

1. “受控自然语言”（剧本）

Visored 并没有强迫 AI 直接编写像 Lean 那样僵硬、类似代码的语言，而是让 AI 使用一种受控版本的英语进行编写。

类比： 这就像是一个“填词游戏”（Mad Libs）风格的剧本。AI 不被允许随心所欲地书写；它必须使用特定的句子模板，如“设 x 为...”、“假设...”、“那么...”等。
为什么有效： 这让 AI 保持在自己的舒适区（编写英语），同时确保其结构足够严密，能够被计算机理解。这就像是给学生一份填空练习题，而不是一张白纸。

2. “中间人”（中间表示层，IR）

Visored 不仅仅是猜测 AI 的意思。它将那段英语脚本转换为一种中间层表示（称为 IR）。

类比： 想象 AI 写了一份草稿。Visored 拿到这份草稿后，会填补 AI 跳过的所有隐形“脚注”。AI 是否假设了 $x$ 是正数？Visored 会把这一点记录下来。AI 是否除以了一个变量？Visored 会检查该变量是否为非零。
神奇之处： 如果 AI 犯了错误，Visored 不仅仅是说“错误”，它还会精确地指出逻辑断裂的具体句子，就像老师用红笔圈出特定错误一样。这给了 AI 一个清晰的信号，告诉它下一步该如何修正。

3. “规则驱动求解器”（自动阅卷器）

一旦 Visored 将证明转换成这种中间层格式，它就会使用一个基于规则的引擎来检查那些“枯燥”的步骤。

类比： 想象一本数学教科书。当教科书说“由此得出...”时，它通常会跳过代数运算，因为这对人类来说显而易见。Visored 的求解器就像一个不知疲倦的机器人，负责填补这些被跳过的步骤。它会自动检查这些小步骤中的算术、代数和逻辑。
结果： 如果 AI 提供了主要思路，Visored 则负责处理这些琐碎的“苦力活”，去证明其中的微小步骤。

4. “回译”（Lean 输出）

如果 Visored 对该证明感到满意，它可以将其翻译回 Lean 代码（即那种严格的语言）进行最终验证。

代价： 论文承认目前的翻译非常“冗长”。这就像是将一份 1 页的摘要扩展成一份 200 页的法律合同，仅仅是为了确保每一个词在法律上都是精确的。虽然可行，但体积巨大。

他们究竟取得了什么成就？

研究人员在 244 个数学问题（主要来自初中竞赛）上测试了该系统。

结果： 使用 Visored 的 AI 智能体成功解决了这些问题中的 91%。
代价： AI 并不是“独自”解决问题的。它是在一个循环中工作的：AI 写一个草稿，Visored 检查并反馈“此处出错”，AI 进行修正，然后再次尝试。
局限性： 它在处理极难问题（如国际数学奥林匹克竞赛题目）时遇到了困难，因为 Visored 的“规则书”尚未具备处理这些高级数学技巧的能力。

核心结论

Visored 并不是一个能瞬间解决难题的“魔杖”。相反，它是一个协作式工作空间。它允许 AI 用它理解的语言（英语）编写证明，同时由一个计算机系统处理严格的逻辑和错误检查。

该论文声称，通过使用这种“中间人”方法，我们可以让 AI 生成真正可靠的数学证明，而无需强迫 AI 从头开始学习那些困难且僵化的形式化证明系统编程语言。它将 AI 的“幻觉”转化为了一个结构化的、可检查的过程。

技术摘要：Visored：一种用于 LLM 生成数学内容的受控自然语言证明器

问题陈述

大语言模型（LLMs）在数学推理方面展现出了日益增强的能力，但它们仍然容易产生幻觉。因此，AI 生成的证明其可靠性完全取决于验证过程。虽然自动定理证明器（ATPs）和全证明模型（例如针对 Lean 或 Rocq 的模型）在 miniF2F 等基准测试中取得了很高的通过率，但它们通常需要一个已经形式化的陈述作为输入。关键的瓶颈在于自动形式化（autoformalization），即如何将非形式化的数学散文翻译为机器可检查的形式。

这种翻译是非平凡的，因为非形式化数学依赖于共享的背景知识、隐式侧条件（例如 $x \neq 0$ ）以及读者会自动填补的符号滥用。直接翻译到形式化语言需要对特定的库引理、子类型、边缘情况约定和强制转换（例如 $\mathbb{N}$ vs. $\mathbb{Z}$ vs. $\mathbb{R}$ ）做出承诺，而这些在源文本中并无痕迹。这些决策产生的错误很少表现为编译器错误，而是表现为“无声的语义漂移”，即陈述虽然编译通过，但已不再反映原始意图。

方法论

Visored 是一个研究原型，旨在通过引入一个位于 LaTeX 与低级证明器（如 Lean）之间的依赖类型中间表示（IR），来弥合非形式化数学写作与形式化验证之间的鸿经过。

核心架构

该系统运行一个由以下阶段组成的流水线（见论文图 2）：

受控自然语言（CNL）输入： Visored 接受嵌入在 LaTeX 中的数学英语受控子集。其词汇表（句子模板如 "Let..."、"Assume..."、"Then..." 以及 LaTeX 命令）由外部 .lpcsv 规范文件定义，允许在不修改解析器的情况下扩展表面语言。
语法与语义： 输入被解析为语法树，然后被细化（elaborated）为类型化抽象语法树（sem AST）。此阶段解析名称、分配类型与种类，并执行**良定义性（well-definedness）**检查。遵循 PVS 的传统，偏函数（例如 $1/x$ 、 $\sqrt{x}$ 、 $\log x$ ）携带隐式的假设参数（例如 $x \neq 0$ 、 $x \ge 0$ ），这些参数必须在表达式被接受前得到解除（discharged）。
中级中间表示（MIR）： 类型化 AST 被降低（lowered）为 Visored MIR，它是求解器的基质。
成本受限求解器： 求解器使用基于规则且成本受限的引擎（名为 "Miracle"）来解除 "Then..." 义务和良定义性条件。它采用了一个包含后向和前向规则的数据库（受 ProofGrader 启发）以及专门的策略（例如代数归一化器、链式求解器），以关闭数学家通常省略的常规步骤。
可选的 Lean 发射： 被接受的证明可以被转译为 Lean 4。转译是一个可选的下游阶段，用于外部内核验证。转译过程涉及重放归一化历史并管理不同数字系统之间的强制转换见证（coercion witnesses）。

设计理念

Visored 的构建基于两个主要观察：

LLM 流畅度： LLM 在很大程度上是在非形式化数学上训练的。CNL 表面语言贴近 LLM 已经具备流畅度的领域，避免了要求模型从零开始学习低级证明器语法（策略、库引理名称）的需求。
可处理性： 弥合自然推理与形式化推理之间的差距比实现完整的自动定理证明更具可处理性。通过让 LLM 提供 CNL 形式的证明大纲，求解器只需要完成微小的、显而易见的步骤，这对于现代智能体工程（agentic engineering）来说是完全可以胜任的任务。

该系统将“向上”的语义解析（LaTeX $\to$ Visored）视为由 LLM 处理的难题，而将“向下”的投影（Visored $\to$ Lean）视为一个确定性的、机械的过程。

核心贡献

用于自动形式化的依赖类型 IR： Visored 引入了一个语义丰富的 IR，其中在 LaTeX 中没有表面痕迹的每一个决策（子类型、库引理、边缘情况约定、强制转换）都被明确化。
规范驱动的可扩展性： CNL 表面由外部配置文件而非硬编码解析器定义，允许在不重新编译系统的情况下，将词汇表调整为特定的数学惯例（教科书、竞赛、研究）。
局部诊断： 不同于在完整 Lean 编译后仅提供单一的接受/拒绝结论，Visored 在细化或求解阶段提供局部诊断。这允许实现“验证并修正”的循环，使 LLM 能够精准定位并修复特定错误。
良定义性强制执行： 系统通过由求解器解除的隐式假设参数来强制执行良定义性（例如，在进行 $1/x$ 操作前确保 $x \neq 0$ ），而不是依赖目标证明器的全总化（totalization）约定。
集成现有流派： Visored 将 Mizar/Naproche（CNL 表面）、PVS（类型检查时的良定义性）、Lean/Rocq（依赖类型）和 ProofGrader（成本预算规则驱动求解）的元素综合进一个面向 LLM 的流水线中。

实验结果

作者在 miniF2F-valid 切分集（244 个问题）上进行了覆盖度研究，该集合同时作为开发集和评估集。

性能： 一个由 Claude 引导、并辅以描述 CNL 表面的技能文档的 LLM 编码智能体，为 244 个问题中的 222 个（91%） 生成了经 Visored 检查的证明。
细分数据：
- 归纳法：100% (8/8)
- 代数：98% (86/88)
- 数论：97% (66/68)
- AMC/AIME：93% / 87%
- IMO (奥林匹克)：35% (7/20)
失败分析： 未解决的问题归因于 Visored 规则数据库的缺失（例如，缺少 AM-GM 不等式、缺乏有限域类型、三角恒等式）或原型的退化，而非 LLM 无法找到证明策略。作者明确指出，智能体未能解决这些问题是因为必要的“机制”尚未在系统中实现。
转译成本： 当前稀疏的发射方案导致 Lean 输出非常冗长，其行数中位数比例约为手写 Lean 证明的 $\approx 250\times$ ，尾部比例可达 $\approx 25,000\times$ 。这是由于需要重放归一化步骤和强制转换见证。

重要性与声明

论文将 Visored 定位为不是一个具有竞争力的自动定理证明器，而是一个新的基础设施概念验证，用于检查和组织 AI 生成的非形式化数学。

适度的声明： 作者明确表示，他们并不声称具有竞争力的自动定理证明能力，也不将结果外推到留存测试集。91% 的覆盖度被呈现为设计所能表达能力的下限，而非调优后的通过率。
瓶颈转移： 这项工作支持了这样一种观点：AI 数学能力的约束正在从“生成想法”转向“大规模验证并组织想法”。
效用模式： Visored 设计为可以执行四种模式：
1. 推理时验证器： LLM 输出的实时检查器。
2. 自动形式化循环： 让 LLM 根据局部诊断进行重写的机制。
3. 密集奖励信号： 为强化学习（RL）提供每步反馈。
4. CNL 数据生成器： 创建可再生、经过形式化检查且具有自然阅读感的证明语料库。

论文总结道，结合 CNL 表面、依赖类型 IR 和规则驱动求解器的组合，创建了一个失败是局部化且可操作的流水线，相比目前的直接自动形式化方法，它提供了一条从非形式化散文到内核检查证明的更可靠路径。未解决的问题代表了缺失规则和机制的积压，而非设计的根本局限。