The Decoder • 25일 전

미스트랄 '린스트랄 1.5' 공개, 수학 벤치마크 완벽 통과 및 코드 버그 검출

IMP

7/10

핵심 요약

Mistral AI가 수학적 증명과 소프트웨어 검증을 위해 설계된 오픈소스 모델 'Leanstral 1.5'를 공개했습니다. 이 모델은 공식 수학 벤치마크인 miniF2F에서 100%의 완벽한 정확도를 기록했으며, 실제 오픈소스 코드를 분석해 숨겨진 5개의 보안 버그까지 발견하며 코드 검증 능력을 입증했습니다.

번역된 본문

Mistral의 오픈소스 Leanstral 1.5가 형식 수학(formal math) 벤치마크에서 완벽한 점수를 기록하고 코드 내 실제 버그를 찾아냅니다. Matthias Bastian | 2026년 7월 4일

Mistral AI는 Lean 4 프로그래밍 언어를 위한 형식 검증(formal verification)을 목적으로 구축된 무료 오픈소스 모델(Apache 2.0 라이선스)인 Leanstral 1.5를 출시했습니다. Lean 4는 수학적 증명과 소프트웨어의 정확성을 형식적으로 검증하기 위해 설계되었습니다.

Mistral에 따르면, 이 모델은 고등학교 수준부터 수학 올림피아드 난이도까지 아우르는 형식 수학 벤치마크인 miniF2F에서 100%의 점수를 달성했습니다. 퍼트넘(Putnam) 수학 대회 문제 672개가 포함된 PutnamBench에서는 587개의 문제를 해결했습니다. 또한, 군론(group theory)과 환론(ring theory) 같은 분야에서 석사 및 박사급 수준의 작업을 테스트하는 대수학 벤치마크 FATE-H 및 FATE-X에서는 각각 최고 수준인 87%와 34%의 점수를 기록했습니다.

이 모델은 주로 수학 분야를 위해 학습되었지만, 코드 검증에도 뛰어난 성능을 발휘한다고 Mistral은 밝혔습니다. 실제 진행된 실무 테스트에서 이 모델은 57개의 오픈소스 리포지토리를 스캔하여 Rust 라이브러리인 varinteger의 오버플로우 버그를 포함해 이전에 알려지지 않았던 5개의 버그를 적발했습니다.

해당 모델은 Hugging Face와 무료 API를 통해 사용할 수 있습니다. 모델 학습 과정에는 미드트레이닝(mid-training), 지도 미세 조정(SFT), 그리고 강화 학습(RL)이 포함되었습니다.

[광고 및 뉴스레터 구독 유도 배너 원문 번역 생략]

원문 보기

원문 보기 (영어)

Mistral's open-source Leanstral 1.5 aces formal math benchmarks and catches real bugs in code Matthias Bastian View the LinkedIn Profile of Matthias Bastian Jul 4, 2026 Mistral AI released Leanstral 1.5, a free open-source model (Apache 2.0 license) built for formal verification in the Lean 4 programming language. Lean 4 is designed to formally verify mathematical proofs and software correctness. Mistral says the model hits 100 percent on miniF2F, a formal math benchmark covering problems from high school level up to math olympiad difficulty. On PutnamBench, which includes 672 problems from the Putnam math competition, it solves 587. On the algebra benchmarks FATE-H and FATE-X, which test master's and doctoral-level tasks in areas like group theory and ring theory, it scores top results of 87 and 34 percent. The model was trained mainly for math, but Mistral says it also performs well at code verification. In a hands-on test, it scanned 57 open-source repositories and caught five previously unknown bugs, including an overflow bug in the Rust library varinteger. The model is available through Hugging Face and a free API . Training involved mid-training, supervised fine-tuning, and reinforcement learning. Ad DEC_D_Incontent-1 Ad AI News Without the Hype – Curated by Humans Subscribe to THE DECODER for ad-free reading, a weekly AI newsletter, our exclusive "AI Radar" frontier report six times a year, full archive access, and access to our comment section. Subscribe now Source: Mistral Ask about this article… Search

오픈소스 수학-증명 형식-검증 코드-버그-검출 미스트랄