llmlean

LLMLean

LLMlean mengintegrasikan LLM dan Lean untuk saran taktik, penyelesaian bukti, dan banyak lagi.

Berikut contoh penggunaan LLMLean pada soal-soal Matematika di Lean:

llmlean_example.mp4

Anda dapat menggunakan LLM yang berjalan di laptop Anda, atau LLM dari Open AI API atau Together.ai API:

LLM di cloud (default):

1. Dapatkan kunci API OpenAI.

2. Tetapkan 1 variabel lingkungan:

 export LLMLEAN_API_KEY=your-openai-api-key

Untuk melakukannya, tambahkan pernyataan ekspor ke file ~/.zshrc (di Mac) atau ~/.bashrc (Linux), dan mulai ulang VS Code.

3. Tambahkan llmlean ke lakefile:

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

4. Impor:

 import LLMlean

Sekarang gunakan taktik yang dijelaskan di bawah ini.

Opsi 2: LLM di laptop Anda:

1. Instal ollama.

2. Tarik model bahasa:

ollama pull wellecks/ntpctx-llama3-8b

3. Tetapkan 2 variabel lingkungan:

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

Kemudian lakukan langkah (3) dan (4) di atas. Sekarang gunakan taktik yang dijelaskan di bawah ini.

Opsi 3: LLM di cloud (together.ai):

1. Dapatkan kunci API Together.ai.

2. Tetapkan 2 variabel lingkungan:

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

Kemudian lakukan langkah (3) dan (4) di atas. Sekarang gunakan taktik yang dijelaskan di bawah ini.

Taktik

taktik llmstep

Saran taktik selanjutnya melalui llmstep "{prefix}" . Contoh:

• llmstep ""

  

• llmstep "apply "

  

Sarannya diperiksa di Lean.

taktik llmqed

Lengkapi bukti saat ini melalui llmqed . Contoh:

• 

Sarannya diperiksa di Lean.

Untuk performa terbaik, terutama untuk taktik llmqed , sebaiknya gunakan Open AI API.

Demo di PFR

Berikut ini contoh pembuktian lemma dengan llmqed (OpenAI GPT-4o):

Dan menggunakan llmqed untuk membuat bagian dari bukti yang ada menjadi lebih sederhana:

Kustomisasi

Silakan lihat yang berikut ini:

• Kustomisasi