Leanstral 1.5: 모두를 위한 증명 풍요

Apache-2.0 라이선스로 공개된 Leanstral 1.5는 총 119B 파라미터 중 6B의 활성 파라미터를 사용하는 모델로, 정식 검증(Formal Verification) 분야에서 압도적인 성능을 보여줍니다.

주요 성과는 다음과 같습니다:

• miniF2F 벤치마크 포화 달성
• PutnamBench 문제 중 587/672개 해결
• FATE-H 87%, FATE-X 34%로 SOTA(State-of-the-art) 기록
• 실제 오픈소스 저장소 57개를 테스트하여 5개의 미발견 버그를 찾아냄

이 모델은 **Mid-training, SFT(Supervised Fine-Tuning), 그리고 CISPO를 활용한 RL(Reinforcement Learning)**의 3단계 과정을 통해 학습되었습니다. 특히 Multiturn 환경과 Code Agent 환경에서의 학습을 통해, 컴파일러 피드백을 받아 증명을 수정하거나 파일 편집 및 Bash 명령어를 실행하며 복잡한 증명 엔지니어링 워크플로우를 수행할 수 있는 능력을 갖췄습니다.

현재 Hugging Face와 무료 API를 통해 이용 가능하며, Lean 4 환경에서 실질적인 증명 엔지니어링 도구로 활용될 수 있습니다.