미스트랄 AI(Mistral AI)가 형식 검증(formal verification) 분야의 새로운 지평을 열 'Leanstral 1.5' 모델을 공개했습니다. Lean 4 언어 기반의 이 모델은 총 119B 파라미터 중 6B의 활성 파라미터만을 사용하며, Apache-2.0 라이선스로 배포되어 누구나 자유롭게 접근하고 활용할 수 있습니다. 이는 형식 검증을 실제 개발 환경에 더 가깝게 통합하려는 노력의 일환으로, 수학적 증명뿐만 아니라 실제 소프트웨어 코드의 안정성을 높이는 데 기여할 것으로 기대됩니다.
Leanstral 1.5는 중간 학습, 지도 미세조정, 그리고 CISPO 기반 강화학습의 3단계 훈련 과정을 거쳤습니다. 특히 강화학습 단계에서는 모델이 정리(theorem)를 증명하거나 반증하고, Lean 컴파일러의 피드백을 바탕으로 증명을 반복 수정하는 '멀티턴 환경'과, 개발자처럼 파일을 편집하고 bash 명령을 실행하며 실시간 피드백을 받는 '코드 에이전트 환경'을 통해 실제와 같은 복잡한 작업을 학습했습니다. 이러한 훈련 덕분에 miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34% 등 수학 증명 벤치마크에서 최고 수준의 성능을 달성했으며, AVL 트리의 O(log n) 시간 복잡도 증명과 같은 복잡한 실제 코드 속성 검증도 성공적으로 수행했습니다. 또한, Rust 코드를 Lean으로 변환하는 파이프라인을 통해 57개 저장소에서 11개의 실제 버그를 찾아내는 등 실용적인 가치를 입증했습니다.
Leanstral 1.5의 등장은 형식 검증의 접근성을 크게 높여 소프트웨어 개발의 신뢰도를 향상시킬 잠재력을 가집니다. 기존에는 고도로 전문화된 지식과 많은 시간이 요구되었던 형식 검증 작업을 AI 모델이 보조함으로써, 더 많은 개발자가 복잡한 시스템의 정확성을 검증하고 잠재적인 버그를 조기에 발견할 수 있게 될 것입니다. 특히, 오픈소스 가중치와 무료 API 제공은 연구자와 개발자들이 Leanstral 1.5를 활용하여 정리 증명, 증명 디버깅, 코드 저장소 기여 등 다양한 증명 엔지니어링 작업에 즉시 적용할 수 있도록 지원합니다. 이는 소프트웨어의 품질과 보안을 강화하는 데 중요한 역할을 할 것이며, 궁극적으로는 더욱 견고하고 신뢰할 수 있는 디지털 생태계를 구축하는 데 기여할 것으로 보입니다.