LLMlean integriert LLMs und Lean für Taktikvorschläge, Proof-Vervollständigung und mehr.
Hier ist ein Beispiel für die Verwendung von LLMLean bei Problemen aus der Mathematik in Lean:
Sie können ein LLM verwenden, das auf Ihrem Laptop ausgeführt wird, oder ein LLM der Open AI API oder Together.ai API:
Holen Sie sich einen OpenAI-API-Schlüssel.
Legen Sie eine Umgebungsvariable fest:
export LLMLEAN_API_KEY=your-openai-api-key Fügen Sie dazu die Export-Anweisung zur Datei ~/.zshrc (auf Mac) oder ~/.bashrc (Linux) hinzu und starten Sie VS Code neu.
llmlean zur Lakefile hinzufügen: require llmlean from git
" https://github.com/cmu-l3/llmlean.git " import LLMleanWenden Sie nun eine der unten beschriebenen Taktiken an.
Ollama installieren.
Ziehen Sie ein Sprachmodell:
ollama pull wellecks/ntpctx-llama3-8b export LLMLEAN_API=ollama
export LLMLEAN_MODEL=wellecks/ntpctx-llama3-8b # model name from aboveFühren Sie dann die oben genannten Schritte (3) und (4) aus. Wenden Sie nun eine der unten beschriebenen Taktiken an.
Holen Sie sich einen Together.ai-API-Schlüssel.
Legen Sie zwei Umgebungsvariablen fest:
export LLMLEAN_API=together
export LLMLEAN_API_KEY=your-together-api-keyFühren Sie dann die oben genannten Schritte (3) und (4) aus. Wenden Sie nun eine der unten beschriebenen Taktiken an.
llmstep Taktik Vorschläge zur nächsten Taktik über llmstep "{prefix}" . Beispiele:
llmstep ""
llmstep "apply "
Die Vorschläge werden im Lean geprüft.
llmqed -Taktik Vervollständigen Sie den aktuellen Beweis über llmqed . Beispiele:
Die Vorschläge werden im Lean geprüft.
Für die beste Leistung, insbesondere für die llmqed -Taktik, empfehlen wir die Verwendung der Open AI API.
Hier ist ein Beispiel für den Beweis eines Lemmas mit llmqed (OpenAI GPT-4o):
Und die Verwendung von llmqed um einen Teil eines vorhandenen Beweises zu vereinfachen:
Bitte beachten Sie Folgendes:
