llmmoyen

LLMLean

LLMlean intègre les LLM et Lean pour des suggestions de tactiques, la réalisation de preuves, etc.

Voici un exemple d'utilisation de LLMLean sur des problèmes de mathématiques en Lean :

llmlean_example.mp4

Vous pouvez utiliser un LLM exécuté sur votre ordinateur portable, ou un LLM de l'API Open AI ou de l'API Together.ai :

LLM dans le cloud (par défaut) :

1. Obtenez une clé API OpenAI.

2. Définir 1 variable d'environnement :

 export LLMLEAN_API_KEY=your-openai-api-key

Pour ce faire, ajoutez l'instruction d'exportation au fichier ~/.zshrc (sur Mac) ou ~/.bashrc (Linux) et redémarrez VS Code.

3. Ajoutez llmlean au fichier lac :

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

4. Importer:

 import LLMlean

Utilisez maintenant une tactique décrite ci-dessous.

Option 2 : LLM sur votre ordinateur portable :

1. Installez Ollama.

2. Extrayez un modèle de langage :

ollama pull wellecks/ntpctx-llama3-8b

3. Définissez 2 variables d'environnement :

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

Effectuez ensuite les étapes (3) et (4) ci-dessus. Utilisez maintenant une tactique décrite ci-dessous.

Option 3 : LLM dans le cloud (ensemble.ai) :

1. Obtenez une clé API Together.ai.

2. Définissez 2 variables d'environnement :

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

Effectuez ensuite les étapes (3) et (4) ci-dessus. Utilisez maintenant une tactique décrite ci-dessous.

Tactique

tactique llmstep

Suggestions de tactiques suivantes via llmstep "{prefix}" . Exemples :

• llmstep ""

  

• llmstep "apply "

  

Les suggestions sont vérifiées en Lean.

tactique llmqed

Complétez la preuve actuelle via llmqed . Exemples :

• 

Les suggestions sont vérifiées en Lean.

Pour de meilleures performances, en particulier pour la tactique llmqed , nous vous recommandons d'utiliser l'API Open AI.

Démo dans PFR

Voici un exemple de preuve d'un lemme avec llmqed (OpenAI GPT-4o) :

Et en utilisant llmqed pour simplifier une partie d'une preuve existante :

Personnalisation

Veuillez consulter ce qui suit :

• Personnalisation