lean-dojo/LeanCopilot

해결하는 문제

Lean Copilot은 대규모 언어 모델(LLM)을 Lean 정리 증명기 내부에 직접 통합하여 형식적 증명 구축의 번거로운 부분을 자동화합니다. 사용자가 "백지 상태"에 빠지는 문제를 해결하기 위해 증명의 다음 단계를 제안하거나, 완전한 증명을 자동으로 검색해 줍니다.

작동 방식

이 프로젝트는 Lean과 LLM 사이의 네이티브 브리지 역할을 합니다. 사용자는 CTranslate2를 통해 로컬에서 모델을 실행하거나 API를 통해 원격 모델에 연결할 수 있습니다. 주요 기능은 다음과 같습니다:

• 타크틱 제안: 증명을 진행할 수 있는 다음 타크틱 후보를 생성하며, 사용자는 클릭하여 적용할 수 있습니다.
• 증명 탐색: LLM이 생성한 타크틱과 aesop 탐색 엔진을 결합하여 다단계 증명을 찾습니다.
• 전제 선택: 리트리버 모델을 사용해 현재 목표와 관련된 유용한 수학적 전제(Lean 및 mathlib4에서)를 식별합니다.

대상 사용자

AI 보조를 통해 형식화 작업을 가속화하고자 하는 수학자 및 컴퓨터 과학자들, 특히 Lean 정리 증명기를 사용하는 사람들에게 적합합니다.

주요 특징

• 유연한 모델 지원: LeanDojo 내장 모델, 로컬 모델(GPU 유무 상관없이), 사용자 정의 원격 모델을 모두 지원합니다.
• 네이티브 통합: Lean 종속성으로 작동하여 Lean 에디터 내에서 직접 LLM 추론을 트리거할 수 있습니다.
• 확장 가능한 API: TextToText 및 TextToVec 인터페이스를 제공하여 개발자가 Lean에서 커스텀 증명 자동화 또는 기타 LLM 기반 애플리케이션을 구축할 수 있도록 합니다.
• 크로스 플랫폼: Linux, macOS, Windows(WSL 포함)를 모두 지원합니다.