미스트랄 AI(Mistral AI)가 수학 및 컴퓨터 과학 분야의 형식 증명(formal proof) 시스템인 린 4(Lean 4)에 최적화된 새로운 대규모 언어모델(LLM) '린스트랄 1.5(Leanstral 1.5)'를 선보였습니다. 이 모델은 자동 정리 증명(automated theorem proving)과 코드의 자동 형식화(automatic formalization)를 핵심 목표로 삼고 있으며, 현재 무료로 제공되어 연구자 및 개발자들의 접근성을 높였습니다.
린스트랄 1.5는 총 1190억 개의 파라미터(119B total parameters)와 65억 개의 활성 파라미터(6.5B active parameters)로 구성되어 있습니다. 특히 256k에 달하는 긴 컨텍스트 길이(context length)를 지원하여 복잡하고 긴 증명이나 문서 맥락을 효과적으로 처리할 수 있습니다. 미스트랄 AI는 이 모델을 'labs-leanstral-1-5'라는 식별자로 제공하며, 챗 완성(Chat Completions), 함수 호출(Function Calling), 에이전트(Agents), 구조화된 출력(Structured Outputs), 문서 QnA(Document QnA), 임베딩(Embeddings) 등 다양한 API와 연동하여 활용할 수 있도록 했습니다. 현재는 가격이 0달러로 책정되어 실험 및 평가 목적으로 자유롭게 사용할 수 있습니다.
린스트랄 1.5의 출시는 형식 검증(formal verification) 분야에서 AI의 역할이 더욱 중요해지고 있음을 시사합니다. 소프트웨어 버그나 시스템 오류는 막대한 손실로 이어질 수 있기에, 수학적 엄밀성을 기반으로 코드나 시스템의 정확성을 증명하는 형식 검증의 가치는 매우 높습니다. AI가 이러한 복잡한 증명 과정을 자동화하고 형식화하는 데 기여한다면, 소프트웨어 개발의 신뢰성과 효율성을 혁신적으로 개선할 수 있을 것입니다. 이는 특히 고신뢰성 시스템(예: 항공우주, 의료 기기) 개발에 큰 영향을 미칠 것으로 기대됩니다. 다만, 아직은 초기 단계이며 실제 상용 환경에 적용되기까지는 추가적인 연구와 검증이 필요합니다.