lean-dojo/LeanCopilot

Lean Copilot – Lean 4 向け LLM 駆動の証明支援

概要

Lean 4 コードから直接大規模言語モデル（LLM）を呼び出して定理証明タスクを自動化できるライブラリです。
3 つの主要な戦術を提供します：
1. suggest_tactics – 現在の目標に対して可能な Lean 戦術のリストを生成します。
2. search_proof – LLM 生成の戦術と aesop プロバーを組み合わせて完全な証明を検索します。
3. select_premises – Lean 4 と Mathlib 4 のスナップショットから有用と思われる補題を取得します。
Hugging Face でホストされている組み込みモデル（CTranslate2 経由）と、ユーザー提供の任意のモデル（ローカルバイナリまたはリモートサーバー）をサポートします。

重要性

記号的定理証明と最新のニューラル言語モデルを橋渡しし、より高速な証明開発と実験を可能にします。
Lean エコシステム内でネイティブに動作するため、ワークフロー全体を 1 か所に保てます – 外部スクリプトは不要です。
オープンソースであり、査読付き論文（NeuS 2025 に採択）が付属しています。

主要コンポーネント

コンポーネント	役割
NativeGenerator / NativeEncoder	CTranslate2（Lean の FFI を介してリンクされる C++ ライブラリ）を使用して、小さなトランスフォーマーモデルをローカルで実行します。
ExternalGenerator / ExternalEncoder	`external_model_api.yaml` で定義されたシンプルな JSON API を使用して、他の場所で提供されるモデル（例：Python HTTP サーバー）を呼び出します。
GenericGenerator / GenericEncoder	`generate` / `encode` 型クラスメソッドを実装する任意の Lean 型をプラグインできます。
Lake 統合	`moreLinkArgs` スニペットと `require LeanCopilot` エントリを提供し、ダウンストリームパッケージが他の Lean ライブラリと同様に依存できるようにします。
Dockerfile / ビルドスクリプト	ネイティブ依存関係の問題に遭遇する Linux/macOS/WSL ユーザー向けの既製環境を提供します。

クイックスタート（簡単な手順）

依存関係を追加 します。README に示されているように lakefile.lean または lakefile.toml に追加します。
実行します。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）は、Lean のバイナリが libc++ にリンクしているため、システムの libstdc++ を取り込むための追加のリンカーフラグが必要です。

コミュニティとサポート

ディスカッション：https://github.com/lean-dojo/LeanCopilot/discussions
問題：OS の詳細、再現手順、デバッグログを添えて GitHub の問題を開いてください。
貢献：プルリクエストを歓迎します。プロジェクトは通常の 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 駆動の証明支援

関連