llmlean

LLMLLean

LLMlean объединяет LLM и Lean для тактических предложений, завершения доказательств и многого другого.

Вот пример использования LLMLean для решения задач по математике в Lean:

llmlean_example.mp4

Вы можете использовать LLM, работающий на вашем ноутбуке, или LLM из Open AI API или API Together.ai:

LLM в облаке (по умолчанию):

1. Получите ключ API OpenAI.

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: LLM в облаке (together.ai):

1. Получите ключ API Together.ai.

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.

Демо в ПФР

Вот пример доказательства леммы с помощью llmqed (OpenAI GPT-4o):

И использование llmqed для упрощения части существующего доказательства:

Кастомизация

Пожалуйста, ознакомьтесь со следующим:

• Кастомизация