중국 AI, 국제수학올림피아드 금메달급 점수 기록

작성일 08-05

<div id="layerTranslateNotice" style="display:none;"></div> 
 <div class="article_view" data-translation-body="true" data-tiara-layer="article_body" data-tiara-action-name="본문이미지확대_클릭"> 
 <section dmcf-sid="BI3EbX41d6">
 <figure class="figure_frm origin_fig" contents-hash="3422e59f9a3a68ba3ae7d3be36f16b906fbdcff5c4e805325bdb6ce170b34aa3" dmcf-pid="bC0DKZ8tR8" dmcf-ptype="figure">
 <img alt="중국 연구진이 AI로 2025년 IMO 문제 대부분을 풀어 금메달급 점수를 기록했다는 연구결과를 발표했다. 게티이미지뱅크 제공" class="thumb_g_article" data-org-src="https://t1.daumcdn.net/news/202508/05/dongascience/20250805174751157ohcj.jpg" data-org-width="680" dmcf-mid="qhouDeIidP" dmcf-mtype="image" height="auto" src="https://img3.daumcdn.net/thumb/R658x0.q70/?fname=https://t1.daumcdn.net/news/202508/05/dongascience/20250805174751157ohcj.jpg" width="658">
 <figcaption class="txt_caption default_figure">
 중국 연구진이 AI로 2025년 IMO 문제 대부분을 풀어 금메달급 점수를 기록했다는 연구결과를 발표했다. 게티이미지뱅크 제공
 </figcaption>
 </figure>
 최근 구글, 오픈AI 등 빅테크 인공지능(AI)이 국제수학올림피아드(IMO)에서 금메달에 해당하는 점수를 획득했다. AI가 어려운 수학 문제를 직접 읽고 논리를 짜고 증명하는 수준에 도달한 것이다. 중국 연구진도 AI로 2025년 IMO 문제 대부분을 풀어 금메달급 점수를 기록했다.
 3일(현지시간) 마크테크포스트, 미디엄 등 미국 매체에 따르면 틱톡 모회사 중국 바이트댄스의 시드(Seed)팀이 레마(lemma)를 먼저 설계하고 복잡한 수학 문제를 스스로 증명하는 증명 추론 AI 모델 '시드-프로버(Seed-Prover)'를 공개했다. 시드-프로버로 IMO 문제 6개 중 5개를 풀어냈다는 결과는 지난 1일 논문 사전공개 사이트 '아카이브(arXiv)'에 공개됐다. 레마는 증명을 위한 디딤돌 역할을 하는 수학 증명을 하기 위해 중간 단계에서 쓰는 보조적인 명제를 가리킨다. 
 대규모언어모델(LLM)을 기반으로 하는 시드-프로버는 사람처럼 증명 과정을 여러 단계로 나누어 사고하고 각 단계를 논리적으로 정리해서 증명할 수 있는 모델이다. 증명 전체를 한 줄씩 쓰기보다는 증명의 구조 자체를 먼저 설계한다. 정리를 증명하기 위해 어떤 레마들을 먼저 증명해야 할지 판단하고 각 레마를 증명한 뒤 이들을 활용해 최종 정리를 증명하는 방식이다. 단순한 증명 생성이 아니라 전체 증명의 전략을 짜는 모델이라고 할 수 있다. 사람처럼 고차원적 구조화 추론을 하는 것이다. 
 시드-프로버는 '린(Lean)'의 피드백, 기존 레마, 자체 증명 요약 데이터를 이용해 증명을 여러 번 시도하고 개선하는 반복적 학습 전략을 수행한다. 마이크로소프트 리서치팀이 수학 증명을 검증하는 소프트웨어로 2013년 개발한 린은 수학 증명 보조프로그램이다. 린이 특정 증명에 대해 맞고 틀렸는지를 판단한 정확성 피드백을 시드-프로버가 학습했다는 의미다. 또 시드-프로버는 과거에 증명된 레마를 재활용하고 스스로 증명한 과정을 요약하고 재구성한 것도 학습했다.
 시드-프로버의 또 다른 주요 특징은 추론을 시작할 때 문제의 난이도에 따라 추론 방식을 바꿀 수 있다는 점이다. 추론 방식 난이도는 경량 모드, 중간 모드, 헤비급 모드 등으로 나뉜다.  경량 모드는 제한된 자원 안에서 빠르게 여러 번 증명을 시도하는 방식, 중간 모드는 증명 전체의 구조를 최적화하는 외부 전략과 어려운 레마 하나하나에 충분한 사고 시간을 들이는 내부 전략이 결합된 방식, 헤비급 모드는 AI가 스스로 '무엇을 증명해야 할지'를 탐색하는 단계까지 나아간다. 헤비급 모드에서 추측 가능한 명제들을 모아두는 '추측 풀(hypothesis pool)'을 만들고 그것들을 하나하나 증명하거나 반박해가며 증명을 완성해 나간다. 
 연구팀은 린의 부족한 기하 문제 처리 능력을 보완하기 위해 시드-프로버와 별도의 AI 엔진 '시드-지오메트리(Seed-Geometry)'를 이용해 2025 IMO 문제 풀이에 도전했다. 2025 IMO는 지난달 10~20일 호주 선샤인코스트에서 열렸다. 
 시드-프로버는 공식적으로 2025 IMO에 참가해 6문제 중 4개를 완전히 풀고 1개를 부분적으로 풀어 은메달에 해당하는 IMO 인증 점수 30점을 획득했다. IMO 문제에서는 답이 나오는 증명 과정을 작성해야 한다. 
 대회 이후 연구팀은 시드-프로버로  2025 IMO의 문제 1개를 추가로 더 풀었다. 6문제 중 총 5문제를 풀어 금메달급 점수를 기록한 것이다. 지금까지 출제된 IMO 문제 155개 중 121개를 완벽히 증명하기도 했다. 
 연구팀은 "시드-프로버는 수학 대회를 위한 AI가 아니다"며 "시드-프로버의 성능은 LLM과 린을 결합했을 때 얼마나 강력한 수학적 추론 시스템이 나올 수 있는지를 시사한다"고 말했다. 이어 "전체 수학 영역에서의 AI 활용 가능성을 탐색하는 데 집중할 계획이다"고 밝혔다. 
 &lt;참고자료&gt;
 -doi.org/10.48550/arXiv.2507.23726 -https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean -https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p2_proof.pdf -https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p3.lean -https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p4.lean -https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver/imo2025/p5.lean
 [이채린 기자 rini113@donga.com]
 </section> 
 </div> 
 Copyright © 동아사이언스. 무단전재 및 재배포 금지.

이전

삼성 갤럭시S25 시리즈 최단기간 300만대 판매

08-05
다음

마이다스그룹 AI역량검사 세계가 인정...네이처 자매지 게재 "면접관보다 정확”

08-05

등록된 댓글이 없습니다.

로그인한 회원만 댓글 등록이 가능합니다.

먹튀폴리스

중국 AI, 국제수학올림피아드 금메달급 점수 기록

멤버랭킹

관련자료

멤버랭킹