本地跑 Leanstral 1.5 做形式化验证 / 先确认显存和 Lean 工具链

想在本地用 Leanstral 1.5 做形式化验证，真正容易卡住的地方通常不是模型会不会写 Lean 语法，而是三件事能不能同时成立：显存装不装得下权重、本地推理服务能不能正常起、Lean 侧有没有一个独立的编译环境把模型输出验一遍。这三件事里任意一环不成立，后面调提示词、改策略都容易变成猜。建议按顺序逐层确认，先跑通「能加载、能返回、能编译」这条最小链路，再考虑别的。

如果只做本地试验，建议按「显存能否装下权重 → 推理服务能否返回文本 → Lean 能否编译通过」的顺序逐层确认，任一步失败就先停在那里，不要急着调提示词。显存和推理框架版本以 Leanstral 1.5 模型发布页的要求为比对依据，不用别人的经验数字估算；Lean 用 elan 装独立工具链，与模型推理环境分开。模型返回的 tactic 看着合理不算数，必须过一遍 lake build。

查看机器显存和 CUDA 版本是否满足推理服务要求

模型权重加载是第一个硬门槛。先确认机器上能看到几张卡、每张卡的显存和驱动情况：

nvidia-smi
nvidia-smi `--query-gpu`=name,memory.total,driver_version `--format`=csv

nvidia-smi 右上角显示的 CUDA Version 是驱动支持的版本上限，实际运行时用的 CUDA 版本要看推理框架自己链接的那一份。可以分别确认 PyTorch 和推理框架的版本：

python -c "import torch; print(torch.__version__, torch.version.cuda)"
python -c "import vllm; print(vllm.__version__)"   # 若使用 vLLM；换其它框架时替换为对应模块

这几条命令本身不回答「够不够」，答案在 Leanstral 1.5 的模型发布页上：那里通常会写明权重的显存量级、推荐的推理框架版本和上下文长度要求。把上面输出的显存总量、CUDA 版本、框架版本与发布页逐项比对，比拿经验数字估算可靠。需要提醒的是，权重之外还要留出 KV cache 的空间，上下文开得越长占用越多，所以「权重文件大小小于显存」不等于能跑起来；多卡场景还要确认张量并行能否覆盖模型层数。

安装 Lean 4 工具链并确认 lake 可用

Lean 侧建议用 elan 管理工具链，和推理服务彻底分开，避免在模型环境里装了一堆 Python 包之后又来折腾 Lean。安装后重新加载 shell 配置并检查：

curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source ~/.profile
lean `--version`
lake `--version`

lake `--version` 能打印版本号，说明构建工具可用。接着建一个最小项目，先确认默认模板能编译，再决定要不要引入 mathlib 这类重依赖：

本地跑 Leanstral 1.5 做形式化验证 / 先确认显存和 Lean 工具链

lake new leancheck
cd leancheck
lake build

项目建好后，把下面一行放进模板生成的 Lean 文件里（文件名以实际生成的为准），跑一次解析：

#check Nat.add_comm

如果 lake build 能过，工具链这一层基本就绪。mathlib 的引入建议放在确认工具链可用之后，它的编译时间明显更长，早期调试没必要背这个负担。

启动本地推理服务并加载 Leanstral 1.5 权重

启动命令这里用占位符写骨架，参数名按你实际选用的推理框架替换。下面以 vLLM 的 OpenAI 兼容接口为例，换成 llama.cpp、Ollama 或其它框架时，找对应参数的等价项即可：

python -m vllm.entrypoints.openai.api_server \
  `--model` /path/to/leanstral-1.5 \
  `--served-model-name` leanstral-1.5 \
  `--host` 127.0.0.1 \
  `--port` 8000 \
  `--tensor-parallel-size` 1 \
  `--max-model-len` 4096 \
  `--gpu-memory-utilization` 0.90

需要替换的部分：模型目录换成实际权重路径，端口换成机器上没有被占用的端口，tensor-parallel-size 按可用卡数调整，max-model-len 按你的证明目标长度决定，gpu-memory-utilization 按剩余显存留出余量。启动后重点看日志：出现权重加载完成、开始监听端口这类行，才算服务真的起来了；如果卡在分配 KV cache 或者直接 OOM 退出，回到上一节重新核对显存。也可以用一条轻量请求确认服务活着：

curl -s http://127.0.0.1:8000/v1/models

用一次简单证明请求测试模型能否返回文本

服务起来之后，发一个最小请求确认推理链路通不通。目标是让模型针对一个 Lean 目标返回 tactic 文本，而不是写整篇解释。可以先写一个 payload 文件：

{
  "model": "leanstral-1.5",
  "messages": [
    {"role": "system", "content": "You are a Lean 4 proof assistant. Reply with tactics only, no explanation."},
    {"role": "user", "content": "Goal: theorem add_zero (n : Nat) : n + 0 = n"}
  ],
  "max_tokens": 256,
  "temperature": 0
}

然后发送：

curl -s http://127.0.0.1:8000/v1/chat/completions \
  -H "Content-Type: application/json" \
  -d @payload.json

检查返回体里 choices[0].message.content 是否非空。非空只说明链路连通，不说明证明正确。同时留意输出里有没有 markdown 代码围栏、前缀说明，或者是 Lean 3 风格的旧语法——这些在下一步入库前都要清掉，否则编译器会把它当语法错误处理。

把返回文本放进 Lean 文件做编译验证

把模型返回的文本转成可编译的 Lean 文件，这一步才算闭环。在项目里新建或打开一个 .lean 文件：

import Init

theorem add_zero (n : Nat) : n + 0 = n := by
  -- 把模型返回的 tactic 行粘贴到这里，注意与 by 的缩进对齐

import 那行按证明需要调整：只用核心库时 import Init 一般就够，用到 mathlib 里的引理才需要改成 import Mathlib。保存后运行：

lake build

输出通常落在两类结果上。编译通过，说明模型给的 tactic 在当前环境下成立，可以把这条记录留下来，作为后续同类目标的参考；报错也很常见，典型的有 unknown identifier（引理名或策略名不存在，可能是幻觉出来的）、unsolved goals（策略没把目标证完）、type mismatch（类型对不上）。把报错原文连原目标一起送回模型，让它基于真实错误修正，比重新生成一遍更有效。另外，模型可能引用当前 import 范围之外的引理，这时补 import 或换等价引理即可，不必直接判定模型输出无效。