เยี่ยมเลย

LMLลีน

LLMlean ผสานรวม LLM และ 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. ตั้งค่าตัวแปรสภาพแวดล้อม 2 รายการ:

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

จากนั้นทำตามขั้นตอน (3) และ (4) ด้านบน ตอนนี้ใช้กลยุทธ์ที่อธิบายไว้ด้านล่าง

ตัวเลือกที่ 3: LLM ในระบบคลาวด์ (together.ai):

1. รับคีย์ API ของ together.ai

2. ตั้งค่าตัวแปรสภาพแวดล้อม 2 รายการ:

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

จากนั้นทำตามขั้นตอน (3) และ (4) ด้านบน ตอนนี้ใช้กลยุทธ์ที่อธิบายไว้ด้านล่าง

กลยุทธ์

ชั้นเชิง llmstep

คำแนะนำกลยุทธ์ถัดไปผ่าน llmstep "{prefix}" ตัวอย่าง:

• llmstep ""

  

• llmstep "apply "

  

คำแนะนำจะถูกตรวจสอบในแบบลีน

llmqed กลยุทธ์

กรอกหลักฐานปัจจุบันผ่าน llmqed ตัวอย่าง:

• 

คำแนะนำจะถูกตรวจสอบในแบบลีน

เพื่อประสิทธิภาพที่ดีที่สุด โดยเฉพาะอย่างยิ่งสำหรับกลยุทธ์ llmqed เราขอแนะนำให้ใช้ Open AI API

การสาธิตใน PFR

นี่คือตัวอย่างของการพิสูจน์บทแทรกด้วย llmqed (OpenAI GPT-4o):

และใช้ llmqed เพื่อทำให้ส่วนหนึ่งของการพิสูจน์ที่มีอยู่ง่ายขึ้น:

การปรับแต่ง

โปรดดูสิ่งต่อไปนี้:

• การปรับแต่ง