廉洁

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使现有证明的一部分变得更简单：

定制化

请参阅以下内容：

• 定制化