廉潔

LLML精益

LLLMlean 整合了法學碩士和精益，以提供策略建議、證明完成等。

以下是使用 LLMLean 解決精實數學問題的範例：

llmlean_example.mp4

您可以使用在筆記型電腦上執行的 LLM，或是來自 Open AI API 或 Together.ai API 的 LLM：

雲端法學碩士（預設）：

1. 取得 OpenAI API 金鑰。

2. 設定1個環境變數：

 export LLMLEAN_API_KEY=your-openai-api-key

為此，請將匯出語句新增至~/.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：雲端法學碩士 (together.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 "

  

這些建議在精實中進行檢查。

llmqed策略

透過llmqed完成目前證明。範例：

• 

這些建議在精實中進行檢查。

為了獲得最佳效能，特別是對於llmqed策略，我們建議使用 Open AI API。

PFR 中的演示

以下是使用llmqed (OpenAI GPT-4o) 證明引理的範例：

並使用llmqed使現有證明的一部分變得更簡單：

客製化

請參閱以下內容：

• 客製化