🤖 machine learning

Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

本文介绍了 Nazrin，这是一个基于图神经网络的 Lean 4 定理证明智能体，它利用了一套新颖的原子策略（atomic tactics）、一种转置原子化算法（transposing atomization algorithm）以及 ExprGraph 数据结构，从而实现了稳健且兼容消费级硬件的证明自动化。

原作者： Leni Aniva, Iori Oikawa, David Dill, Clark Barrett

发布于 2026-07-01

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Leni Aniva, Iori Oikawa, David Dill, Clark Barrett

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

想象一下，你正试图教一个机器人去解决复杂的数学谜题。机器人的目标是证明一个数学命题是正确的。在计算机科学领域，这被称为“机器辅助定理证明”（Machine-Assisted Theorem Proving）。

这篇论文介绍了一个名为 Nazrin 的新机器人（其名称代表 Neural Atomizer for Inhabitation Problems，即用于填充问题问题的神经原子化器）。Nazrin 被设计得比以往的机器人更聪明、更快、更高效。以下是它的工作原理，通过简单的概念和类比进行拆解。

1. 问题所在：选择太多

想象你在玩一款电子游戏，目标是到达一个藏宝地点。在旧的教学方法中，机器人会被给予一个庞大且无限的动作菜单。它可以说“跳跃”、“奔跑”、“飞行”、“使用魔法咒语”，或者“按特定顺序组合 50 种不同的咒语”。

因为这个菜单如此庞大且混乱，机器人会感到困惑。它不知道人类玩家选择某个动作是因为这是最佳动作，还是仅仅因为玩家当时想这么做。此外，人类编写的证明过程往往会跳过步骤或使用一些在纸面上看起来很漂亮、但很难让机器人从零开始构建的巧妙捷径。

2. 解决方案：原子策略（乐高积木）

Nazrin 通过给机器人一个微小的、有限的原子策略（Atomic Tactics）盒子来解决这个问题。把这些想象成标准的乐高积木。

与其说“建造一座城堡”，机器人只能得到类似“放置一块红砖”、“放置一块蓝砖”或“连接两块积木”的指令。
这些“砖块”是简单的、有限的且定义严格的。
论文声称，如果你拥有正确的这套简单砖块，你就可以构建出任何有效的数学证明。

这让机器人的工作变得更加容易。它不再需要从无限的菜单中进行选择，而只需在每一步中从一份小巧、可控的选项列表中进行挑选。

3. 翻译器：转置原子化

你可能会问：“但如果现有的数学证明都是用‘华丽的人类语言’编写的，并且带有巨大的捷径，我们该如何教机器人呢？”

作者创建了一个特殊的翻译器，称为转置原子化（Transposing Atomization）。

类比： 想象一位人类厨师写下一份食谱，上面写着“制作完美的舒芙蕾”。这是“呈现视图”（Presentation View）——它看起来很棒，但跳过了细节。
该翻译器会将那份食谱分解成步步拆解的原子动作列表：“打 3 个鸡蛋”、“搅拌 2 分钟”、“加入糖”、“以 350 度烘焙”。
这个过程将“华丽”的人类证明转化为一段长而详细的简单“原子”步骤序列。这为机器人提供了一个庞大的训练数据库供其学习。

4. 地图：ExprGraph

数学表达式可能非常杂乱。它们经常包含许多重复的数字或变量，或者使用不同的名称来指代同一事物。

类比： 想象一张城市地图。在普通地图中，每条街道都是单独绘制的。但在 Nazrin 的地图（称为 ExprGraph）中，如果两条街道实际上是同一条路，它们就会被绘制成单条线。如果两栋建筑是同类型的，它们就会共享同一个图标。
这种“本质化”（Essentialization）剥离了令人困惑的细节，只关注数学的结构。它帮助机器人看到问题的“形状”，而不被无关紧要的信息所干扰。

5. 大脑：Nazrin 证明器

Nazrin 是机器人的大脑。它是一种被称为图神经网络（Graph Neural Network, GNN）的人工智能。

因为数学问题已被转化为这些清晰的“地图”（ExprGraphs），Nazrin 可以观察地图并预测下一个最佳的“乐高积木”（原子策略）应该放在哪里。
超能力： Nazrin 的速度极快。其他机器人（如使用大语言模型的机器人）可能需要数秒钟才能想出一个动作，而 Nazrin 每分钟可以生成数千个动作。
硬件： 它非常高效，甚至可以在标准的家用电脑（“消费级”机器）上运行，而不仅仅是依赖大型超级计算机。

6. 结果：效果如何？

作者在两个巨大的数学问题库（“标准库”和“Mathlib”）上测试了 Nazrin。

他们用一组问题训练 Nazrin，然后要求它解决来自相似集合的新、未见过的题目。
结果： Nazrin 成功证明了标准库中约 57% 的问题，以及更大的 Mathlib 库中 34% 的问题。
至关重要的是，Nazrin 能够解决一些其他著名的自动化工具（如 Aesop 和 Grind）无法解决的问题。它作为一种不同类型的工具，与现有工具形成互补。

总结

简而言之，这篇论文介绍了 Nazrin，这是一个定理证明机器人，它：

将复杂的数学分解为简单的、原子的步骤（就像乐高积木一样）。
将人类编写的证明转化为这些简单的步骤以便学习。
使用一种特殊的“地图”来理解数学结构，而不被细节所困扰。
在普通计算机上运行快速，并且能解决其他工具无法处理的数学问题。

作者强调，这是一种处理数学证明的新方法，它侧重于寻找解决方案的过程（搜索），而非仅仅关注最终的书面结果。

技术摘要：Nazrin：一种在 Lean 4 中的原子神经证明自动化策略

问题陈述

在像 Lean 4 这样的系统中，针对人类编写的证明训练自动化智能体面临着重大挑战。主要的障碍包括：

无界动作空间： 人类证明利用了具有任意参数的无限种多样化的策略（例如，带有长参数列表的 simp，或带有任意见证者的 use），这创造了一个嘈噪声大且难以学习的搜索空间。
展示视图与搜索视图的差异： 人类编写的证明通常优先考虑简洁性和可读性（展示视图，Presentation View），从而掩盖了发现证明实际所需的增量式、后向推理步骤（搜索视图，Search View）。这包括“神秘的跳跃”以及中间步骤的省略。
元变量耦合： 在 Lean 中，目标之间往往存在相互依赖关系（耦合元变量）。朴素的树搜索无法考虑到解决一个目标可能会瞬间解决另一个目标或导致某条路径变得不可能这一事实，这使得搜索是在有向无环图（DAG）而非简单的树上进行。
硬件约束： 现有的神经定理证明器通常需要大量的计算资源，限制了它们的普及程度以及能够处理的训练数据规模。

方法论

本文介绍了 Nazrin（神经原子化问题填充器，Neural Atomizer for Inhabitation Problems），一种基于图神经网络（GNN）的定理证明智能体。该方法依赖于三个核心支柱：

1. 原子策略 (Atomic Tactics)

作者定义了一组小规模、有限的“原子策略”，这些策略能够证明 Lean 中的任何可证明陈述。这些策略的设计旨在具有受限的参数空间，从而确保智能体的动作空间是有限的。

完备性： 该集合涵盖了 Lean 中所有的顶级表达式构造器（例如，用于 $\lambda$ 抽象的 intro，用于常量的 exact/apply，用于归纳类型的 cases）。
属性： 这些策略是保持不变的（在不进行回溯的情况下不会改变已分配的元变量）、完备的、进展性的（始终能取得进展）且是确定性的。
最小化横截面： 选择该集合的目的是最小化“横截面”（耦合目标的数量），从而降低引导生成问题的难度。

2. 转置原子化 (Transposing Atomization)

为了训练智能体，作者开发了一种新算法，将现有的、人类编写的证明（展示视图）转换为原子策略序列（搜索视图）。

原子化： 该算法将任意证明项翻译成一系列原子步骤。它利用地面真值（ground-truth）证明项来指导构建一个新的仅使用原子策略的证明。
转置： 该算法重新排列策略的执行顺序以匹配“搜索视图”。它优先处理“后继”目标（即其解能为前驱提供信息的目标），而非“前驱”目标。这模仿了发现过程中的后向推理（例如 $\epsilon$ - $\delta$ 证明），而非前向展示。
状态级与目标级转置： 系统通过重新排列策略调度来避免死路。例如，它允许对目标或自由变量起作用的非冲突“半梯度（semigrade）”策略以任意顺序进行调度，即使耦合的目标尚未实例化。

3. ExprGraph 与神经架构

智能体使用图神经网络（GNN）来处理被表示为 ExprGraph 的 Lean 表达式。

本质化： 表达式被转换为图形，其中无关的技术性区别（例如特定的变量名、元数据）被消除。该图保留了基本的对称性（例如 $\alpha$ -等价性），并确保子表达式对应于子图。
神经概率自动机 (NPA)： Nazrin 并非使用标准的生成模型，而是使用了一个 NPA。GNN 用于调节有限状态自动机的转移概率。
- 种类状态 (Kind State)： 选择策略类型（例如 intro、apply）。
- 后继状态 (Descendant States)： 特化的 GNN 头生成参数（例如，为 apply 选择一个常量或一个自由变量）。
效率： 该模型规模很小（标准库为 150 万参数，Mathlib 为 1100 万参数），可在消费级 CPU 硬件上运行，每分钟生成数千个策略。

核心贡献

原子策略： 一组有限且完备的策略，将定理证明的动作空间缩减为可控的大小，从而实现高效的强化学习和监督训练。
转置原子化算法： 一种通过将现有的形式化数学转换为原子化、搜索视图证明来生成大规模训练数据的方法，有效地教会智能体如何寻找证明，而非如何展示证明。
ExprGraph： 一种简化的基于图的 Lean 表达式表示法，它利用了数学对称性和变量引用，显式地模仿了语言模型中发现的注意力机制。
Nazrin 证明器： 一个低资源、基于 GNN 的智能体，能够成功在原子化数据上进行训练并泛化到新的定理。
评估框架： 一个模拟开发新理论过程的严格评估框架，通过在库的一个切片上进行训练并在下一个切片上进行测试，以确保没有信息泄漏。

结果

作者在 Lean 的标准库和 Mathlib 上对 Nazrin 进行了评估：

原子化成功率： 在 170,180 个定理中，约 58% 的定理被成功原子化。
泛化能力：
- 在标准库切片 1 上训练后，Nazrin 在切片 2 上达到了 57% 的准确率。
- 在 Mathlib 切片 3 上训练后，Nazrin 在切片 4 上达到了 34% 的完成率。
对比： Nazrin 展示了证明现有自动化策略（如 Aesop 和 Grind）无法在 15 秒时限内完成的定理的能力。
性能： 该系统在消费级硬件上高效运行，这与许多基于 LLM 的证明器所需的高资源需求形成鲜明对比。

重要性与主张

论文声称 Nazrin 解决了人类编写证明的结构与自动化搜索需求之间的根本不匹配问题。通过利用原子策略强制执行有限的动作空间，并通过转置原子化生成训练数据，作者证明了：

机器学习智能体可以被训练去增量式地发现证明，而无需从头开始生成复杂的、任意的参数。
基于图的表示法在捕捉数学证明的结构对称性方面是有效的。
高性能的定理证明可以在适度的硬件上实现，使该技术更具普适性。

作者指出，虽然该系统前景广阔，但目前尚未覆盖所有定理（原子化在某些高横截面证明中会失败），且架构尚未完全调优。他们建议未来的工作可以专注于提高原子化覆盖率、减少横截面，以及改进神经架构以更稳健地处理多参数调节和非符号数据（数字/字符串）。