Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Created by
- Haebom
Category
Empty
저자
Peiyang Song, Kaiyu Yang, Anima Anandkumar
개요
본 논문은 대규모 언어 모델(LLM)을 증명 보조기(Lean)와 결합한 신경 정리 증명에서 LLM을 인간의 증명 과정을 돕는 조력자(Copilot)로 활용하는 Lean Copilot 프레임워크를 제안합니다. Lean Copilot은 LLM 추론을 Lean 내에서 실행하여 사용자가 사전 훈련된 모델이나 자체 모델을 사용하여 증명 단계 제안, 목표 증명 완성, 관련 전제 선택 등의 기능을 제공합니다. Mathematics in Lean 교재를 사용한 실험 결과, Lean Copilot은 기존의 규칙 기반 자동 증명 시스템(aesop)에 비해 인간의 증명 단계 수를 줄이고, 자동 증명 성공률을 크게 향상시키는 것으로 나타났습니다. 모든 코드와 결과물은 MIT 라이선스 하에 공개됩니다.
시사점, 한계점
•
시사점:
◦
LLM을 증명 보조기와 통합하여 신경 정리 증명의 효율성을 높이는 새로운 프레임워크를 제시합니다.
◦
인간 사용자의 개입을 최소화하면서 정리 증명 자동화를 향상시킵니다.
◦
기존 규칙 기반 시스템보다 우수한 성능을 보여줍니다.
◦
오픈소스로 공개되어 추가 연구를 위한 기반을 마련합니다.
•
한계점:
◦
현재는 Mathematics in Lean 교재에 대한 실험 결과만 제시되어 다른 영역으로의 일반화 가능성에 대한 추가 연구가 필요합니다.
◦
LLM의 성능은 사전 훈련 데이터에 의존적이며, 새로운 유형의 문제에 대한 적응력은 제한적일 수 있습니다.
◦
완전한 자율적인 정리 증명은 아직 어렵고, 여전히 인간의 개입이 필요한 경우가 있습니다.
