Leanstral 1.5
·2026.07.01 05:44
Mistral AI가 자동 정리 증명 및 자동 형식화에 최적화된 Lean 4 모델인 Leanstral 1.5를 출시했다.
Mistral AI가 Lean 4 정식 증명 공학(formal proof engineering)에 최적화된 신규 모델인 Leanstral 1.5를 공개했습니다.
이 모델은 자동 정리 증명(automated theorem proving) 및 자동 형식화(autoformalization) 작업에 특화되어 설계되었습니다.
주요 사양 및 특징은 다음과 같습니다:
- 파라미터 규모: 총 119B 파라미터 중 6.5B개의 활성(active) 파라미터 사용
- 지원 기능: Chat Completions, Function Calling, Agents, Structured Outputs, OCR, TTS 등 Mistral AI Studio API의 주요 기능 지원
이 요약은 원문 이해를 돕기 위한 큐레이션입니다. 저작권은 원저작자에게 있으며, 정확한 내용과 맥락은 원문을 확인하세요.
요약 오류, 출처 표기 문제, 삭제 요청은 문의 · 건의로 알려주세요.
