정형 검증 모델 공개와 1M 컨텍스트 API 업데이트 #68
오늘의 레터
Mistral AI, Leanstral 1.5 공개
- Mistral AI가 7월 2일 Lean 4용 정형 검증 모델 Leanstral 1.5를 공개함
- Apache-2.0 라이선스의 무료 공개 모델이며, 총 119B 파라미터 중 6B만 활성화되는 구조라고 밝힘
- miniF2F 포화, PutnamBench 672문제 중 587문제 해결, FATE-H 87%, FATE-X 34%를 기록했다고 발표함
- 학습은 mid-training, 지도 미세조정, CISPO 기반 강화학습의 3단계로 진행됐다고 설명함
- 멀티턴 증명 환경에서는 정리의 증명·반증 시도 후 Lean 컴파일러 피드백을 받아 반복 수정하는 방식임
- 코드 에이전트 환경에서는 파일 수정, bash 명령 실행, Lean 언어 서버 점검을 통해 장기 증명 작업과 코드 검증을 수행함
- 57개 오픈소스 저장소 검증 과정에서 기존에 알려지지 않았던 버그 5건을 찾아냈다고 덧붙임
- Hugging Face와 무료 API로 제공되며, 실사용 가능한 증명 엔지니어링 접근성을 높이는 모델로 제시됨
원문: mistral.ai
DeepSeek, V4 Preview 공개 및 API 지원
- DeepSeek가 4월 24일 DeepSeek-V4 Preview를 공개하고 오픈 웨이트와 기술 보고서를 함께 배포함
- 상위 모델 DeepSeek-V4-Pro는 총 1.6T 파라미터·활성 49B 구조, 보급형 DeepSeek-V4-Flash는 총 284B·활성 13B 구조로 안내됨
- 두 모델 모두 1M 컨텍스트를 기본 지원하며 Thinking 모드와 Non-Thinking 모드를 함께 제공함
- API는 기존 base_url을 유지한 채 모델명만 deepseek-v4-pro 또는 deepseek-v4-flash로 바꾸면 사용 가능함
- OpenAI ChatCompletions API와 Anthropic API 호환을 명시했고, chat.deepseek.com에서는 Expert Mode와 Instant Mode로 체험 가능함
- DeepSeek는 V4-Pro가 에이전트 코딩 벤치마크에서 오픈소스 최고 수준 성능을 보였다고 설명했고, V4-Flash는 단순 에이전트 작업에서 V4-Pro와 비슷한 수준이라고 밝힘
- 긴 컨텍스트 처리에는 토큰 단위 압축과 DSA(DeepSeek Sparse Attention)를 적용했다고 설명함
- 기존 deepseek-chat과 deepseek-reasoner는 2026년 7월 24일 15:59 UTC 이후 완전 종료 예정이며, 현재는 deepseek-v4-flash의 비사고형·사고형 모드로 라우팅됨
원문: api-docs.deepseek.com
참고: github.com · theregister.com
조코레터는 개발자와 만드는 사람을 위해 AI, 소프트웨어, 제품 흐름을 한국어로 정리합니다.
#DeepSeek #Mistral