미스트랄 AI가 형식 검증(formal verification) 분야에서 혁신적인 성능을 제공하는 오픈소스 모델 '린스트랄 1.5(Leanstral 1.5)'를 공개했습니다. 이 모델은 60억 개의 활성 매개변수(active parameters)를 가지고 있으며, 아파치 2.0(Apache-2.0) 라이선스로 무료로 제공됩니다. 린스트랄 1.5는 수학적 추론 능력과 실제 코드 검증 능력에서 기존 모델들을 뛰어넘는 성과를 보여주며, 복잡한 증명(proof) 작업을 더욱 강력하고 접근 가능하게 만들었습니다.
린스트랄 1.5는 미니F2F(miniF2F) 벤치마크를 완전히 통과하고, 퍼트넘벤치(PutnamBench) 문제 672개 중 587개를 해결했습니다. 또한 FATE-H에서 87%, FATE-X에서 34%의 최첨단(state-of-the-art) 결과를 달성했습니다. 특히, 이 모델은 수학적 문제 해결을 넘어 실제 오픈소스 저장소(repository)에서 5개의 알려지지 않은 버그를 발견하며 코드 검증 능력도 입증했습니다. 린스트랄 1.5는 중간 훈련(mid-training), 지도 미세조정(supervised fine-tuning), 그리고 CISPO를 활용한 강화 학습(reinforcement learning)의 3단계 과정을 거쳐 훈련되었으며, 다중 턴(multiturn) 환경과 코드 에이전트(code agent) 환경에서 광범위한 강화 학습을 통해 개발자처럼 파일 편집, 셸(bash) 명령 실행, 린(Lean) 언어 서버 사용 등 실제 증명 엔지니어링 워크플로우를 학습합니다. 이 과정에서 문제당 약 4달러의 비용으로, 경쟁 모델인 시드-프루버 1.5(Seed-Prover 1.5)의 300달러 이상에 비해 훨씬 저렴한 비용 효율성을 자랑합니다.
린스트랄 1.5의 출시는 형식 검증 분야의 실용적 적용 가능성을 크게 확장할 것으로 기대됩니다. 기존에는 고도의 전문성과 막대한 비용이 요구되었던 형식 검증이 이제는 더 많은 개발자와 연구자에게 접근 가능해졌습니다. 특히, 이 모델이 실제 코드에서 새로운 버그를 찾아내는 능력은 소프트웨어 품질과 보안을 향상시키는 데 중요한 역할을 할 수 있습니다. 린스트랄 1.5는 오픈소스 커뮤니티에 기여하고, 복잡한 시스템의 신뢰성을 높이는 데 기여하며, AI 기반 증명 기술의 상업적 활용 가능성을 열어줄 것입니다.