딥시크, 대규모 합성 데이터로 AI의 수학 증명 능력 대폭 강화

현대 수학의 증명이 점점 복잡해지면서 동료 평가 과정에서도 오류를 발견하기 어려워지고 있다. 이러한 문제를 해결하기 위해 린(Lean), 이자벨(Isabelle), 코크(Coq) 등의 형식 수학 언어가 개발됐지만, 이를 다루기 위해서는 전문적인 지식과 많은 노력이 필요했다. 딥시크(DeepSeek)는 이러한 한계를 극복하기 위해 대규모 언어 모델(LLM)의 수학 증명 능력을 획기적으로 향상시키는 데 성공했다.

연구팀이 개발한 ‘DeepSeek-Prover’는 고등학교와 대학 수준의 수학 문제에서 추출한 800만 개의 형식 증명 데이터로 학습을 진행했다. 그 결과 기존 최고 성능의 GPT-4를 크게 뛰어넘는 성과를 달성했다. 특히 수학 증명 벤치마크 ‘miniF2F’에서 52%의 정답률을 기록했는데, 이는 GPT-4의 23% 정답률을 두 배 이상 뛰어넘는 수준이다.

DeepSeek-Prover의 진정한 가치는 국제 수학 올림피아드(IMO) 문제를 형식화한 ‘FIMO’ 벤치마크에서 드러났다. 이 모델은 148개의 고난도 문제 중 5개를 해결하는 데 성공했다. GPT-4가 단 한 문제도 풀지 못했다는 점을 고려하면 괄목할 만한 성과다.

연구팀은 이러한 성과가 대규모 합성 데이터의 활용에서 비롯됐다고 설명한다. 기존의 AI 모델들은 학습 데이터 부족으로 인해 성능 향상에 한계가 있었다. 파이썬이나 자바 같은 일반적인 프로그래밍 언어와 달리, 형식 증명 언어는 소수의 수학자들만이 사용하기 때문에 학습에 필요한 데이터를 확보하기가 매우 어려웠다.

연구팀은 이 문제를 해결하기 위해 자연어로 된 수학 문제를 형식 증명으로 변환하는 자동화 기술을 개발했다. 또한 품질이 낮은 증명을 걸러내고 모순된 가설을 제거하는 등 데이터의 질적 향상에도 주력했다.

특히 주목할 만한 점은 반복적 개선 방식을 도입했다는 것이다. 초기에는 제한된 데이터로 학습된 AI 모델을 사용해 형식 증명을 생성하고, 이를 린4(Lean 4) 검증기를 통해 검증했다. 검증을 통과한 증명은 다시 모델 학습에 활용됐다. 이러한 과정을 여러 차례 반복하면서 모델의 성능은 지속적으로 향상됐다.

또한 증명 생성 과정의 효율을 높이기 위해 독특한 방법을 도입했다. 기존에는 증명이 불가능한 명제에 대해서도 시간 제한에 도달할 때까지 계속해서 증명을 시도하는 문제가 있었다. 연구팀은 이를 해결하기 위해 원래 명제와 그 부정을 동시에 증명하는 방식을 채택했다. 둘 중 하나가 증명되면 즉시 전체 과정을 종료하도록 함으로써 자원 낭비를 최소화했다.

이번 연구는 대규모 합성 데이터를 활용해 AI의 수학적 추론 능력을 획기적으로 향상시킬 수 있다는 가능성을 보여줬다. 특히 고등학교와 대학 수준의 수학 문제에서 추출한 데이터만으로도 국제 수학 올림피아드 수준의 문제를 해결할 수 있다는 점은 주목할 만하다.

연구팀은 “현재는 대수학과 정수론 분야에 초점을 맞추고 있지만, 향후 더 다양한 수학 분야로 연구 범위를 확장할 계획”이라고 밝혔다. 또한 연구팀은 데이터셋과 모델을 공개함으로써 자동 수학 증명 분야의 발전을 가속화하겠다는 의지를 표명했다.

이는 AI가 수학 증명이라는 인간 지성의 핵심 영역에서 한 걸음 더 발전했음을 시사한다. 향후 AI는 수학자들의 증명 검증을 돕는 도구를 넘어, 새로운 수학적 통찰을 제공하는 협력자로 발전할 수 있을 것으로 기대된다.

기사에 인용된 리포트 원문은 링크에서 확인할 수 있다.

기사는 클로드 3.5 Sonnet과 챗GPT-4o를 활용해 작성되었습니다. 

관련 콘텐츠 더보기