llmlean

LMLean

يدمج LLMlean بين LLMs وLean للحصول على اقتراحات تكتيكية وإكمال الإثبات والمزيد.

فيما يلي مثال لاستخدام LLMLean في مسائل الرياضيات في Lean:

llmlean_example.mp4

يمكنك استخدام LLM الذي يعمل على الكمبيوتر المحمول الخاص بك، أو LLM من Open AI API أو Together.ai API:

LLM في السحابة (افتراضي):

1. احصل على مفتاح OpenAI API.

2. تعيين متغير البيئة 1:

 export LLMLEAN_API_KEY=your-openai-api-key

للقيام بذلك، قم بإضافة عبارة التصدير إلى ملف ~/.zshrc (في نظام Mac) أو ~/.bashrc (Linux)، وأعد تشغيل VS Code.

3. أضف llmlean إلى ملف Lakefile:

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

4. يستورد:

 import LLMlean

الآن استخدم التكتيك الموضح أدناه.

الخيار 2: LLM على الكمبيوتر المحمول الخاص بك:

1. قم بتثبيت أولاما.

2. سحب نموذج اللغة:

ollama pull wellecks/ntpctx-llama3-8b

3. قم بتعيين متغيرين للبيئة:

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

ثم قم بالخطوتين (3) و (4) أعلاه. الآن استخدم التكتيك الموضح أدناه.

الخيار 3: LLM في السحابة (together.ai):

1. احصل على مفتاح Together.ai API.

2. قم بتعيين متغيرين للبيئة:

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

ثم قم بالخطوتين (3) و (4) أعلاه. الآن استخدم التكتيك الموضح أدناه.

التكتيكات

تكتيك llmstep

اقتراحات التكتيك التالي عبر llmstep "{prefix}" . أمثلة:

• llmstep ""

  

• llmstep "apply "

  

يتم فحص الاقتراحات في Lean.

تكتيك llmqed

أكمل الإثبات الحالي عبر llmqed . أمثلة:

• 

يتم فحص الاقتراحات في Lean.

للحصول على أفضل أداء، خاصة بالنسبة لتكتيك llmqed ، نوصي باستخدام Open AI API.

العرض التوضيحي في PFR

فيما يلي مثال على إثبات lemma باستخدام llmqed (OpenAI GPT-4o):

واستخدام llmqed لجعل جزء من الدليل الموجود أكثر بساطة:

التخصيص

يرجى الاطلاع على ما يلي:

• التخصيص