렘린

LLMLean

LLMlean은 전술 제안, 증명 완성 등을 위해 LLM과 Lean을 통합합니다.

다음은 Lean 수학 문제에 LLMLean을 사용하는 예입니다.

llmlean_example.mp4

노트북에서 실행되는 LLM을 사용하거나 Open AI API 또는 Together.ai API의 LLM을 사용할 수 있습니다.

클라우드의 LLM(기본값):

1. OpenAI API 키를 받으세요.

2. 1개의 환경 변수를 설정합니다.

 export LLMLEAN_API_KEY=your-openai-api-key

이렇게 하려면 내보내기 문을 ~/.zshrc 파일(Mac) 또는 ~/.bashrc (Linux)에 추가하고 VS Code를 다시 시작하세요.

3. Lakefile에 llmlean 추가합니다.

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. together.ai API 키를 받으세요.

2. 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 데모

다음은 llmqed (OpenAI GPT-4o)를 사용하여 보조정리를 증명하는 예입니다.

그리고 llmqed 사용하여 기존 증명의 일부를 더 간단하게 만듭니다.

맞춤화

다음을 참조하십시오:

• 맞춤화