[혁신] 인공지능과 수학의 만남: DEEPSEEK-PROVER-V2의 자동 정형 증명 기술

인공지능으로 수학의 엄밀함에 도전하다: DeepSeek-Prover-V2가 여는 자동 정형 증명의 미래

인공지능(AI)이 예술 생성, 언어 번역, 글쓰기 보조 등 다양한 영역에서 활약하고 있는 가운데, 최근에는 한층 더 높은 사고 능력이 요구되는 '수학 정형 증명(formal proof)' 영역까지 진입하고 있습니다. 특히 2025년 5월 공개된 DeepSeek-AI의 최신 연구 성과인 DeepSeek-Prover-V2는 자연어 기반의 직관적 추론과 논리적 형식성의 간극을 좁히며 큰 주목을 받고 있습니다. 이 모델은 거대 언어 모델(LLM)이 기성 체계에서 부딪혀온 한계를 돌파하고, Lean 4 같은 형식 언어를 활용한 정형 증명을 자동으로 생성할 수 있는 기술적 혁신을 제시합니다.

수학 정형 증명이란 무엇인가?

정형 증명(Formal Proof)이란, 수학적인 명제를 증명하기 위한 모든 논리적 과정을 명확한 형식 언어로 표현하고 체계화하는 행위를 의미합니다. 이는 인간 수학자가 작성한 직관적 설명과 달리, 프로그래밍 언어처럼 구조화되어 있고, 컴퓨터가 검증 가능한 단계적 논리를 요구합니다. 대표적인 도구로는 Lean, Coq, Isabelle 등의 proof assistant 소프트웨어가 있으며, 이러한 툴들은 시스템 내에서 수학 증명 과정을 논리적으로 완전하게 실행하고 검토할 수 있게 도와줍니다. 하지만 이 정형성은 엄격한 규칙과 수많은 전제 조건을 필요로 하며, 특히 인간 직관에 의존해 '뛰어넘는' 사고를 강력히 배제합니다.

언어 모델에겐 너무 완벽한 세상

GPT-4, Claude, Gemini 등의 언어 모델은 자연어를 기반으로 글을 생성하고 질의응답을 수행하며, 정답을 ‘그럴듯하게’ 설명하는 데 있어 강력한 성능을 보여줍니다. 그러나 그들은 간결하거나 설명적인 해결을 선호하는 성향 때문에 논리적으로 완전한 형식 증명을 생성하는 데 있어 명확성을 결여한 출력을 만들 가능성이 높습니다. 이렇다 보니 기존 LLM 기반 수학 문제 해결은 대부분 ‘스케치’ 중심의 프로세스에 머물렀습니다. 대략적인 아이디어 또는 증명 방향은 자연어로 출력할 수 있었지만, 이 스케치를 Lean과 같은 시스템에서 사용할 수 있는 기계적으로 정확한 입력으로 전환하는 데 큰 어려움이 있었습니다.

DeepSeek-Prover-V2가 가져온 변화

DeepSeek-AI 연구진은 이 문제를 해결하기 위해 자연어-수학 정형의 중간 다리 역할을 할 수 있는 새로운 모델을 출시했습니다. DeepSeek-Prover-V2는 DeepSeek-V3 기반의 자연어 설명 생성기와, 70억 매개변수 규모의 프로버(Prover) 모델을 결합하여, 복잡한 수학 증명을 하위 목표 분해(Subgoal Decomposition) 기술로 접근합니다.

다음은 프로세스의 개요입니다:

① DeepSeek-V3가 인간과 유사한 자연어 스케치(예비 증명)를 생성
② 이를 기초로 Lean 4 언어 기반의 형태로 불완전한 정형 증명을 생성
③ 각 하위 목표는 공식적으로 ‘have’ 문장으로 표현되어 증명이 필요함을 나타냄
④ 7B 사이즈의 프로버 모델이 각 하위 목표를 독립적으로 증명
⑤ 최종적으로 이를 통합해 완전한 Lean 4 정형 증명으로 재구성

이 과정의 장점은 명확합니다. 복잡한 수학적 정리에 대해 인간이 사용하듯 ‘하위 문제로 나누어 해결’하는 이 전략은, 연역적 체계를 유지하면서도 LLM의 자연어 처리 능력을 최대한 활용하는 방식입니다.

학습은 어떻게 이뤄졌나 — 콜드 스타트부터 강화학습까지

DeepSeek-Prover-V2는 사람이 직접 주석한 증명 데이터를 전혀 사용하지 않고, 전 과정에서 합성된 증명 데이터(synthetic data)만을 사용해 학습했다는 점에서 주목받고 있습니다. 이는 누구든 고품질 데이터를 활용해 완전히 새로운 AI 시스템을 훈련할 수 있다는 가능성을 암시합니다. 또한, 연구진은 점진적 난이도 조절(curriculum learning)을 통해 모델이 쉬운 증명부터 어려운 증명으로 자연스럽게 학습 곡선을 따라가도록 설계했습니다. 각각의 하위 목표 증명은 마치 독립된 레벨처럼 작동하며, 초기의 쉬운 문제는 성공률을 높이고, 후속 학습에 자신감을 부여합니다.

두 가지 하위 목표 설계 전략

DeepSeek-Prover-V2의 학습 설계에는 다음과 같은 두 가지 서브골 유형이 포함되어 있습니다.

의존성 포함(dependent subgoals): 이전 단계의 결과를 현재 단계에 활용
독립 구성(independent subgoals): 각 서브골이 독립적으로 존재

이러한 이중 접근은 다양한 수학적 난이도에 대응하는 유연성을 제공합니다.

성능은 어떠한가? — 벤치마크로 본 결과

DeepSeek-Prover-V2는 다음과 같은 대규모 수학 테스트에서 강력한 성과를 거두었습니다:

MiniF2F-test (Pass@8192): 정형 모델 중 최고 수준인 88.9% 정답률
PutnamBench (658개 문제 중 49개 해결): 미국 푸트남 수학대회 스타일의 고난도 문제에서 우수한 성능
AIME 2024/2025 문제(15개 중 6개 해결): 실사용 문제 접근성 입증
ProverBench 데이터셋 구축: 325개의 Lean 기반 문제로 구성된 새 테스트셋 제안

이러한 수치는 단순한 모델 시험이 아니라, 실제의 수학 교육과 학문 연구 분야로 AI가 들어올 준비가 되었다는 신호탄으로 해석할 수 있습니다.

이 기술은 어디에 활용될 수 있을까?

DeepSeek-Prover-V2 같은 시스템은 단지 연구 도구로 머무르지 않습니다. 다음과 같은 분야에 적용되어 AI의 가능성을 확장시킬 수 있습니다:

수학 교육 보조 – 고등학생이나 대학생이 정형 논리를 이해하는 데 assisted tool로 대상화 가능
교수나 연구자 보조 – 논문 작성 중 수학 공식화 작업 자동화
형식 검증 – 소프트웨어 개발 시 코드의 기능 검사를 논리적으로 증명
국가 시험 대비 – AIME, IMO 등 수학 경시대회 대비에 활용 가능

마무리: DeepSeek-Prover-V2가 여는 미래

지금까지의 AI는 ‘지식의 모사자’ 역할에 머물렀지만, DeepSeek-Prover-V2는 기계가 창의적으로 사고하고 정형화된 논리를 수행할 수 있다는 실질적 가능성을 제시했습니다. 기존 LLM의 한계를 넘어서기 위한 수많은 시도 중에서도, 이 모델은 입출력의 명확성, 단계적 학습 설계, 벤치마크 성능 등에서 매우 높은 평가를 받을 수 있습니다. 향후 이 기술은 수학 뿐만 아니라 논리적 기반이 필요한 법률, 윤리학, 물리학, 심지어는 철학적 논증까지 적용 가능할 것이라는 기대를 모으고 있습니다. AI와 논리의 융합이라는 새로운 시대, 그 중심에 DeepSeek-Prover-V2가 있습니다.

https://youtube.co.kr/@unganimation-u2j