DeepSeek이 수학 정리 증명 분야에서 특화 모델 Prover-V2를 공개했다. 목표는 AI를 사용해 Lean 4 형식 검증 시스템 내에서 수학 정리를 자동으로 증명하는 것이다.
이 방향이 중요한 이유
수학 정리 증명은 AI 능력의 극한 테스트장이다. 수학은 '거의 맞다'는 것을 인정하지 않는다. 증명은 완전히 맞거나 틀리거나 둘 중 하나다. '95% 정확한 증명'이라는 것은 존재하지 않는다.
형식 검증 시스템(예: Lean 4)은 컴파일러가 구문을 검사하는 것처럼 추론의 각 단계를 검사한다. 한 단계라도 틀리면 전체 증명이 오류가 된다. 이는 AI의 논리적 추론 능력에 대한 가장 엄격한 시험이다.
Prover-V2의 성능
miniF2F 벤치마크에서 Prover-V2는 최신 최고 수준에 근접하거나 일치하는 결과를 달성했다. 사용된 방법은 하위 목표 분해다. 복잡한 증명을 일련의 더 작은 하위 목표로 나누어 하나씩 해결하는 방식이다.
이는 인간 수학자의 사고 방식과 유사하다. 어려운 문제에 직면했을 때, 'A를 증명하려면 먼저 B와 C를 증명해야 하고, B를 증명하려면 먼저 D를 확인해야 한다...'고 생각하는 것이다.
범용 추론 모델과의 차이점
범용 모델(GPT, Claude, Gemini)은 수학적 추론을 위해 Chain-of-Thought(사고의 사슬)에 의존한다. 본질적으로 '자연어로 단계별로 추론하는' 방식이다. 이 방법은 간단한 문제에는 효과적이지만, 복잡한 증명에서는 특정 단계에서 논리적 허점이 쉽게 발생할 수 있다.
Prover-V2는 형식화된 경로를 택하며, 모든 단계가 Lean 4에 의해 검증된다. 장점은 '환각'이 존재하지 않는다는 것이고, 단점은 적용 범위가 매우 좁아 형식화된 시스템 내에서만 작동할 수 있다는 점이다.
의의
수학 정리 증명은 겉보기에는 틈새 시장처럼 보이지만 영향력이 큰 방향이다. AI가 형식화된 시스템 내에서 복잡한 정리를 신뢰할 수 있게 증명할 수 있다면, 소프트웨어 검증, 하드웨어 검증, 암호학 증명 등 일련의 핵심 분야에 적용될 수 있다.
DeepSeek이 이 방향에 투자하고 있다는 것은 범용 대규모 모델 벤치마크 경쟁에만 몰두하는 것이 아니라 기초 과학 도구 구축에도 진지하게 힘을 쏟고 있음을 보여준다.
출처: CocoLoop, DeepSeek Prover-V2 논문