datrs/varinteger

의 zigzag 디코딩(decode) 처리 과정에 부호를 잘못 다루는 오버플로(overflow)가 숨어 있었다. 디버그 빌드(debug build)에서는 크래시(crash)가 발생하고, 릴리스 빌드(release build)에서는 조용히 값이 망가지는 종류의 버그다. GitHub의 Issue에는 아무도 올리지 않았었다. 이것을 발견한 것은 보안 연구자도, 퍼징(fuzzing) 도구도 아닌, Lean 4의 증명을 작성하기 위해 훈련된 Mistral의 모델, Leanstral 1.5였다.

코드 리뷰를 하는 LLM은 드물지 않다. 하지만 "버그가 있을 것 같습니다"라고 지적하는 것과, "이 함수는 주어진 불변 조건(invariant condition)을 만족하지 않는다"라고 컴파일러(compiler)에게 증명하게 하는 것은 신뢰도가 전혀 다르다. 전자는 그럴듯한 추측이며 틀릴 때도 있다. 후자는 수학적으로 체크되었으며, 통과한다면 거짓말을 할 수 없다. Leanstral 1.5가 흥미로운 점은, 후자를 수행하기 위해 만들어진 모델이 실제로 존재하는 57개의 OSS 리포지토리(repository)에서 47건의 성질 위반과 11건의 진짜 버그를 찾아냈으며, 그중 5건은 미보고된 것이었다는 점에 있다.

Lean 4는 정리 증명 지원 시스템(proof assistant)이라고 불리는 도구다. 수학의 정리나 프로그램의 성질을 형식 언어(formal language)로 작성하고, 그 증명을 기계가 한 줄씩 검증한다. 증명이 통과되면 그것은 "옳다는 것이 확인되었다"를 의미하며, 인간의 리뷰와 같은 간과가 원리적으로 들어갈 수 없다.

이 지점이 LLM과 궁합이 좋다. 일반적인 생성 AI는 자신만만하게 틀리지만(이른바 할루시네이션 (hallucination)), Lean 4에서는 증명을 작성해도 컴파일러가 통과시키지 않으면 즉시 "불합격"이 반환된다. 즉, 출력의 정확성을 외부의 엄격한 채점자가 보증해 준다. 모델은 컴파일러의 에러(error)를 읽고 다시 작성하며, 통과할 때까지 다듬는다. 속임수가 통하지 않는 환경에서 돌리기 때문에, 강화학습 (RL)의 보상(reward)도 깔끔하게 설계할 수 있다. Mistral은 이 학습을 중간 학습, 지도 학습 기반 파인튜닝 (supervised fine-tuning), CISPO라는 강화학습의 3단계로 진행했다고 밝혔다.

증명 AI의 실력은 지금까지 수학 올림피아드급 문제를 모은 miniF2F나, Putnam(전미 대학 수학 경시 대회) 유래의 PutnamBench로 측정되어 왔다. Leanstral 1.5의 수치를 보면, 이 무대가 끝나가고 있음을 알 수 있다.

벤치마크	Leanstral 1.5	비고
miniF2F (val+test)	100%	Mistral에 따르면 "포화"
...

miniF2F에서 100%라는 것은, 이 검증 세트에서는 더 이상 차이를 낼 수 없다는 뜻이다. 벤치마크가 만점이 되면, 다음은 실제 코드로 축이 옮겨간다. 이번 발표가 버그 발견 실적을 전면에 내세우고 있는 것은 그 이행을 상징하고 있다.

비용 측면의 차이도 무시할 수 없다. PutnamBench에서 경쟁 모델인 Seed-Prover 1.5를 7문제 앞서면서도, 한 문제당 약 $4로 해결한다. Mistral은 이를 Seed-Prover의 고설정 시 한 문제당 약 10 H20-day(GPU 약 10일분), 금액으로 $300 이상 걸리는 것과 대비시키고 있다. 80배 가까운 효율 차이다. 증명 탐색을 자본으로 밀어붙이던 단계에서, 실무에 적용 가능한 가격대로 내려온 것이다.

이전 세대인 Leanstral-2603(3월 공개, Mistral의 첫 Lean 4용 오픈 소스 코드 에이전트)에서 본질적으로 변한 것은, "증명을 한 번에 내뱉는" 모델에서 "리포지토리 안에서 작업하는 에이전트"로의 성격 변화다.

Leanstral 1.5는 실제 파일 시스템 위에서 동작한다. 파일을 편집하고, bash를 실행하며, Lean language server가 반환하는 골(goal, 남은 증명 목표)·타입(type)·에러(error)를 실시간으로 읽으면서, 부분 증명을 채우고, 보조 정리(lemma)를 직접 만들며, 컨텍스트(context)가 넘치면 요약(compaction)하여 긴 작업을 계속한다. 이는 서두의 버그 발견이 단순한 채점이 아니라, 실제 코드에 증명을 작성하여 반례를 찾아내는 워크플로우(workflow)였음을 설명해 준다. 59.0%의 SWE-Bench를 목표로 하는 범용 코딩 에이전트와는 방향이 다르며, "정확성을 기계 증명으로 확보한다"라는 한 점에 특화되어 있다.

아키텍처는 MoE(Mixture of Experts)로, 총 파라미터(parameter) 119B, 토큰당 6.5B가 유효하다(128개의 전문가 중 4개가 활성화). Mistral Small 4 계열이며, 컨텍스트 길이(context length)는 256k이다. 긴 증명 파일과 관련 코드를 함께 담을 수 있다. 라이선스는 Apache 2.0이며, 가중치(weight)를 그대로 상업적 이용할 수 있다.

가중치와 API가 모두 공개되어 있다. 확인된 식별자는 다음과 같다.

# 가중치 (Apache 2.0)
mistralai/Leanstral-1.5-119B-A6B # Hugging Face
# 무료 API 엔드포인트 모델 ID
...

자신의 실무에 즉시 적용할 수 있느냐고 묻는다면, Lean 4로 성질을 기술할 수 있는 사전 지식이 필요하기 때문에 만인을 위한 것은 아니다. 다만, 암호학이나 금융 계산, 시리얼라이저(serializer)와 같이 "고장 나면 조용히 틀리는" 코드를 가지고 있다면, 그 부분만 형식 검증 (formal verification)으로 고정하는 선택지가 Apache 2.0 라이선스로 문제당 4달러의 비용에 포함되어 제공된다는 점은 큰 의미가 있다. 생성형 AI의 약점은 정확성의 보장이 없다는 것이었으나, 컴파일러 (compiler)를 채점자로 세운 이 계열은 그 약점을 정면으로 돌파하고 있다. miniF2F가 만점이 된 지금, 다음에 포화시킬 대상은 우리의 리포지토리 (repository)가 될 것이다.