672개 형식증명을 111달러에 생성

NEAR AI의 Lean 에이전트가 PutnamBench의 Lean 4 문제 672개를 모두 해결하는 데 총 111달러를 썼다는 결과가 공개됐다. NEAR Protocol 공동창업자이자 현재 코드 형식검증을 연구하는 Alex Skidanov는 두 번째로 저렴한 제출과 비교해 비용이 250분의 1이라고 설명했다. 단순 계산하면 문제 하나당 약 0.17달러다. 높은 정답률뿐 아니라 대규모 형식증명의 경제성을 전면에 내세운 결과다.

“NEAR AI Lean agent solved ALL problems in Putnam Bench.”

PutnamBench는 북미의 대표적인 대학 수학경시대회인 William Lowell Putnam Mathematical Competition 문제를 증명 보조기 언어로 옮긴 평가다. 원 논문은 640개 정리를 바탕으로 Lean 4, Isabelle, Coq에 걸친 1,600개 이상의 수작업 형식화를 제공한다. 분석학, 선형대수, 추상대수, 정수론, 조합론처럼 넓은 분야를 다루며, 초기 평가 당시 기존 신경망·기호 정리증명기는 소수 문제만 해결했다. 자연어 답만 그럴듯하게 만드는 것이 아니라 Lean 커널이 검사할 수 있는 증명을 제출해야 한다는 점이 중요하다.

재현 자료와 비용 산정이 다음 검증대

Skidanov는 시스템이 완전한 오픈소스라고 강조했지만, 게시물 자체에는 실행 로그, 모델별 호출량, 실패 후 재시도 횟수, 하드웨어 비용의 포함 범위가 자세히 적혀 있지 않다. 672라는 숫자도 원 논문이 설명하는 전체 다언어 형식화 수가 아니라 특정 Lean 평가 묶음을 가리킨다. 따라서 이번 성과를 다른 시스템과 비교하려면 같은 문제 버전, 같은 성공 판정, 같은 추론비 회계 기준을 적용해야 한다.

형식증명에서는 최종 산출물을 커널이 검사할 수 있어 일반 자연어 벤치마크보다 오답 판정이 명확하다. 그렇더라도 정리 라이브러리에 이미 있는 보조정리를 얼마나 쉽게 검색했는지, 문제별로 몇 번의 후보를 생성했는지는 시스템의 실제 능력과 비용을 좌우한다. 특히 전체 성공을 주장할 때는 첫 시도 성공률과 무제한 재시도 성공률을 구분해야 한다. 저렴한 실패 반복이 최종 성공률을 높였다면 운영 목적에 따라 평가는 달라질 수 있다.

형식증명 에이전트가 이 비용으로 재현된다면 소프트웨어 검증과 수학 연구에서 사람이 초안을 만들고 기계가 검증하던 흐름이 뒤집힐 수 있다. 다만 벤치마크 학습 오염, 정리 라이브러리 검색 범위, 병렬 샘플 수에 따라 총비용과 일반화 성능이 크게 달라질 수 있다. 다음으로 볼 것은 코드와 실행 명령의 공개, 독립 연구자의 재현, 새로운 비공개 문제에서의 성공률이다. 주장의 출처는 Skidanov의 원문 게시물이며, 평가 설계와 데이터는 PutnamBench 저장소에서 확인할 수 있다.

#lean-4

NEAR AI Lean 에이전트, PutnamBench 672문제를 111달러에 전부 증명