llmlean

LLMリーン

LLMlean は、戦術の提案、証明の完了などのために LLM と Lean を統合します。

以下は、Lean の数学の問題で LLMLean を使用する例です。

llmlean_example.mp4

ラップトップで実行されている LLM、または Open AI API または Together.ai API の LLM を使用できます。

クラウド内の LLM (デフォルト):

1. OpenAI API キーを取得します。

2. 1 つの環境変数を設定します。

 export LLMLEAN_API_KEY=your-openai-api-key

これを行うには、export ステートメントを~/.zshrcファイル (Mac) または~/.bashrc (Linux) に追加し、VS Code を再起動します。

3. llmlean Lakefile に追加します。

require llmlean from git
  " https://github.com/cmu-l3/llmlean.git "

4. 輸入：

 import LLMlean

ここで、以下に説明する戦術を使用してください。

オプション 2: ラップトップ上の LLM:

1. オラマをインストールします。

2. 言語モデルをプルします。

ollama pull wellecks/ntpctx-llama3-8b

3. 2 つの環境変数を設定します。

 export LLMLEAN_API=ollama
export LLMLEAN_MODEL=wellecks/ntpctx-llama3-8b # model name from above

次に、上記の手順 (3) と (4) を実行します。ここで、以下に説明する戦術を使用してください。

オプション 3: クラウド内の LLM (togetter.ai):

1. together.ai API キーを取得します。

2. 2 つの環境変数を設定します。

 export LLMLEAN_API=together
export LLMLEAN_API_KEY=your-together-api-key

次に、上記の手順 (3) と (4) を実行します。ここで、以下に説明する戦術を使用してください。

戦術

llmstep戦術

llmstep "{prefix}"による次の戦術の提案。例:

• llmstep ""

  

• llmstep "apply "

  

提案は Lean でチェックされます。

llmqed戦術

llmqedを介して現在の証明を完了します。例:

• 

提案は Lean でチェックされます。

特にllmqed戦術で最高のパフォーマンスを得るには、Open AI API を使用することをお勧めします。

PFR でのデモ

以下は、 llmqed (OpenAI GPT-4o) を使用して補題を証明する例です。

そして、 llmqed使用して既存の証明の一部を簡素化します。

カスタマイズ

以下を参照してください。

• カスタマイズ