lean-dojo/LeanCopilot

解決する課題

Lean Copilot は、大規模言語モデル（LLM）を Lean 定理証明器に直接統合し、形式的証明構築の面倒な部分を自動化します。ユーザーが「白紙の状態」に陥るのを防ぎ、証明の次のステップを提案したり、完全な証明を自動的に検索したりします。

動作方法

このプロジェクトは Lean と LLM の間のネイティブなブリッジを提供します。ユーザーは CTranslate2 を通じてローカルでモデルを実行したり、API を通じてリモートモデルに接続したりできます。主に以下の3つの機能を実装しています：

• タクティック提案：証明を進めるための次のタクティック候補を生成し、ユーザーがクリックして適用できます。
• 証明探索：LLM が生成したタクティックと aesop 探索エンジンを組み合わせて、複数ステップの証明を検索します。
• 前提選択：リトリーバーモデルを使用して、現在のゴールに関連する有用な数学的前提（Lean や mathlib4 から）を特定します。

対象ユーザー

Lean 定理証明器を使って数学やコンピュータサイエンスの研究を行う研究者や開発者で、AIアシスタントを使って形式化作業を加速させたい人向けです。

特徴

• 柔軟なモデル対応：LeanDojo に内蔵されたモデル、ローカルモデル（GPU 有無問わず）、カスタムリモートモデルをサポート。
• ネイティブ統合：Lean の依存関係として動作し、Lean エディタ内で直接 LLM 推論をトリガーできます。
• 拡張可能な API：TextToText と TextToVec インターフェースを提供し、開発者がカスタム証明自動化やその他の LLM に基づくアプリケーションを Lean で構築できるようにします。
• クロスプラットフォーム：Linux、macOS、Windows（WSL を含む）をサポート。