▲

Gemini Deep Think, 국제수학올림피아드(IMO)에서 금메달 기준 공식 달성

 (deepmind.google)
3P by GN⁺ 16시간전 | ★ favorite | 댓글 4개
  • Google DeepMind의 Gemini Deep Think 모델이 2025년 국제수학올림피아드(IMO)에서 금메달 기준 점수(35점) 를 달성함
  • 이 모델은 6문제 중 5문제를 완벽하게 풀었으며, IMO 공식 심사위원단의 평가로 명확하고 정밀한 수학적 풀이를 인정받음
  • 작년 AlphaProof·AlphaGeometry 2의 은메달(28점) 수준에서 크게 도약, 자연어로 공식 문제를 이해하고, 4.5시간 내에 인간처럼 증명을 완성함
  • Deep Think 모드는 병렬 사고(parallel thinking) 와 최신 강화학습을 적용해 여러 해결책을 동시에 탐색·종합, IMO 스타일 문제 해결에 최적화함
  • Google은 앞으로 수학자와 협업을 확대하고, 수학적 추론과 공식 검증 능력을 결합한 차세대 AGI 개발로 나아갈 계획임

Breakthrough Performance at IMO 2025 with Gemini Deep Think

  • Google DeepMind의 Gemini Deep Think는 2025년 국제수학올림피아드(IMO)에서 총 35점(6문제 중 5문제 완벽 해결) 을 받아, 금메달 기준을 공식적으로 달성함
  • IMO 공식 심사위원단은 명확성, 정밀성, 이해하기 쉬운 풀이를 높이 평가했으며, IMO 위원장 Prof. Dr. Gregor Dolinar는 "Google DeepMind가 금메달 점수 35점을 달성했음을 확인한다"는 공식 성명을 발표함
  • 작년 AlphaGeometry·AlphaProof는 전문가가 문제를 자연어→도메인 특화 언어(Lean 등)로 번역해야 했고, 계산도 이틀 이상 소요되었음. 올해 Gemini는 문제 이해부터 증명 작성까지 전 과정을 자연어 기반으로, IMO 대회 시간(4.5시간) 내에 완수함

Making the most of Deep Think mode

  • Gemini Deep Think는 병렬 사고(parallel thinking) 등 최신 연구기법을 적용한 향상된 추론 모드로, 여러 풀이 경로를 동시에 탐색해 최적의 해결책을 도출함
  • 모델은 복잡한 수학 문제 해결을 위해 강화학습 기법과 다양한 IMO 스타일 증명 데이터로 훈련되었으며, IMO 문제 접근법에 관한 일반적 힌트와 팁도 추가로 주입됨
  • 이 Deep Think 모델은 신뢰할 수 있는 일부 수학자 및 전문가에게 테스트 버전이 우선 제공될 예정이며, 추후 Google AI Ultra 구독자 대상으로 공개 계획임

The Future of AI and Mathematics

  • Google DeepMind는 수학 커뮤니티와의 협력을 지속하면서, 자연어 기반 추론뿐 아니라 AlphaGeometry·AlphaProof 등 공식(포멀) 체계 기반 연구도 병행 중임
  • 앞으로는 자연어 이해력과 공식적·검증 가능한 수학적 추론 능력을 결합한 AI가 수학·과학·공학·연구 분야에서 핵심 도구로 자리잡을 전망임
  • DeepMind는 이번 성과를 AGI(범용 인공지능)로 가는 길목에서의 중요한 진전으로 평가하며, 향후 더욱 복잡하고 수준 높은 수학 문제 해결에 도전할 계획임

답변 검증 및 IMO의 공식 입장

  • IMO 조직위원회는 제출된 답변이 완전하고 정확한 솔루션임을 공식적으로 확인함
  • 다만, IMO의 검토는 시스템, 프로세스 또는 기본 모델 자체의 검증까지는 포함하지 않음을 명시함
  • 상세 내용과 확대 해석은 IMO 공식 성명서(자세히 보기) 참고 가능
▲
xguru 16시간전  [-]

OpenAI, 2025 국제수학올림피아드(IMO)에서 금메달급 성과 달성 발표

2일전에 OpenAI가 먼저 발표를 해버려서 김이 샜는데, OpenAI의 Alexander Wei가 IMO랑 논의도 없이 먼저 얘기한건 에티켓이 없는거라는 얘기도 있더군요.
공식적으로 IMO측에서 인정도 안했는데 발표해버려서, AI가 아닌 일반 참여자들의 축하와 공로를 가로챈거라고요.

답변달기
▲
cenoch 9시간전  [-]

덕분에 OAI는 자체 패널이 검증한거지, IMO의 공식적인 채점을 받지도 않은 상황이 된거죠. 게다가 답변의 품질도 제미나이가 좀 더 낫다고 보는 의견이 많은 것을 보면... 더 모양빠지는 상황이지 않나 싶네요. 평판에 대한 리스크 감수는 없고, 성공하면 발표(그것도 공식적인 채점이 아닌 상황에서) 결과가 나쁘면 발을 뺀다는건, 벤치마크에서는 그렇게 해도 돼도, 참가자들이 자신의 이름을 걸고 뛰는 대회에서 보여줄 올바른 모습이 아닌것 같습니다.

답변달기
▲
crawler 14시간전  [-]

구글이랑 OpenAI가 LLM 성능은 비등비등해도 기업의 노련함 차이가 여기서 나는군요

답변달기
▲
GN⁺ 16시간전  [-]
Hacker News 의견

  • AlphaGeometry와 AlphaProof는 자연어 문제를 먼저 Lean과 같은 도메인 특화 언어로 번역한 후, 다시 증명 결과를 자연어로 변환하는 과정을 거쳤음, 그리고 계산에는 2~3일이 소요되었음, 올해의 Gemini 모델은 자연어만으로 공식 문제 설명에서 수학적 증명을 직접 생성하는 엔드 투 엔드 방식을 사용하였음, 즉 Lean으로 먼저 번역하지 않았다는 의미임, 하지만 내부적으로 Lean, 인터넷 검색, 계산기, Python 등의 툴을 사용했는지 명확하지 않음, OpenAI는 자사 모델에서는 이러한 도구를 사용하지 않았다고 밝혔지만 Gemini에도 정확히 해당되는 주장인지는 잘 모르겠음, 두 시스템이 각각 사용하는 계산량, 즉 비용의 대략적인 수준도 알고 싶음, 만약 가격이 엄청나다면 아직 실용성이 떨어진다는 의미임, 아직 공개된 정보가 없으니 엄청나게 비쌀 거라고 추측함, 그리고 "도구 사용 없음, 인터넷 연결 없음"이 확인되었다는 링크를 공유함 https://x.com/FredZhang0/status/1947364744412758305

    • 올해의 Gemini 모델은 자연어만으로 공식 문제 설명에서 수학적 증명을 생성하며, 4.5시간의 대회 시간 내에 모든 과정이 진행됨, 외부 도구를 사용하지 않았음

    • 공식적으로는 Lean과 같은 형식 검증 도구가 IMO 문제를 실제로 풀 때 사용되지 않는다고 하지만, 모델을 학습시키는 과정에서는 사용되는지 궁금함, Google의 2024년 IMO 연구에서는 자연어 증명을 공식적으로 검증 가능한 형식 언어로 변환하는 기술이 있음, 이를 RLVR(강화학습을 통한 검증-보상) 트레이닝에 활용하는 것이 자연스러운 다음 단계라고 생각함, 수학 LLM이 생성하는 모든 추론을 번역하고 검증해 보상 신호로 활용할 수 있다면 보상 신호가 훨씬 촘촘해짐, 완벽한 공식 증명을 얻는 것은 여전히 어렵겠지만, 틀린 추론이나 해독 불가능한 문장은 피하도록 유도하는 데 유용함, 엄청난 계산량과 함께라면 IMO 난이도의 문제도 해결이 가능해짐, AlphaProof처럼 Lean 증명과 LLM 출력을 오가며 추론 공간을 효율적으로 탐색하면 IMO급 문제도 풀 수 있음을 이미 보여줌, 중간 단계를 생략하고 RLVR로 LLM에게 공식 추론을 모방하게 가르치면 비슷한 효율성과 문제 해결 능력을 얻을 수 있지 않나 생각함

    • 왜 Lean을 쓰지 않는지도 궁금함, Lean을 쓰면 요즘에는 문제 풀이가 너무 쉬워진다는 의미인지, 아니면 Lean 자체가 오히려 방해 요인인지 궁금함

    • "도구 사용 없음, 인터넷 연결 없음"이 실제로는 구글 인프라 없이 오프라인에서도 구동될 수 있다는 의미인지, 즉 필요에 따라 로컬에 배포가 가능할 지도 궁금함

  • 올해는 고도화된 Gemini 모델이 자연어로만 공식 문제 설명에서 수학적 증명을 바로 생성했다고 하지만, 나는 오히려 형식화 기술에서 멀어지는 것이 아쉽게 느껴짐, 수학을 진정 자동화하거나, 예를 들어 수천 페이지 분량의 증명을 기계적으로 만들어낼 수준에 도달하려면 형식화 이외에는 길이 없다고 생각함, 그렇지 않으면 여전히 인간 검토자가 필요해지고, 증명을 정말 신뢰할 방법이 없어짐

    • 만약 LLM이 자연어로 엄격한 증명을 만들어낼 수 있다면, Lean과 같은 형식 언어로 증명하는 것도 큰 어려움이 없을 것임, AlphaProof에서 Lean을 사용한 것은 상당히 한정적이고 특정 수학 문제에 특화된 방식이었음, 반면 RL 방식과 자연어로 동일한 걸 달성한다면 검증이 까다로운 다양한 분야에도 확장 가능함

    • DeepMind가 현재 공식적으로 미해결 문제들을 형식화해서 기록하는 저장소를 모으고 있다는 사실도 공유함 https://github.com/google-deepmind/formal-conjectures

    • 나는 수학자이지만 더 이상 연구는 하지 않음, 왜 많은 수학자들이 형식 기법에 미온적인지 약간의 맥락을 제공하고 싶음, 현실적으로 수천 페이지 증명을 만들려면 당연히 형식화 없이는 불가능하고, 무언가 "신뢰"하려면 공식적으로 검증해야 한다는 데는 동의함, 하지만 실제로 수학자들이 진정 원하는 것은 "왜" 그 결과가 참인지에 대한 설명임, 진짜 상품은 예-아니오 답이 아니라 그 해석과 이유임, 예를 들어 리만 가설이 아마도 참일 것이라고 다들 생각은 하지만, 그저 정답을 기다리는 건 아님, 심지어 "만약 리만 가설이 참이면 이런 새로운 정리가 성립한다"는 식의 결과도 많음, 증명에서 기대하는 건 근본적으로 새로운 통찰이나, 수 이론에 대한 깊은 이해를 주는 방식임, Lean처럼 공식적으로 참임을 검증만 해주고 인간이 이해조차 못하면 그건 거의 의미가 없음

    • 정확한 형식화는 문제 푸는 것보다 쉬운 편이니, 문제를 먼저 풀고 이후에 형식화해서 확인하는 것도 가능함

    • IMO 문제는 애초에 인간이 도구 없이 풀도록 설계된 문제임, 더 어려운 문제를 모델에게 풀게 한다면 그땐 충분히 도구를 제공할 수 있음, 적어도 인간 수준의 능력을 도구 없이 먼저 재현하는 것은 좋은 방향이라 생각함

  • OpenAI와 Gemini의 답변을 비교해 보면, Gemini 쪽 글쓰기 스타일이 훨씬 명확하게 느껴짐, 제시 방식은 조금 더 나았으면 좋겠지만 증명 내용 자체는 따라가기 쉽고, OpenAI의 답변보다 더 짧으면서도 정돈된 문장으로 이루어져 있음

    • Google의 증명은 아마 사후적으로 요약한 결과일 수도 있고, Tree of Thoughts와 같은 메커니즘의 일부가 요약 과정일 가능성도 있음, 단순하고 수동적으로 "최종 답안을 내라"는 명령 결과는 아닌 것 같음

    • 언급된 OpenAI와 Google의 IMO 증명 결과는 각각 Google 증명 PDF와 OpenAI의 증명 예시 Repository에서 볼 수 있음

  • "4.5시간 대회 내에 모든 과정을 끝냈다"는 점은 OpenAI와 Google 모두 강조했지만, 이 제한이 중요한 의미가 있는지 의문임, 사실상 수백만 개의 병렬 추론 프로세스를 동시에 돌려서 증명을 찾을 수도 있었겠음, 물론 이러려면 결과를 평가하고 최종적으로 제출할 증명을 선정하는 평가용 모델에도 많은 계산량이 필요할 것임, 실제로 수백 년치 GPU 시간이 들어갔을 수 있음, 그렇다 해도 이런 방식이 해답을 찾는다는 점, 그리고 병렬화가 이 정도까지 가능하다는 것 자체가 놀랍긴 함, 결국 AGI를 더 많은 컴퓨팅으로 달성하든 아니든 인간 두뇌는 이렇게 쉽게 확장되지 않으니 결과의 의미는 분명함

    • 실제로 아무도 진짜 수백만 개의 병렬 추론을 실행한 것은 아님, 증명을 나열하는 것 자체가 결정론적 시스템에서는 매우 어려움, 이와 관련해서는 철학과 복잡성 이론의 교차점에 대해 Aaronson의 논문을 강력 추천함 https://www.scottaaronson.com/papers/philos.pdf

  • 지난해의 Lean 특화 시스템에서 자연어 기반의 범용 LLM + RL로 방식이 전환된 점이 매우 흥미로움, 이런 접근이 수학 경진대회 분야 외 영역에서도 성능 향상에 기여할 것으로 예상함, 앞으로 어디까지 확장될 수 있을지 기대됨, 그리고 이번 시스템이 여름에 공개될 예정인 "DeepThink" 모델/기능과도 크게 차이나지 않는 것으로 보임

  • 지금은 마치 기계와의 수학 경쟁에서 Deep Blue와 Kasparov 시기의 순간을 경험하는 느낌임, 불과 몇 년 전보다 엄청난 발전이 있었지만 여전히 제대로 된 AI 수학자에는 한참 부족하다고 생각함, 하지만 참 놀라운 시대에 살고 있음

    • 최근 팟캐스트에서 Terrence Tao도 이런 도구들과 함께 작업하는 데 큰 관심을 보였음, 그는 당분간 최고의 활용 방식이 인간이 아이디어/파라미터를 설정해주고 LLM이 탐색과 증명 등을 병렬적으로 해보는 것이라고 언급함, 체스 엔진 비유도 적절함, 최고의 체스 선수들도 예전에는 다수의 전문가 팀이 분석을 도왔으나, 현재는 슈퍼컴퓨터와 소프트웨어로 수많은 포지션을 분석해서 최고의 아이디어를 뽑고 선수에게 전달함

    • Deep Blue와 천재 아동의 대결에 더 가깝다고 생각함, IMO 참가자는 세계적인 수학자가 아니라 고등학생임

    • 여기의 차이점은 단순한 브루트포스만으로는 시간 내에 고득점을 얻을 수 없다는 점임, 진정한 기술적 이정표이고, Deep Blue 때의 '원칙적으로 가능'과는 다름

  • 6번 문제는 의아함, openai와 deepmind 모두 답변을 내지 못했음, 인간은 부분적 해답이라도 내는데 AI는 답이 없는 것이 이상함, 혹시 LLM이 자신이 푸는 데 실패했다는 걸 스스로 인지한 것인가라는 의문이 듦, LLM의 한계 중 하나가 ‘내가 모른다는 걸 모른다’라는 점이고, 이렇게 되면 솔버 없이 논리적 일관성을 확인한다는 게 거의 불가능하다고 생각함

    • 아마 대회 시간 제한 내에 '생각'을 마치지 못하고 '출력' 단계로 나아가지 못했기 때문일 가능성이 높음

    • 이 한계는 가장 기본적인 프리트레인된 LLM 텍스트 생성에만 해당함, 추가적으로 linear probe(간단한 신경망 계층)를 훈련시켜 confidence score를 출력하게 할 수도 있음, 물론 100% 신뢰할 수는 없지만, 적어도 수학처럼 제한된 영역에 적용하면 꽤 신뢰가 갈 수도 있음

  • 형식 검증 도구 없이 실제로 활용하기에는 여전히 위험이 클 수 있음, 예전 o3도 최신은 아니지만 참고 문헌을 잘 찾고 새로운 불평등을 제안하는 데 강점이 있었음, 하지만 실제 증명 단계에서는 설득력 있게 보이지만 세부에서 틀린 명제나 대수적 실수를 포함한 답변을 내놓을 수 있음, 모델이 더 좋아질수록 이런 미묘한 오류는 오히려 더 찾기 어려울 수 있음

    • o3는 공식적으로 보여질 듯한 논증을 마치 제대로 체계적으로 풀어낸 것처럼 작성하는 성향이 강했음, MathOverflow의 대학원 수준 수학 질문을 여러 개 줘보면 분명히 틀린 답변을 내기도 했음, 때론 복잡한 대수 한가운데서 실수한 부분을 찾아내기가 쉽지 않음, 설득력 있지만 틀린 논거만큼 위험한 것은 없음

  • 왜 그들이 정리 증명기를 사용하지 않았다는 점을 강조하는지 궁금함, 결국 모델 성능을 높이기 위한 어떤 도구든 쓰면 좋은 것 아닌지, 게다가 Gemini도 IMO에 맞춘 방식으로 특화되었음, 강화학습을 통해 다단계 추론/문제 해결/정리 증명 데이터로 모델을 훈련했고, 고품질 수학 문제 해설집들과 IMO 문제 접근법에 관한 힌트도 제공함

    • 정리 증명기를 사용하지 않았다는 점이 강점으로 강조되는 이유는 Gemini가 실질적으로 외부 도구에 의존하지 않고 독립적으로 추론했다는 것이 AI/ML 분야에서는 혁신적임, 추상적 추론은 인지의 핵심임

  • "Gemini Deepthink의 고급 버전"이 실제로는 출시될 Gemini Ultra 구독 제품에 들어갈 Deepthink와는 아마 다르거나, 훨씬 더 많은 테스트 단계 연산량(compute)을 썼을 것이라 추정함, 그래도 OpenAI와 Google이 경쟁하는 모습을 지켜보는 게 재미있음

답변달기