lean-dojo/LeanCopilot

Lean Copilot – 面向 Lean 4 的 LLM 驱动证明辅助

它是什么

一个允许你直接从 Lean 4 代码调用大型语言模型（LLM）以自动化定理证明任务的库。
提供三个主要策略：
1. suggest_tactics – 为当前目标生成可能的 Lean 策略列表。
2. search_proof – 将 LLM 生成的策略与 aesop 证明器结合，搜索完整证明。
3. select_premises – 从 Lean 4 和 Mathlib 4 的冻结快照中检索可能有用的引理。
支持 Hugging Face 上托管的内置模型（通过 CTranslate2）以及任何用户提供的模型（本地二进制或远程服务器）。

为什么重要

将符号定理证明与现代神经语言模型连接起来，实现更快的证明开发和实验。
在 Lean 生态系统中原生工作，因此你可以将整个工作流程保持在一个地方 – 无需外部脚本。
开源并附带同行评审论文（已接受至 NeuS 2025）。

关键组件

组件	作用
NativeGenerator / NativeEncoder	通过 CTranslate2（通过 Lean 的 FFI 链接的 C++ 库）在本地运行小型 transformer 模型。
ExternalGenerator / ExternalEncoder	使用 `external_model_api.yaml` 中定义的简单 JSON API 调用在其他地方服务的模型（例如 Python HTTP 服务器）。
GenericGenerator / GenericEncoder	允许你插入任何实现 `generate` / `encode` 类型类方法的 Lean 类型。
Lake 集成	提供 `moreLinkArgs` 片段和 `require LeanCopilot` 条目，使下游包可以像任何其他 Lean 库一样依赖它。
Dockerfile / 构建脚本	为遇到原生依赖问题的 Linux/macOS/WSL 用户提供现成环境。

快速入门（快速步骤）

添加依赖 到你的 lakefile.lean 或 lakefile.toml，如 README 所示。
运行 lake update LeanCopilot，然后运行 lake exe LeanCopilot/download 获取预训练模型（每个约 200 MiB）。
构建原生代码，使用 lake build（如果你尚未导入它，则使用 lake build LeanCopilot）。
在 Lean 文件中，import LeanCopilot 并尝试：
```
example (n m : Nat) : n + m = m + n := by
  suggest_tactics
```
点击建议的策略以插入，或运行 search_proof 让系统自动尝试多步证明。

高级用法

通过 suggest_tactics 选项调整生成超参数（温度、束大小、返回的策略数量），详见 LeanCopilotTests/TacticSuggestion.lean。
通过编辑 ModelAPIs.lean 示例并将 ExternalGenerator 指向你自己的服务器，将默认模型替换为更大的模型。
通过提供系统库路径，使用 Lake 的 -KsystemOpenblas 和 -KsystemCtranslate2Lib 标志，跳过从源码构建 CTranslate2/OpenBLAS。

需要注意的注意事项

select_premises 返回快照中的原始定理名称；一些派生引理可能以不同名称出现。
search_proof 偶尔会产生无法通过终止检查的证明；临时重命名定理可以解决此问题。
在 Linux 上，依赖 Lean Copilot 的可执行文件（lean_exe）需要额外的链接器标志来引入系统的 libstdc++，因为 Lean 自己的二进制文件链接的是 libc++。

社区与支持

讨论：https://github.com/lean-dojo/LeanCopilot/discussions
问题：打开 GitHub issue，附上操作系统详细信息、复现步骤和调试日志。
贡献：欢迎提交 pull request；项目遵循通常的 Lean 社区约定。

引用如果你在研究中使用 Lean Copilot，请引用随附的论文：

@article{song2024leancopilot,
  title={Lean copilot: Large language models as copilots for theorem proving in lean},
  author={Song, Peiyang and Yang, Kaiyu and Anandkumar, Anima},
  journal={arXiv preprint arXiv:2404.12534},
  year={2024}
}

Lean Copilot 使 LLM 成为 Lean 定理证明世界中的一等公民，为神经语言模型和形式数学之间提供了实用的桥梁。

lean-dojo/LeanCopilot

Lean Copilot – 面向 Lean 4 的 LLM 驱动证明辅助

相关