수학 증명을 기계가 검사할 수 있는 형태로 적는 언어이자 증명 보조 도구입니다. 사람이 읽어 판단하던 증명을 컴파일 통과 여부로 바꿔서, AI가 낸 증명의 진위를 자동으로 확인할 수 있게 합니다.
용어 자세히 보기
6B만 활성화되는 119B 모델인데, Lean 4 정리 증명에서 miniF2F를 만점으로 채우고 PutnamBench 672문제 중 587개를 풀었습니다.
점수만 보면 새 영역은 아닙니다.
Seed-Prover 1.5가 이미 miniF2F를 포화시키고 PutnamBench 88%를 찍었기 때문입니다.
달라진 건 값입니다.
Leanstral은 문제당 4달러인데, Seed-Prover 고성능 설정은 문제 하나에 H20 GPU를 10일씩 굴립니다.
70배 넘게 싼 걸 6B 오픈 모델로 해낸 겁니다.
토큰 예산을 늘릴수록 푸는 문제가 계속 늘어서, 5만 토큰이면 44개, 400만 토큰이면 587개까지 갑니다.
쓰임은 수학 밖으로도 넓어졌습니다.
Rust 레포 57개를 자동으로 Lean으로 옮겨 성질을 증명시켰더니, 테스트·퍼징이 놓친 미보고 버그 5개가 나왔습니다.
Choi
같은 점수를 문제당 4달러까지 내린 지점이 이번 공개의 의미입니다. 증명 도구가 코드 버그 탐지로 넘어간 사례도 함께 나왔습니다.
매일 아침 AI 소식도 함께 와요. 언제든 그만 받을 수 있어요.
