미스트랄AI, 신뢰 가능한 AI 코딩 위한 검증 AI 모델 공개

프랑스 AI 스타트업 미스트랄 AI가 수학적 증명 및 소프트웨어 사양 검증 등을 지원하는 AI 모델 린스트랄(Leanstral)을 공개했다. 린스트랄은 형식 증명 툴 린 4(Lean 4)에 대응하는 오픈소스 AI 에이전트로 수학과 프로그램 정확성을 엄밀히 검증하는 증명 엔지니어링을 지원하는 걸 목적으로 한다.

AI는 고도의 추론, 수학적 증명, 코딩 등이 가능하지만 AI가 완료한 태스크에 문제가 없는지는 인간이 최종 확인·검증해야 한다. 하지만 최첨단 연구 수학이나 복잡한 소프트웨어의 경우 검증 난이도도 높아 인간이 수동으로 리뷰하는 데 필요한 시간과 전문 지식이 엔지니어링 속도를 저해하는 최대 요인이 된다.

이에 미스트랄 AI는 태스크를 실행하는 데 그치지 않고 구현 정당성을 형식적으로 증명할 수 있는 더 유용한 코딩 에이전트 세대를 구상하고 있다. 그 일환으로 수학 연구 및 소프트웨어 검증 등 분야에서 사용되는 증명 지원 시스템 린 4를 위해 설계된 첫 오픈소스 코드 에이전트가 바로 린스트랄이다.

린스트랄은 증명의 구축과 검증을 AI가 보조할 수 있도록 하는 것을 목표로 하며 MoE(Mixture-of-Experts) 아키텍처를 채택하고 있다. MoE 아키텍처는 증명 공학 태스크에 최적화되어 있으며 필요한 전문 모듈만을 능동적으로 선택해 연산을 수행하기 때문에 모델 전체 파라미터 수가 크더라도 실제 연산에서는 일부만을 사용해 높은 성능과 낮은 연산 비용을 동시에 달성할 수 있다. 린을 검증기로 활용하면서 복수 추론 결과를 동시에 생성·검증해 린스트랄은 기존 클로즈드소스 경쟁 제품 대비 높은 성능과 비용 효율을 실현하고 있다.

형식적 증명 완료 및 새로운 수학적 개념에 대한 올바른 정의에 대해 벤치마킹하는 플트이발(FLTEval) 점수를 보면 경쟁 오픈 모델 중 가장 강력한 큐웬3.5 397B-A17B도 4회 시도에서 25.4라는 점수에 도달했지만 린스트랄은 2회 시도 만에 26.3이라는 더 뛰어난 점수를 달성했고 4회 시도에서는 29.3까지 점수를 끌어올렸다.

또 비용 대비 성능을 비교해보면 린스트랄은 소넷 4.6이나 하이쿠 4.5와 동등한 점수를 획득하는 데 필요한 실행 비용이 대폭 낮아졌다. 또 클로드 오퍼스 4.6 점수는 39.6으로 상당히 높지만 실행 비용은 린스트랄을 2회 실행하는 경우보다 92배에 달해 린스트랄이 높은 비용 대비 성능을 갖췄다고 한다.

린스트랄은 아파치 2.0 라이선스 하에 미스트랄 바이브(Mistral Vibe) 내 에이전트 모드 및 무료 API 엔드포인트를 통해 공개되어 연구자와 개발자가 자유롭게 이용·수정할 수 있다. 또 트레이닝 기법 세부 내용을 해설한 기술 리포트와 경시 수학에 편중된 평가에서 탈피하기 위한 새로운 평가 스위트 플트이발도 공개 예정이다. 관련 내용은 이곳에서 확인할 수 있다.