llmlean

LMLean

LLMlean integra LLMs e Lean para sugestões táticas, conclusão de provas e muito mais.

Aqui está um exemplo de uso do LLMLean em problemas de Matemática no Lean:

llmlean_example.mp4

Você pode usar um LLM em execução em seu laptop ou um LLM da API Open AI ou da API Together.ai:

LLM na nuvem (padrão):

1. Obtenha uma chave de API OpenAI.

2. Defina 1 variável de ambiente:

 export LLMLEAN_API_KEY=your-openai-api-key

Para fazer isso, adicione a instrução export ao arquivo ~/.zshrc (no Mac) ou ~/.bashrc (Linux) e reinicie o VS Code.

3. Adicione llmlean ao lakefile:

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

4. Importar:

 import LLMlean

Agora use uma tática descrita abaixo.

Opção 2: LLM em seu laptop:

1. Instale ollama.

2. Extraia um modelo de linguagem:

ollama pull wellecks/ntpctx-llama3-8b

3. Defina 2 variáveis ​​de ambiente:

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

Em seguida, execute as etapas (3) e (4) acima. Agora use uma tática descrita abaixo.

Opção 3: LLM na nuvem (together.ai):

1. Obtenha uma chave de API Together.ai.

2. Defina 2 variáveis ​​de ambiente:

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

Em seguida, execute as etapas (3) e (4) acima. Agora use uma tática descrita abaixo.

Táticas

tática llmstep

Sugestões de próxima tática via llmstep "{prefix}" . Exemplos:

• llmstep ""

  

• llmstep "apply "

  

As sugestões são verificadas no Lean.

tática llmqed

Conclua a prova atual via llmqed . Exemplos:

• 

As sugestões são verificadas no Lean.

Para obter o melhor desempenho, especialmente para a tática llmqed , recomendamos o uso da API Open AI.

Demonstração em PFR

Aqui está um exemplo de prova de um lema com llmqed (OpenAI GPT-4o):

E usando llmqed para simplificar parte de uma prova existente:

Personalização

Por favor, veja o seguinte:

• Personalização