Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

本文介绍了 Apply2Isar 工具，它能够自动将 Isabelle/HOL 中可读性较差的过程式"apply-style"证明脚本转换为更稳健且易读的声明式 Isar 证明，并通过在 Isabelle 形式化证明档案上的大规模评估验证了其有效性。

要点

这篇论文介绍了一个名为 Apply2Isar 的新工具，它的核心任务可以比喻为：把“乱涂乱画的草稿”自动整理成“工整的正式文档”。

为了让你更容易理解，我们可以用**“做菜”或者“写代码”**的比喻来拆解这篇论文。

1. 背景：两种不同的“做菜”方式

在 Isabelle/HOL（一个用于数学证明的超级电脑软件）里，证明一个数学定理就像做一道复杂的菜。用户有两种主要的“烹饪风格”：

• Apply-style（应用风格/草稿模式）：

  • 比喻： 就像你在厨房里手忙脚乱地试菜。你往锅里扔一点盐，尝一口；不行，再扔点糖，再尝一口。你只关心“下一步该放什么”，而不关心“为什么放”。
  • 特点： 这种写法写起来很快，适合快速探索（试错）。但是，它就像一张潦草的笔记。如果以后你想修改食谱（比如把盐换成酱油），你很难知道哪一步会出错，因为步骤之间没有明确的逻辑连接，一旦中间某一步变了，整个菜可能就废了，而且很难找出是哪一步搞砸的。
  • 缺点： 脆弱、难读、难维护。

• Isar-style（结构化风格/正式文档）：

  • 比喻： 就像一本正式的食谱书。每一步都写得清清楚楚：“首先，我们要证明 A 是咸的；然后，基于 A，我们证明 B 是甜的；最后，因为 A 和 B 都成立，所以整道菜是美味的。”
  • 特点： 这种写法读起来非常顺畅，逻辑清晰。即使以后你想改食谱，你也能一眼看出哪一行需要修改，因为它像搭积木一样，每一步都稳稳地建立在下一步的基础上。
  • 缺点： 写起来比较慢，需要更多的思考和规划。

痛点： 很多用户喜欢用“草稿模式”（Apply-style）快速试错，但最后为了长期维护，又不得不把它改写成“正式文档”（Isar）。但这就像要把一堆乱糟糟的草稿手抄成正式文档，非常累人，而且容易抄错。

2. 解决方案：Apply2Isar 工具

Apply2Isar 就是为了解决这个痛点而生的“自动整理机器人”。

• 它是怎么工作的？
  想象你有一堆乱序的乐高积木（Apply-style 脚本）。Apply2Isar 会：

  1. 重演过程： 它像回放录像一样，重新运行你的草稿，记录下每一步操作后剩下的积木（中间状态）。
  2. 逆向构建： 因为它知道最终要拼成什么，它会从最后一步倒着推回去，把每一步的“积木”（中间目标）和“操作”（证明方法）重新排列。
  3. 生成文档： 它把这些信息自动组装成一本结构清晰的“正式食谱”（Isar 证明）。

• 它的特点：

  • 忠实还原： 它不会为了“好看”而重新发明你的证明逻辑。它生成的文档可能看起来有点“机械感”（比如会有很多像 h_1_2 这样的临时标签），但它保证逻辑和你原来的草稿一模一样。
  • 自动纠错： 如果原来的草稿里有些步骤太乱（比如同时处理多个目标），它会智能地拆分，确保生成的文档在逻辑上是严丝合缝的。

3. 遇到的挑战（就像翻译中的“方言”问题）

把“草稿”变成“正式文档”并不像简单的翻译，因为两者底层逻辑不同。作者们在开发工具时遇到了一些有趣的难题：

• 多目标处理： 有时候一个命令能同时解决好几个问题（比如“把锅里的所有菜都炒熟”）。在草稿里这很简单，但在正式文档里，必须把每个菜单独列出来。工具需要聪明地决定是“一次性列出”还是“分步列出”。
• 变量重名（Shadowing）： 就像你在写文章时，前面用了“小明”，后面又定义了一个叫“小明”的人。在草稿里，电脑能分清；但在正式文档里，如果不改名，就会混淆。工具需要自动给变量起新名字（比如“小明_1"），防止搞错。
• 未知的变量： 有时候证明过程中会出现“待定项”（就像食谱里写着“加适量的盐”）。正式文档通常要求明确，所以工具遇到这种情况时，会暂时保留一小段草稿，或者标记为“部分转换”。

4. 效果如何？

作者们找来了几千个真实的“草稿”证明（来自 Isabelle 的官方档案库）来测试这个工具。

• 成功率： 在 95% 到 99% 的情况下，工具都能成功把“草稿”转换成“正式文档”。
• 部分成功： 剩下的少数情况，通常是因为证明太复杂，包含了一些特殊的“待定项”，工具只能转换大部分，留一小段草稿。
• 结论： 这个工具非常实用，能帮用户节省大量时间，把原本脆弱、难读的证明，变成坚固、易读的文档。

总结

Apply2Isar 就像是一个**“证明文档的自动排版师”**。

它允许你先用最灵活、最快速的方式（Apply-style）去探索数学真理，不用担心写得乱；等你找到答案后，一键点击，它就能帮你把那些凌乱的探索过程，自动整理成一份逻辑严密、清晰易读的正式数学证明（Isar）。这让数学家和程序员既能享受“快速试错”的快感，又能拥有“长期维护”的安心。

技术摘要

Apply2Isar 技术总结

1. 研究背景与问题 (Problem)

在 Isabelle/HOL 交互式定理证明器中，存在两种主要的证明风格：

• Apply-style（过程式）： 类似于传统的策略脚本（Tactic Scripts），用户通过向后推理（Backward Reasoning）调用方法（Methods）来逐步消除目标。这种风格便于快速探索搜索空间，但生成的脚本通常是“黑盒”式的，缺乏中间状态的显式声明，导致可读性差、脆弱（Brittle），且难以维护。一旦底层简化规则或方法行为发生变化，脚本容易在后期步骤中失败，且难以定位错误源头。
• Structured Isar（声明式）： 用户显式地写出中间目标、假设和推理步骤，通常采用向前推理（Forward Reasoning）。这种风格具有极高的可读性、鲁棒性和可维护性，是 Isabelle 社区（包括 AFP 归档库）的首选。

核心问题： 尽管 Isar 风格更优，但许多用户（尤其是初学者或在进行复杂探索时）倾向于先编写 Apply-style 脚本。将过程式脚本手动重构为声明式 Isar 证明是一个极其繁琐且易错的过程，因为用户必须手动记录每一步的中间状态并重新组织证明结构。目前缺乏一种自动化工具能高效、准确地将 Apply-style 脚本转换为高质量的 Isar 证明。

2. 方法论 (Methodology)

论文提出了 Apply2Isar，一个基于 Isabelle/ML 实现的自动化工具，旨在将 Apply-style 脚本转换为结构化 Isar 证明。其核心工作流程如下：

1. 解析与 AST 构建： 工具首先使用 Isabelle/ML 生态系统中的函数对输入的 Apply 脚本进行词法分析和语法分析，构建自定义的抽象语法树（AST）。
2. 证明重放（Replay）： Apply2Isar 在内部重放原始脚本中的每一个证明命令。在重放过程中，它记录每个方法应用后的中间证明状态（即剩余的目标列表和上下文事实）。
3. 逆向构建 Isar： 由于 Isar 倾向于向前推理，而 Apply 脚本是向后推理的，工具将记录的中间状态逆向处理。它从最终状态回溯到初始状态，构建声明式的证明结构。
4. 生成结构化证明： 工具将中间目标打印为 have 语句，将对应的证明方法作为 by 子句。为了连接步骤，它使用 fact 方法作为“粘合剂”，确保前一步产生的事实能被后续步骤引用。

关键设计挑战与解决方案

为了处理 Apply 脚本与 Isar 之间的结构性差异，作者解决了以下技术难点：

• 多目标处理 (Multiple Goals)：
  • 挑战： 某些命令（如 auto, simp_all）可能同时影响多个目标，甚至证明部分目标。
  • 方案： 实现了 smart_goals 选项。默认情况下，工具只打印发生变化的目标，避免冗余。对于被证明的目标，工具会在最后通过 show 语句统一提交，或者在中间步骤使用 fact+ 来消耗已解决的目标。
• 证明流与事实管理 (Proof Flow & Facts)：
  • 挑战： subgoal（子目标）和 supply（引入事实）命令会改变证明上下文，且顺序敏感。直接反转命令顺序会导致事实在定义前被引用。
  • 方案： 工具将所有 subgoal 子证明和 note（对应 supply）命令提升（Lift） 到 Isar 证明块的开头，确保事实定义早于引用。同时提供了 dummy_subproofs 选项，用占位符替换移动的子证明以保持原始逻辑流的视觉相似性。
• 命令交互 (Command Interactions)：
  • 挑战： using（引入事实）和 unfolding（展开定义）可能同时作用于目标和事实。
  • 方案： 实现了 smart_unfolds 选项，将一系列 using/unfolding 的效果与随后的 apply 命令合并，减少重复代码。但在涉及 subgoal 的复杂序列中，回退到更保守的重复展开策略以保证正确性。
• 变量遮蔽 (Shadowing)：
  • 挑战： subgoal 命令会对元量化变量进行 Skolem 化，用户可能选择与现有变量同名的名称，导致冲突。
  • 方案： 默认行为处理“负责任”的遮蔽（无冲突）。提供了 subgoal_fix_fresh 选项，强制重命名变量以避免冲突，但这可能导致显式引用旧名称的代码失效。
• 模式变量 (Schematic Variables)：
  • 挑战： Apply 脚本中常包含未实例化的模式变量（如 ?x），而 Isar 的 have 语句不允许包含模式目标。
  • 方案： 当遇到模式目标时，工具停止转换，将包含模式变量的部分保留为嵌套的 Apply-style 子证明。这被视为“部分转换”。
• 类型注解 (Types)：
  • 挑战： 打印目标时可能丢失类型信息，导致重新解析失败。
  • 方案： 提供 print_types 选项，允许用户选择打印所有类型、必要类型或不打印，通过重解析检查来确保生成的代码类型正确。

3. 主要贡献 (Key Contributions)

1. 首个自动转换工具： 提出了 Apply2Isar，这是第一个专门用于将 Isabelle/HOL 的 Apply-style 脚本自动转换为结构化 Isar 证明的工具。
2. 混合证明支持： 工具不仅处理纯 Apply 脚本，还支持混合证明（在 Apply 脚本中嵌入 Isar 块）和部分证明（使用 sorry 占位符），极大地提高了其实用性。
3. 鲁棒性与灵活性： 通过多种配置选项（如 smart_goals, named_facts, print_types 等），工具能够适应不同的证明风格和复杂场景，平衡了生成的代码的机器可读性与人类可读性。
4. 确定性转换： 与基于大语言模型（LLM）的转换方法不同，Apply2Isar 是完全确定性的，基于 Isabelle 内核的精确重放，保证了转换结果的可信度。

4. 评估结果 (Results)

作者在 Isabelle 归档库（AFP）中选取了 5 个包含大量 Apply-style 证明的条目（如 Group-Ring-Module, AutoCorres2 等），构建了包含 4461 个 Apply-style 证明的基准测试集。

• 成功率： 在默认配置下，Apply2Isar 在 95%–99% 的测试案例中成功生成了可工作的 Isar 证明（包括完全转换和部分转换）。
  • 完全成功： 大部分条目（如 Group-Ring-Module）的成功率极高。
  • 部分转换： 约 4%–15% 的转换是部分的，主要原因是遇到了模式变量（Schematic Goals），导致部分证明步骤仍保留为 Apply 风格。
• 失败原因分析：
  • 打印/解析不一致： 约 1% 的失败是由于 Isabelle 内部的目标打印机制与重新解析机制之间的不一致（通常涉及自定义语法）。
  • 超时： 极少数情况因类型检查或重解析耗时过长导致超时。
  • 其他： 少量边缘情况的方法交互问题。
• 性能： 工具在普通硬件上运行良好，处理包含 350 多条命令的长脚本也未见明显性能瓶颈（设置了 30 秒超时限制）。

5. 意义与影响 (Significance)

1. 提升代码质量与维护性： Apply2Isar 允许用户利用 Apply-style 进行快速原型设计和探索，随后自动将其转换为鲁棒、易读的 Isar 证明。这显著降低了维护大型形式化证明库（如 AFP）的门槛。
2. 降低学习曲线： 对于不熟悉 Isar 高级语法的用户，该工具提供了一个从“过程式”平滑过渡到“声明式”的桥梁，有助于推广 Isar 的最佳实践。
3. 增强证明鲁棒性： 转换后的 Isar 证明对底层自动化行为的变化（如简化规则更新）具有更强的抵抗力，减少了因环境变化导致的证明断裂。
4. 与现有生态的互补： 相比于基于 LLM 的 Isabelle Assistant（如 AWS 的 Isabelle Assistant），Apply2Isar 提供了完全确定性的转换，且无需云端依赖，适合本地化、高可靠性的开发场景。

综上所述，Apply2Isar 有效地解决了 Isabelle 社区中长期存在的“过程式探索”与“声明式维护”之间的矛盾，为形式化验证工具的实用化和普及化提供了强有力的支持。