DeepSeek-Prover-V2: 공식 수학적 추론과 비공식적 추론 간의 간격을 메우다

DeepSeek-R1은 비공식적 추론에서 AI의 능력을 크게 향상시켰지만, 공식 수학적 추론은 여전히 AI에게 도전적인 과제로 남아있다. 이는 검증 가능한 수학적 증명을 생성하기 위해 깊은 개념적 이해와 정교한 논리적 논증을 구성하는 능력이 모두 필요하기 때문이다. 최근에 DeepSeek-AI의 연구자들은 DeepSeek-Prover-V2를 소개했는데, 이는 수학적 직관을 엄격한 증거로 변환할 수 있는 오픈 소스 AI 모델이다. 이 기사는 DeepSeek-Prover-V2의 세부 사항과 미래 과학적 발견에 대한 잠재적인 영향을 살펴본다.

공식 수학적 추론의 도전

수학자들은 종종 직관, 휴리스틱, 고수준 추론을 사용하여 문제를 해결한다. 이러한 접근 방식은 명백한 단계나 근사치를 생략할 수 있게 해준다. 그러나 공식 정리 증명은 다른 접근 방식이 필요하다. 완전한 정밀성이 필요하며, 모든 단계가 명시적으로 표시되고 논리적으로 정당화되어야 하며, 모호성이 없어야 한다.

최근의 대규모 언어 모델(Large Language Model, LLM)의 발전은 자연어 추론을 사용하여 복잡한 수학 문제를 해결할 수 있음을 보여주었다.尽管如此, LLM은 여전히 직관적 추론을 기계가 검증할 수 있는 공식 증거로 변환하는 데 어려움을 겪는다. 이는 비공식적 추론이 종종 생략된 단계와 약식 단계를 포함하기 때문이다.

DeepSeek-Prover-V2는 비공식적 추론과 공식적 추론의 강점을 결합하여 이러한 문제를 해결한다. 복잡한 문제를 더 작은, 관리 가능한 부분으로 나누면서도 공식적 검증에 필요한 정밀성을 유지한다. 이러한 접근 방식은 인간의 직관과 기계가 검증할 수 있는 증거 간의 간격을 메우는 것을 더 쉽게 만든다.

새로운 정리 증명 접근 방식

본질적으로, DeepSeek-Prover-V2는 비공식적 추론과 공식적 추론을 모두 포함하는 고유한 데이터 처리 파이프라인을 사용한다. 파이프라인은 일반적인 목적의 LLM인 DeepSeek-V3에서 시작하여 수학적 문제를 자연어로 분석하고, 이를 더 작은 단계로 나누고, 기계가 이해할 수 있는 공식 언어로 번역한다.

整个 문제를 한 번에 해결하려고 시도하는 대신, 시스템은 “하위 목표”라고 하는 중간 레마를 생성한다. 이러한 레마는 최종 증명을 향한 단계 stones로 작용한다. 이는 인간 수학자들이 어려운 문제를 해결하는 방식, 즉 한 번에 모든 것을 해결하려고 하지 않고 관리 가능한 청크로 나누어 해결하는 방식과 유사하다.

이 접근 방식이 특히 혁신적인 것은 어떻게 훈련 데이터를 생성하는지에 있다. 복잡한 문제의 모든 하위 목표가 성공적으로 해결되면, 시스템은 이러한 해결책을 완전한 공식 증거로 결합한다. 이 증거는 DeepSeek-V3의 원래 사고 연쇄 논증과 결합되어 모델 훈련을 위한 높은 품질의 “콜드 스타트” 훈련 데이터를 생성한다.

수학적 추론을 위한 강화 학습

초기 훈련 데이터에 대한 훈련 후, DeepSeek-Prover-V2는 추가적으로 강화 학습을 사용하여 자신의 능력을 향상시킨다. 모델은 자신의 해결책이 올바른지 여부에 대한 피드백을 받고, 이러한 피드백을 사용하여 어떤 접근 방식이 가장 효과적인지 학습한다.

여기서的一个 도전은 생성된 증거의 구조가 항상 사고 연쇄에 의해 제안된 레마 분해와 일치하지 않는다는 것이다. 이를 해결하기 위해, 연구자들은 일관성 보상을 훈련 단계에 포함하여 구조적 불일치를 줄이고 최종 증거에 모든 분해된 레마를 포함하도록 강제한다. 이러한 일관성 접근 방식은 다단계 추론을 요구하는 복잡한 정리에서 특히 효과적이다.

실제 성능과 능력

DeepSeek-Prover-V2의 성능은 기존 벤치마크에서 그 능력을 보여준다. 모델은 MiniF2F-test 벤치마크에서 인상적인 결과를 달성하고, PutnamBench의 658개의 문제 중 49개를 성공적으로 해결한다. 후자는 윌리엄 로웰 푸트넘 수학 경시회의 문제를 수록한 것이다.

더욱 인상적인 것은, 모델이 최근 American Invitational Mathematics Examination (AIME) 경시회에서 선정된 15개의 문제 중 6개를 성공적으로 해결했다는 것이다. 또한, DeepSeek-Prover-V2와 비교하여 DeepSeek-V3는 다수결 투표를 사용하여 이들 문제 중 8개를 해결했다. 이는 LLM에서 공식적 수학적 추론과 비공식적 추론 간의 간격이 빠르게 좁혀지고 있음을 시사한다. 그러나, 모델의 성능은 여전히 조합론적 문제에서 개선의 여지가 있다. 이는 미래 연구에서 집중할 수 있는 분야이다.

ProverBench: 수학에서 AI를 위한 새로운 벤치마크

DeepSeek 연구자들은 또한 LLM의 수학적 문제 해결 능력을 평가하기 위한 새로운 벤치마크 데이터셋을 소개했다. 이 벤치마크, ProverBench는 325개의 공식화된 수학적 문제로 구성되어 있다. 이는 최근 AIME 경시회에서 선정된 15개의 문제와 함께, 교과서와 교육 튜토리얼의 문제를 포함한다. 이러한 문제는 수론, 대수, 미적분학, 실해석학 등 다양한 분야를 다룬다. AIME 문제의 도입은 특히 중요하다. 이는 모델이 단순히 지식 회수를 요구하는 문제가 아니라, 창의적인 문제 해결을 요구하는 문제에서 평가되기 때문이다.

오픈 소스 접근과 미래의 영향

DeepSeek-Prover-V2는 오픈 소스 형태로 제공되어 흥미로운 기회를 제공한다. Hugging Face와 같은 플랫폼에서 호스팅되며, 모델은 연구자, 교육자, 개발자 등 다양한 사용자에게 접근할 수 있다. 7억 파라미터 버전과 671억 파라미터 버전이 모두 제공되므로, 다양한 컴퓨팅 자원을 가진 사용자도 이를 활용할 수 있다. 이러한 오픈 소스 접근은 실험을鼓励하며, 개발자가 고급 수학적 문제 해결을 위한 AI 도구를 생성할 수 있도록 한다. 따라서, 이 모델은 수학 연구에서 혁신을 驅動하고, 연구자들이 복잡한 문제를 해결하고 새로운 통찰력을 얻을 수 있도록 할 잠재력을 가지고 있다.

AI와 수학적 연구에 대한 영향

DeepSeek-Prover-V2의 개발은 수학적 연구뿐만 아니라 AI에도重大한 영향을 미친다. 모델의 공식 증거 생성 능력은 수학자들이 어려운 정리를 해결하고, 증명 과정을 자동화하며, 심지어 새로운 추측을 제안하는 데 도움을 줄 수 있다. 또한, DeepSeek-Prover-V2를 생성하기 위한 기술은 다른 분야에서 논리적 추론을 사용하는 미래의 AI 모델 개발에 영향을 미칠 수 있다.

결론

DeepSeek-Prover-V2는 AI 주도 수학적 추론에서重大한 발전이다. 비공식적 추론과 공식적 추론을 결합하여 복잡한 문제를 해결하고 검증 가능한 증거를 생성한다. 벤치마크에서 보여준 성능은 수학자们을 지원하고, 증명 검증을 자동화하며, 심지어 새로운 발견을 驅動하는 잠재력을 보여준다. 오픈 소스 모델로, 다양한 사용자에게 접근할 수 있으며, AI와 수학에서 새로운 응용과 혁신의 가능성을 제공한다.