pantograph

发表于 更新于 阅读次数： 字数： 1.4k 时间 ≈ 5 分钟
TODO

唠唠闲话

项目地址：https://github.com/lenianiva/PyPantograph

论文地址：https://arxiv.org/abs/2410.16429

CARTS: 通过多样化策略校准和抗偏置树搜索推进神经定理证明

项目分析：

  1. 缺陷：
    • 版本限制。需要构建 repl 文件，来处理操作，版本存在明显限制
    • 缺陷：交互结果可能不准确。
  2. 特性：
    • 更简明容易上手的交互过程，但是不是仅限于 expr，必须用 load_sorry
    • 基础的分析脚本（这里提到了 MCTS，但似乎就是全部了？）
  3. 可能的 bug：python debug mode 出错
  4. 一个建议（倾向于 pure tool，而不是将 vllm 接入，减少体积）

原理介绍

概要：该工具为 Lean 4 校对助手提供了多功能接口，并通过强大的搜索算法（如 Monte Carlo Tree Search）实现了高效的校对搜索。

一个说明性用例：使用机器学习模型和验证草图来证明 Lean4 定理。

一个用于 Lean 4 的 API 和 REPL，其主要目标是为训练和评估定理证明代理提供一个方便的接口。

名称 “Pantograph” 含义：recording the movement of a pen while drawing in order to create a copy.

LSP 是为人类用户交互式使用而提供的标准接口，创建 Pantograph 的主要动机是克服 Lean4 语言服务器协议 （LSP） 提供的接口的限制。LSP 作为机器界面存在许多问题，接口要求其用户跟踪文本中光标的位置，机器用户将承担解析来自 LSP 的消息的负担。LSP 接口也不显示有关元变量耦合的信息。此外，没有简单的方法可以从 LSP 界面提取战术训练数据或执行草图绘制。相比之下，Pantograph 是从头开始设计的，为机器（尤其是机器学习）代理提供了一个高效、方便的界面。

主要贡献：

  1. Pantograph handles metavariable coupling, which is a phenomenon that complicates tree search [13].
  2. 支持使用高级推理步骤 tactic
  3. 完全支持基本的数据提取任务，将证明表示提取为程序的重要功能，它允许对证明进行一次性预测
  4. 可用于支持草图校样 （DSP） 方法

关于 DSP 的讨论：https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Autoformalization.20of.20Coding.20Problems

如图所示：
20241202094835

人类操作员通过 IDE 与 Lean 4 的内核进行交互，但机器学习代理可以通过 Pantograph 的一个接口进行交互。

Pantograph 提供了三个接口：

  1. 一个名为 PyPantograph 的 Python 接口
  2. 通过 pantograph-repl 可执行文件的 REPL
  3. 通过 C 外部函数接口（FFI）的库

当用户执行策略时，Pantograph 会调用 Lean 4 内核的功能。在内部，Lean 4 的许多函数都是 monad，它们是抽象结构，可以在其他函数式语言中进行状态操作。Lean 4 的 monad 层次结构（从最一般的顺序到最不通用的顺序）的顺序为 IO，State 和 Option。

20241202095209

在通过 Pantograph 执行策略期间调用的最重要函数。

使用教程

环境配置

安装 Python 环境管理器 poetry

1
curl -sSL https://install.python-poetry.org | python3 -

poetry install 会创建虚拟环境，如果用 conda 来管理环境，则修改默认设置，避免冲突：

1
2
3
4
# 取消创建虚拟环境
poetry config virtualenvs.create false
# 设置镜像源（可选）
poetry config repositories.aliyun-pypi https://mirrors.aliyun.com/pypi/simple/

下载项目仓库：

1
git clone --recurse-submodules https://github.com/lenianiva/PyPantograph.git

构建并安装 Python 依赖：

1
2
poetry build
poetry install

安装需等待较长时间。

交互示例

pantograph 通过类 Server 与 Lean 环境交互，在初始化该类时，会导入 Init 库允许基础的操作。

证明表达式可直接通过 goal_start 创建目标，并用 goal_tactic 运行策略直到证明完毕。

举个例子：

1
2
3
4
5
6
import Init
example : forall (p : Prop), p -> p := by {
  intro p
  intro h
  exact h
}

用 Python 的交互方式：

1
2
3
4
5
6
7
8
from pantograph import Server
server = Server()
state0 = server.goal_start("forall (p : Prop), p -> p")
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro p")
# str(state1) # 'p✝ : Prop\n⊢ p✝ → p✝'
state2 = server.goal_tactic(state1, goal_id=0, tactic="intro h")
state3 = server.goal_tactic(state2, goal_id=0, tactic="exact h")
state3 # GoalState(state_id=3, goals=[], _sentinel=[])

操作说明：

  • goal_start 返回 GoalState 对象，可被策略作用
  • goal_tactic 执行策略后，返回新的 GoalState 对象，执行失败则抛出 TacticFailure
  • GoalState.goals 返回 Goal 对象列表
  • GoalState.is_solved 检查证明是否完成

在初始化 Server 时，可通过 imports 参数添加其他库，比如用于搜索证明的 Aesop。

非表达式需使用 load_sorry 策略。