lean-dojo/LeanCopilot

Lean Copilot – Lean 4를 위한 LLM 기반 증명 지원

정의

Lean 4 코드에서 직접 대규모 언어 모델(LLM)을 호출하여 정리 증명 작업을 자동화할 수 있는 라이브러리입니다.
세 가지 주요 전술을 제공합니다:
1. suggest_tactics – 현재 목표에 대한 가능한 Lean 전술 목록을 생성합니다.
2. search_proof – LLM 생성 전술과 aesop 프로버를 결합하여 완전한 증명을 검색합니다.
3. select_premises – Lean 4 및 Mathlib 4의 스냅샷에서 유용한 보조정리를 검색합니다.
Hugging Face에서 호스팅되는 내장 모델(CTranslate2 경유)과 사용자 제공 모델(로컬 바이너리 또는 원격 서버)을 지원합니다.

중요성

기호 정리 증명과 현대 신경 언어 모델을 연결하여 더 빠른 증명 개발과 실험을 가능하게 합니다.
Lean 생태계 내에서 기본적으로 작동하므로 전체 워크플로를 한 곳에서 유지할 수 있습니다 – 외부 스크립트가 필요 없습니다.
오픈소스이며 동료 검토 논문(NeuS 2025에 채택)이 함께 제공됩니다.

주요 구성 요소

구성 요소	역할
NativeGenerator / NativeEncoder	CTranslate2(Lean의 FFI를 통해 연결된 C++ 라이브러리)를 통해 로컬에서 작은 트랜스포머 모델을 실행합니다.
ExternalGenerator / ExternalEncoder	`external_model_api.yaml`에 정의된 간단한 JSON API를 사용하여 다른 곳에서 제공되는 모델(예: Python HTTP 서버)을 호출합니다.
GenericGenerator / GenericEncoder	`generate` / `encode` 타입클래스 메서드를 구현하는 모든 Lean 타입을 연결할 수 있습니다.
Lake 통합	`moreLinkArgs` 스니펫과 `require LeanCopilot` 항목을 제공하여 하위 패키지가 다른 Lean 라이브러리처럼 의존할 수 있게 합니다.
Dockerfile / 빌드 스크립트	네이티브 종속성 문제가 있는 Linux/macOS/WSL 사용자를 위한 준비된 환경을 제공합니다.

빠른 시작(빠른 단계)

종속성 추가 – README에 표시된 대로 lakefile.lean 또는 lakefile.toml에 추가합니다.
실행 – lake update LeanCopilot을 실행한 다음 lake exe LeanCopilot/download를 실행하여 사전 훈련 모델(각각 약 200MiB)을 가져옵니다.
빌드 – lake build(아직 가져오지 않은 경우 lake build LeanCopilot)로 네이티브 코드를 빌드합니다.
Lean 파일에서 import LeanCopilot을 사용하고 시도하세요:
```
example (n m : Nat) : n + m = m + n := by
  suggest_tactics
```
제안된 전술을 클릭하여 삽입하거나 search_proof를 실행하여 시스템이 다단계 증명을 자동으로 시도하게 하세요.

고급 사용법

suggest_tactics 옵션(LeanCopilotTests/TacticSuggestion.lean에 문서화됨)을 통해 생성 하이퍼파라미터(온도, 빔 크기, 반환 전술 수)를 조정합니다.
ModelAPIs.lean 예제를 편집하고 ExternalGenerator를 자체 서버로 지정하여 기본 모델을 더 큰 모델로 교체합니다.
Lake의 -KsystemOpenblas 및 -KsystemCtranslate2Lib 플래그로 시스템 라이브러리 경로를 제공하여 CTranslate2/OpenBLAS를 소스에서 빌드하는 것을 건너뜁니다.

주의 사항

select_premises는 스냅샷에서 원래 정리 이름을 반환합니다. 일부 파생 보조정리는 다른 이름으로 나타날 수 있습니다.
search_proof는 종료 검사를 통과하지 못하는 증명을 생성할 수 있습니다. 정리를 임시로 이름 변경하면 이 문제를 해결할 수 있습니다.
Linux에서 Lean Copilot에 의존하는 실행 파일(lean_exe)은 Lean의 바이너리가 libc++에 링크되어 있으므로 시스템 libstdc++를 포함하기 위해 추가 링커 플래그가 필요합니다.

커뮤니티 및 지원

토론: https://github.com/lean-dojo/LeanCopilot/discussions
이슈: OS 세부 정보, 재현 단계, 디버그 로그와 함께 GitHub 이슈를 엽니다.
기여: 풀 리퀘스트를 환영합니다. 프로젝트는 일반적인 Lean 커뮤니티 규칙을 따릅니다.

인용 연구에서 Lean Copilot을 사용하는 경우, 함께 제공되는 논문을 인용하세요:

@article{song2024leancopilot,
  title={Lean copilot: Large language models as copilots for theorem proving in lean},
  author={Song, Peiyang and Yang, Kaiyu and Anandkumar, Anima},
  journal={arXiv preprint arXiv:2404.12534},
  year={2024}
}

Lean Copilot은 LLM을 Lean 정리 증명 세계에서 일급 시민으로 만들어 신경 언어 모델과 형식 수학 사이의 실용적인 다리를 제공합니다.

lean-dojo/LeanCopilot

Lean Copilot – Lean 4를 위한 LLM 기반 증명 지원

관련