수학 증명과 코드 검증을 위한 오픈소스 AI, 린스트랄 1.5 핵심 정리

이번 글에서는 수학 증명과 코드 검증에 특화된 오픈소스 AI 모델 ‘린스트랄 1.5(Leanstral 1.5)’가 무엇인지, 어떤 배경에서 등장했는지, 그리고 기존 모델 대비 어떤 기술적·실질적 강점을 갖는지 정리합니다.
정형 수학 증명, 논리 검증, 소프트웨어 결함 탐지에 관심 있는 개발자와 연구자라면 왜 이 모델이 주목받는지 이해할 수 있도록 핵심만 쉽게 풀어 설명합니다.

반응형

---

린스트랄 1.5란 무엇인가

린스트랄 1.5는 미스트랄 AI가 공개한 수학 증명 및 코드 검증 전용 오픈소스 AI 모델입니다.
기존 린스트랄-2603의 후속 모델로, 미스트랄 스몰 4 계열을 기반으로 개발됐으며, 정형 증명 보조 시스템 ‘Lean 4’에 최적화된 AI 코드 에이전트라는 점이 핵심입니다.

이 모델의 주요 목적은 두 가지입니다.

• 수학 정리의 논리적 타당성을 기계적으로 증명하거나 반박
• 프로그램 코드의 논리 오류와 숨은 버그를 자동으로 검증

즉, “정답을 그럴듯하게 말하는 AI”가 아니라, 증명 가능한 정확성을 목표로 설계된 모델입니다.

---

Lean 4 기반 정형 증명 환경에 최적화

린스트랄 1.5는 수학 증명을 위한 프로그래밍 언어 Lean과 그 최신 증명 환경인 Lean 4를 중심으로 작동합니다.
Lean은 수학자와 컴퓨터 과학자가 정리와 증명을 코드 형태로 작성하고, 이를 컴파일러를 통해 기계적으로 검증하는 도구입니다.

린스트랄 1.5는 이 환경에서 다음과 같은 역할을 수행합니다.

• 정리를 증명하는 코드 초안 생성
• 컴파일 오류와 타입 오류를 기반으로 증명 수정
• 보조 정리 생성 및 장시간 증명 작업 유지

이 덕분에 사람처럼 “틀리면 고치고, 다시 시도하는” 증명 과정을 자동으로 반복할 수 있습니다.

---

MoE 구조로 구현한 고성능·저비용 모델

린스트랄 1.5의 기술적 특징 중 하나는 전문가 혼합(MoE, Mixture of Experts) 구조입니다.

• 전체 매개변수: 1,190억 개
• 실제 연산에 사용되는 매개변수: 약 65억 개

입력 토큰마다 128개의 전문가 중 4개만 활성화하는 방식으로,
대규모 모델의 추론 성능은 유지하면서 계산 비용은 크게 줄였습니다.

또한 최대 256,000 토큰의 컨텍스트 길이를 지원해, 매우 긴 수학 증명이나 복잡한 코드 검증에도 적합합니다.

---

강화학습 기반 에이전트형 추론 설계

린스트랄 1.5는 단순한 텍스트 학습 모델이 아니라, 에이전트처럼 동작하도록 학습됐습니다.
학습 과정은 다음 세 단계로 구성됩니다.

1. 중간 학습(Mid-training)
2. 지도 미세조정(SFT)
3. CISPO 기반 강화학습(RL)

특히 강화학습은 두 가지 환경에서 진행됐습니다.

1) 수학 정리 증명 환경

• 모델이 증명을 작성
• Lean 컴파일러의 피드백을 받음
• 오류를 수정하며 증명을 반복 개선

2) 실제 개발 환경 시뮬레이션

• 파일 시스템 접근
• Bash 명령 실행
• Lean 언어 서버로 오류·타입 정보 확인
• 미완성 증명 보완 및 보조 정리 생성

이 설계 덕분에 린스트랄 1.5는 장시간 추론이 필요한 문제에서도 성능이 유지됩니다.

---

퍼트넘벤치 최고 성적이 의미하는 것

린스트랄 1.5는 정형 수학 벤치마크에서 매우 인상적인 결과를 보였습니다.

• miniF2F: 검증·테스트셋 모두 100%
• 퍼트넘벤치: 672문제 중 587문제 해결
• FATE-H / FATE-X: 각각 87%, 34%로 SOTA 달성
• FLTEval: Pass@1, Pass@8 모두 큰 폭 개선

특히 퍼트넘벤치는 미국 최고 수준의 수학 경시대회 문제로 구성된 벤치마크로,
이 성적은 단순 계산 능력이 아닌 깊은 논리 추론 능력을 보여줍니다.

---

테스트 타임 스케일링의 강력함

린스트랄 1.5의 가장 큰 강점으로 꼽히는 요소는 테스트 타임 스케일링(Test-time Scaling)입니다.

• 5만 토큰: 44문제 해결
• 20만 토큰: 244문제 해결
• 100만 토큰: 493문제 해결
• 400만 토큰: 587문제 해결

즉, 추론에 더 많은 토큰과 시간을 할당할수록 성능이 지속적으로 개선됩니다.
이는 “어려운 문제일수록 오래 생각하면 더 잘 푼다”는 인간의 사고 방식과 유사합니다.

---

코드 검증에서 실제 버그를 찾아낸 사례

린스트랄 1.5는 수학뿐 아니라 실제 소프트웨어 코드 검증에서도 성과를 냈습니다.

• Rust 코드를 Lean으로 변환하는 Aeneas와 결합
• 57개 오픈소스 저장소 분석
• 47개 속성 위반 발견
• 그중 11개는 실제 버그, 5개는 미보고 신규 버그

대표적으로 Rust 라이브러리의 지그재그 디코딩 함수에서 발생한 64비트 정수 오버플로우 버그를 자동으로 탐지했습니다.
이는 기존 테스트나 퍼징으로는 발견하기 어려운 유형의 문제였습니다.

---

오픈소스 공개와 활용 방법

린스트랄 1.5는 다음 경로로 누구나 사용할 수 있습니다.

• 허깅페이스를 통한 오픈소스 모델 공개
• 미스트랄 AI 에이전트 CLI ‘Mistral Vibe’
• 무료 API 엔드포인트 leanstral-1-5

연구 목적은 물론, 정형 검증이 필요한 실무 환경에서도 접근성이 높은 것이 특징입니다.

---

728x90

린스트랄 1.5는 단순한 성능 향상을 넘어, 정형 수학 증명과 코드 검증을 현실적인 자동화 영역으로 끌어올린 모델입니다.

• 증명 가능한 정확성
• 장시간 추론에 강한 구조
• 압도적인 비용 효율
• 오픈소스 공개

이 네 가지 요소는 앞으로 수학 연구, 안전한 소프트웨어 개발, 고신뢰 시스템 검증 분야에서 AI 에이전트 활용을 빠르게 확산시킬 가능성을 보여줍니다.
린스트랄 1.5는 “AI가 생각해준다”를 넘어, “AI가 증명해준다”는 단계로 가는 중요한 이정표라 할 수 있습니다.

300x250

https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B

mistralai/Leanstral-1.5-119B-A6B · Hugging Face