DeepSeek, 수학 정리 자동 증명 모델 공개

DeepSeek는 수학 정리를 자동으로 증명하는 인공지능 모델 "DeepSeek-Prover-V2"를 공개했다. 이 모델은 오픈소스로 제공되며, 수식의 형식적 증명을 작성·검증하는 프로그래밍 언어 "Lean 4"에 대응한다.

"정리 증명"이란 수학적 명제가 올바름을 컴퓨터가 논리적으로 확인하는 과제를 의미한다. 이는 단순한 계산과는 다르며, 복잡한 추론의 축적이 필요하기 때문에 인공지능에게 난이도 높은 분야로 여겨져 왔다. 근래에 대규모 언어 모델(LLM)의 능력 향상에 따라 이 분야로의 응용 연구가 활발해지고 있으며, DeepSeek의 노력도 이러한 흐름 속에 위치하고 있다.

DeepSeek-Prover-V2의 훈련에는 동사가 개발한 대규모 언어 모델 "DeepSeek-V3"가 활용되었다. DeepSeek-V3를 사용하여 학습용 데이터를 생성하는 방식을 취하고 있으며, 재귀적 증명 탐색(문제를 더 작은 부분으로 분해하면서 반복적으로 해를 찾는 방법)과 강화학습(시행착오를 통해 모델의 정확도를 높이는 방법)을 결합하여 모델을 개선하고 있다.

성능 평가로서 정리 증명 벤치마크 "MiniF2F"에서 최고 수준의 결과를 달성했다고 보고되었다. MiniF2F는 수학 올림피아드 수준의 문제 등을 포함하는 표준 평가 세트이며, 이 벤치마크에서의 높은 점수는 모델의 실용적 증명 능력을 보여주는 지표로 널리 참조된다.

이번 공개가 오픈소스 형식을 취한 점도 주목된다. 연구자와 개발자가 모델의 세부 사항을 확인·수정할 수 있기 때문에 학술 커뮤니티에서의 활용과 추적 연구가 진행하기 쉬워질 것으로 보인다. DeepSeek은 지금까지도 여러 오픈 모델을 공개해 왔으며, 투명성이 높은 개발 자세를 취하는 기업으로 알려져 있다.

인공지능에 의한 수학 증명 자동화는 순수 수학 연구 지원에 그치지 않으며, 소프트웨어의 정확성 검증이나 암호 이론의 검증 등 실용적 응용의 가능성을 가진 분야이기도 하다. DeepSeek-Prover-V2가 그 능력을 얼마나 확장할 수 있을지, 향후 연구 커뮤니티에서의 검증이 하나의 관전 포인트가 될 것이다.

향후에는 MiniF2F 이외의 더 높은 난이도의 벤치마크에서의 평가나, 실제의 미해결 문제에 대한 적용 가능성이 연구상의 초점이 될 것으로 생각된다. 오픈소스로의 공개에 따라 외부로부터의 검증·개량도 더해짐으로써 이 분야의 연구가 가속화될 것이라는 견해가 가능하다.