니어AI, 111달러로 수학 672문제 풀이 주장

니어AI(NEAR AI)가 수학 형식증명 벤치마크 풋넘벤치(PutnamBench)의 린4(Lean 4) 문제 672개를 총 111달러(약 15만원)에 풀었다고 주장했다. 수치가 같은 조건에서 재현되면 AI 에이전트의 비용 효율을 보여주는 사례가 될 수 있다.

크립토브리핑(CryptoBriefing)은 니어AI의 린 에이전트가 풋넘벤치 전 문항을 풀었고 경쟁 시스템보다 250배 낮은 비용을 기록했다고 전했다. 다만 이 비교는 어떤 모델, 실행 예산, 탐색 방식, 재시도 구조를 같은 조건으로 맞췄는지까지 완결적으로 제시되지는 않았다.

현재 확인되는 핵심 사실은 니어AI가 672개 문제 완주와 총비용 111달러를 제시했다는 점이다. 풋넘벤치 공개 리더보드에 같은 결과가 독립 반영된 단계는 아니다.

풋넘벤치 공식 저장소는 린4 기준 문제 수를 672개로 제시한다. 이 벤치마크는 미국·캐나다 대학 수학경시대회인 풋넘 문제를 린4, 이사벨(Isabelle), 코크(Coq) 같은 형식언어로 바꿔 자동 정리증명 능력을 평가한다.

형식증명은 AI가 단순히 답을 맞히는 수준을 넘어, 기계가 검증할 수 있는 증명 절차를 내놓는지를 본다. 저장소가 공개 증명 코드를 확인용 증거처럼 쓰지 말라고 안내하는 것도 결과 수치만큼 재현 절차와 검증 방식이 중요하다는 뜻이다.

니어AI의 주장이 니어프로토콜(NEAR) 생태계에서 의미를 갖는 이유는 니어AI가 ‘검증 가능한 AI’를 전면에 세워 왔기 때문이다. NEAR 공식 AI 페이지는 사용자 소유 AI, 신뢰실행환경(TEE), 실시간 검증을 핵심 구조로 설명한다.

신뢰실행환경은 데이터를 격리된 하드웨어 환경에서 처리해 외부 접근을 제한하는 기술이다. 블록체인과 결합할 경우 AI 추론 과정, 결제, 에이전트 실행을 얼마나 검증 가능하게 만들 수 있는지가 쟁점이 된다.

니어AI는 2월 아이언클로(IronClaw), 컨피덴셜 GPU 마켓플레이스(Confidential GPU Marketplace), 멀티모달 기밀 추론을 공개하며 에이전트가 계산하고 거래하고 협업하는 인프라를 강조했다. 이번 풋넘벤치 주장은 그 기술 서사에 비용 효율 수치를 더한 사례다.

본지는 앞서 니어AI가 NEAR 스테이킹을 AI 컴퓨트 이용권과 연결한 구조를 보도했다. 당시 핵심은 일반 스테이킹 수익보다 AI 서비스 결제와 프라이버시였고, 이번 주장은 같은 흐름에서 검증형 AI 인프라의 성능 비용을 내세운 것이다.

형식증명 분야의 경쟁도 이미 진행 중이다. 미스트랄AI(Mistral AI)는 7월 2일 공식 발표에서 린스트랄 1.5(Leanstral 1.5)가 풋넘벤치 587/672를 달성했다고 밝혔다.

미스트랄AI는 같은 발표에서 문제당 약 4달러(약 5400원)의 비용을 제시했다. 로지컬 인텔리전스(Logical Intelligence)는 알레프 프로버(Aleph Prover)가 1월 6일 기준 풋넘벤치 668/672를 풀었고, 해결 문제당 평균 비용이 약 68달러(약 9만1800원)라고 밝혔다.

이 비교만 놓고 보면 니어AI의 총비용 111달러 주장은 눈에 띈다. 그러나 각 시스템은 모델 구조, 탐색 방식, 실행 예산, 문제 재시도 조건이 달라 비용 비교를 그대로 우열 판단으로 연결하기 어렵다.

풋넘벤치 리더보드도 접근별 컴퓨트 예산을 더 잘 표시하는 방식을 논의 중이라고 적고 있다. 비용 효율 평가는 공식 리더보드와 연구 노트가 같은 기준으로 정리된 뒤에야 더 분명해질 수 있다.

니어AI의 성과가 NEAR 가격이나 생태계 수요에 어떤 영향을 줄지는 기사로 확인된 범위를 넘어선다. 현재 쟁점은 가격 전망이 아니라 검증형 AI 인프라가 실제 벤치마크에서 어느 정도 비용 효율을 냈는지, 그리고 그 결과가 독립 재현될 수 있는지다.