llmlean

LLMLano

LLMlean integra LLM y Lean para sugerencias tácticas, finalización de pruebas y más.

A continuación se muestra un ejemplo del uso de LLMLean en problemas de Matemáticas en Lean:

llmlean_example.mp4

Puede utilizar un LLM ejecutándose en su computadora portátil, o un LLM de Open AI API o Together.ai API:

LLM en la nube (predeterminado):

1. Obtenga una clave API de OpenAI.

2. Establecer 1 variable de entorno:

 export LLMLEAN_API_KEY=your-openai-api-key

Para hacerlo, agregue la declaración de exportación al archivo ~/.zshrc (en Mac) o ~/.bashrc (Linux) y reinicie VS Code.

3. Agregue llmlean al archivo lake:

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

4. Importar:

 import LLMlean

Ahora utilice una táctica que se describe a continuación.

Opción 2: LLM en su computadora portátil:

1. Instalar ollama.

2. Extraiga un modelo de lenguaje:

ollama pull wellecks/ntpctx-llama3-8b

3. Establezca 2 variables de entorno:

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

Luego siga los pasos (3) y (4) anteriores. Ahora utilice una táctica que se describe a continuación.

Opción 3: LLM en la nube (together.ai):

1. Obtenga una clave API together.ai.

2. Establezca 2 variables de entorno:

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

Luego siga los pasos (3) y (4) anteriores. Ahora utilice una táctica que se describe a continuación.

Táctica

táctica llmstep

Sugerencias de tácticas siguientes a través de llmstep "{prefix}" . Ejemplos:

• llmstep ""

  

• llmstep "apply "

  

Las sugerencias se verifican en Lean.

tactica llmqed

Complete la prueba actual a través de llmqed . Ejemplos:

• 

Las sugerencias se verifican en Lean.

Para obtener el mejor rendimiento, especialmente para la táctica llmqed , recomendamos utilizar la API Open AI.

Demostración en PFR

A continuación se muestra un ejemplo de demostración de un lema con llmqed (OpenAI GPT-4o):

Y usar llmqed para simplificar parte de una prueba existente:

Personalización

Por favor vea lo siguiente:

• Personalización