AI 만점 주장 여섯 건, 공식 채점은 둘뿐

만점을 주장한 AI는 여섯, 공식 채점은 둘뿐이었다

7월 16일 상하이에서 국제수학올림피아드(IMO)가 끝났어요. 666명이 응시했고, 42점 만점을 받은 학생은 7명이었어요.

그런데 그 다음 주가 더 시끄러웠어요. 일주일 사이에 여섯 개의 AI 시스템이 “우리도 42점 만점”이라고 발표했거든요. 화웨이, 샤오홍슈, 그리고 독립 테스트에서 나온 네 개 모델까지요.

이 여섯 중에서 IMO 주최 측에 실제로 답안을 넘긴 건 둘뿐이에요. 나머지는 공식 채점 밖의 결과예요. 여기에는 Claude 기반 에이전트가 채점한 테스트와 AxiomProver의 Lean 4 형식 증명이 함께 포함돼요. 공식 채점과는 검증 방식이 달라요.

지금 AI 평가에 부족한 건 더 어려운 문제가 아니에요. 답안을 누가, 어떤 조건에서, 어떻게 채점했는지를 기록으로 남기는 절차예요. 점수만 발표하는 벤치마크가 아니라, 응시 조건과 검증 절차가 있는 시험이 필요하다는 뜻이에요.

---

만점 주장은 여섯 건, 응시 조건은 제각각이었다

인간 쪽 성적은 명확해요. 666명 중 7명이 만점. 학생들은 이틀에 걸쳐 총 9시간 동안 6문제를 풀었어요. 같은 날, 같은 시간, 같은 방에서요. AI 쪽은 이렇게 갈려요.

공식 채점 경로: 화웨이의 Celia와 샤오홍슈의 dots-note-3.0이 인간 대회가 끝난 뒤 문제를 받아 정해진 시간 안에 답안을 제출했고, 그 답안을 IMO 주최 측에 넘겼어요. 샤오홍슈는 “어떤 형태의 인간 개입도 엄격히 금지했다”고 밝혔고요.

독립 테스트 경로: 아래 표에는 연구자가 직접 만든 테스트 환경의 결과와 Axiom Math가 공개한 AxiomProver의 형식 증명 결과가 함께 들어 있어요.

모델	첫 시도	최종	비용	소요 시간
Claude Fable 5	42/42	42/42	약 51달러	2.5시간
GPT-5.6 Sol (xhigh)	39/42	42/42	약 21달러	3.8시간
Kimi K3	36/42	42/42	약 31달러	17.4시간
AxiomProver	형식 증명	42/42	비공개	약 25시간

숫자만 보면 놀랍긴 해요. Fable 5는 한 번에 풀었고, 학생들에게 주어진 9시간의 3분의 1도 안 걸렸어요. AxiomProver는 결이 다른데, Lean 4¹라는 형식 증명 언어로 6문제를 총 7,722줄에 걸쳐 기계가 검증 가능한 증명으로 만들었어요. 3번 문제 하나에만 4,229줄, 869분이 들었고요.

그런데 이 표를 보면서 제가 계속 걸렸던 건 성적이 아니라 조건이었어요.

일반 언어로 쓴 풀이를 AI 에이전트가 채점한 결과와, Lean 4로 증명을 검증한 AxiomProver는 구분해서 봐야 해요. 노력 설정(effort tier)을 어떻게 두느냐에 따라 같은 모델이 11점씩 움직였고요. 그리고 가장 불편한 대목 하나. 같은 테스트에서 Meta의 Muse Spark와 DeepSeek V4 Pro가 3번 문제에 똑같은 오답을 냈어요.

사람 시험장이었으면 이건 곧바로 조사 대상이에요. 같은 오답이 나온 이유를 추가로 확인해야 하기 때문이에요. 학습 데이터가 겹쳤을 수도 있지만, 오답이 같다는 사실만으로 독립적으로 풀지 않았다고 결론낼 수는 없어요. 그런데 벤치마크에는 그 상황을 다룰 절차 자체가 없어요. 그냥 둘 다 ‘오답 1개’로 기록되고 끝이에요.

---