논리적 사고

8,192번 중 한 번 성공한 80.7%를 ‘한 번의 실력’으로 읽어도 될까?

Kimina-Prover Preview v1의 강화학습과 miniF2F pass@8192 결과를 살펴보며 대규모 후보 탐색 성과와 단일 시도 능력, 형식 검증 비용을 구분한다.

그림에서 무엇을 볼까요?

한 문제에서 첫 후보 하나와 8192개 후보 묶음이 각각 검증기로 들어가 pass at 1과 pass at 8192로 나뉘는 도식

100문제에서 첫 후보가 35문제를 풀고, 8,192개까지 허용했을 때 81문제를 풀었다고 하자. 후자는 더 강한 탐색 결과지만 ‘첫 답 81점’은 아니다.

문제당 계산비용이 8,192배가 되는 것도 단순히 가정할 수 없다. 조기 성공과 병렬화가 있기 때문에 실제 후보 수·시간·전력 측정이 필요하다.

프리뷰 v1과 miniF2F 중심 결과이므로 다른 수학 영역·라이브러리·모델 버전에 그대로 일반화할 수 없다.

pass@8192는 큰 탐색 예산을 포함하고 공개된 1.5B·7B 증류 모델이 72B 모델과 같은 수치를 낸다는 뜻이 아니다.

pass@8192가 80.7%면 한 번만 질문해도 약 81% 맞을까?

정리증명 인공지능(AI)를 시험할 ‘환경’은 왜 필요할까? $수학 자료 사전학습에서 후보 풀이가 생성되고 독립 계산·형식 커널 두 검증 문을 거쳐 게시 상자로 들어간다.$ 수학 자료를 더 읽은 언어모델은 증명도 믿을 수 있을까?