DeepSeek, Prover-V2 공개: 형식 수학 증명에 혁명을 일으키는 오픈 소스 LLM
DeepSeek는 Lean 4 프레임워크 내에서 복잡한 형식 정리 증명 영역을 위해 세심하게 제작된 획기적인 오픈 소스 대규모 언어 모델 (LLM)인 DeepSeek-Prover-V2를 소개했습니다. 이 새로운 모델은 DeepSeek의 최첨단 DeepSeek-V3 기반 모델의 힘을 활용하여 재귀적 정리 증명 파이프라인을 활용합니다. Lean 4는 Microsoft Research에서 개발한 대화형 증명 지원 도구인 Lean 정리 증명기의 최신 버전입니다. 이 정교한 함수형 프로그래밍 언어 및 대화형 정리 증명 시스템은 수학자와 컴퓨터 과학자가 비교할 수 없는 기계 검사 검증을 통해 형식 증명을 구성할 수 있도록 지원합니다.
이 프로젝트는 형식적 추론과 비형식적 수학적 추론 사이의 격차를 해소하는 데 있어 기념비적인 진전을 의미합니다. 범용 LLM의 고유한 기능을 활용함으로써 형식 정리 증명이라는 고도로 구조화된 영역을 효과적으로 다루려고 합니다. DeepSeek 연구팀은 자신들의 혁신적인 접근 방식이 인간 수학자가 증명을 구성할 때 사용하는 인지 과정을 반영하여 복잡한 정리를 더 관리하기 쉽고 이해하기 쉬운 구성 요소로 세심하게 분석한다고 주장합니다.
평가 프레임워크 확장: ProverBench 소개
DeepSeek 팀은 연구의 엄격함을 강화하기 위한 중요한 조치로 형식 정리 증명 기능을 포괄적으로 평가하기 위해 특별히 설계된 완전히 새로운 벤치마크 모음인 ProverBench를 도입하여 평가 프레임워크를 크게 확장했습니다. 이 포괄적인 모음은 형식 수학 컨텍스트에서 LLM의 성능을 평가하는 데 유용한 리소스 역할을 합니다.
"기존 벤치마크를 넘어 평가 프로세스를 풍성하게하기 위해 세심하게 선별된 325개의 공식화된 문제 모음인 ProverBench를 자랑스럽게 소개합니다. 이 모음에는 최근 미국 초청 수학 시험 (AIME) 대회, 특히 24-25년도에서 직접 가져온 신중하게 선택된 15개의 문제가 포함되어 있습니다."라고 연구원들은 자세히 설명했습니다.
ProverBench 데이터 세트에 AIME 문제가 포함된 것은 특히 주목할 만합니다. 수학 커뮤니티 내에서 널리 인정되는 도전적이고 잘 확립된 수학 문제 세트를 도입하기 때문입니다. 이는 DeepSeek-Prover-V2의 성능을 평가하고 다른 접근 방식과 비교하기 위한 표준화되고 엄격한 기반을 제공합니다.
유망한 초기 결과: AIME 문제 해결
이러한 어려운 AIME 문제에 대한 엄격한 테스트에서 비롯된 초기 결과는 세심하게 설계된 특수 정리 증명 모델에서 예외적으로 유망한 성능을 보여주었습니다. DeepSeek 팀은 DeepSeek-Prover-V2가 제시된 15개의 AIME 문제 중 6개를 성공적으로 해결하여 자신의 기량을 입증했다고 자랑스럽게 보고합니다. 반면, 범용 DeepSeek-V3 모델은 다수결 투표 기술을 사용하여 8개의 문제를 성공적으로 해결했습니다.
이러한 결과는 복잡한 수학 문제를 해결하는 데 있어 특수 LLM과 범용 LLM 모두의 잠재력을 강조합니다. 범용 모델이 이 특정 벤치마크에서 약간 더 높은 성공률을 보였지만, 특수 정리 증명 모델은 형식 수학적 추론 능력을 입증했습니다.
인간 증명 구성 모방: 연쇄 사고 접근 방식
"일반적인 모델이 완전한 Lean 증명을 생성하려고 시도할 때 종종 겪는 잘 문서화된 어려움을 감안할 때, 우리는 DeepSeek-V3에게 복잡한 세부 사항을 의도적으로 생략한 높은 수준의 증명 스케치만 생성하도록 전략적으로 지시했습니다. 결과적으로 발생하는 사고의 연쇄는 일련의 have 문으로 구성된 Lean 정리로 마무리되며, 각 문장은 해결해야 할 하위 목표를 효과적으로 나타내는 sorry 자리 표시자로 세심하게 결론지어집니다. 이 혁신적인 접근 방식은 복잡한 정리가 일련의 더 관리하기 쉬운 보조 정리로 점진적으로 축소되는 인간 스타일의 증명 구성을 우아하게 반영합니다."라고 DeepSeek 팀은 자세히 설명했습니다.
높은 수준의 증명 스케치를 생성하는 이 혁신적인 접근 방식은 수학자들이 복잡한 증명에 접근하는 방식과 일치합니다. 전체 구조와 주요 단계에 집중함으로써 모델은 증명의 후속 개선 및 완료를 효과적으로 안내할 수 있습니다.
체계적인 전략: 각 증명 구성 요소를 개별적으로 처리
그런 다음 시스템은 증명의 각 개별 구성 요소를 처리하기 위해 질서 정연하고 구조화된 전략을 세심하게 사용합니다. 이 체계적인 접근 방식을 통해 증명의 모든 측면을 신중하게 고려하고 논리적이고 일관된 방식으로 처리할 수 있습니다. 이 시스템은 이전에 설정된 결과를 기반으로 각 후속 단계에 대한 견고한 토대를 보장하여 정리 증명에 대한 고도로 구조화된 접근 방식을 만듭니다.
"DeepSeek-V3에서 생성된 하위 목표를 활용하여 재귀적 해결 전략을 채택하여 각 중간 증명 단계를 체계적으로 해결합니다. have 문에서 하위 목표 표현식을 추출하여 주어진 문제에서 원래 목표를 대체한 다음 이전 하위 목표를 전제로 통합합니다. 이 구성을 통해 중간 결과를 사용하여 후속 하위 목표를 해결할 수 있으므로 더 국소화된 종속성 구조를 촉진하고 더 간단한 보조 정리 개발을 용이하게 합니다."라고 연구자들은 자세히 설명했습니다.
재귀적 해결 전략은 시스템이 복잡한 증명을 처리할 수 있는 능력의 핵심 측면입니다. 문제를 더 작고 관리하기 쉬운 하위 목표로 분해함으로써 시스템은 각 개별 구성 요소에 추론 능력을 효과적으로 적용할 수 있습니다.
컴퓨팅 리소스 최적화: 특수 7B 매개변수 모델
컴퓨팅 리소스를 효과적으로 최적화하고 효율적인 처리를 보장하기 위해 시스템은 분해된 보조 정리를 처리하기 위해 더 작고 고도로 전문화된 7B 매개변수 모델을 전략적으로 사용합니다. 이 접근 방식은 광범위한 증명 검색과 관련된 컴퓨팅 요구 사항을 효과적으로 관리하는 데 중요하며, 시스템이 검색 공간의 복잡성에 압도되지 않고 효율적으로 작동할 수 있도록 보장합니다. 이 접근 방식은 모든 분해된 단계가 성공적으로 해결될 때 자동으로 파생된 완전한 증명으로 궁극적으로 마무리됩니다.
"알고리즘 프레임워크는 두 가지 보완적인 모델 즉, 보조 정리 분해를 위한 DeepSeek-V3와 해당 형식 증명 세부 정보를 완료하기 위한 7B 증명기 모델을 활용하여 두 개의 개별 단계로 작동합니다."라고 연구자들은 설명했습니다.
이 2단계 접근 방식을 통해 시스템은 대규모 범용 모델과 더 작은 특수 모델 모두의 강점을 활용할 수 있습니다. 대규모 모델은 높은 수준의 증명 스케치를 생성하는 데 사용되는 반면, 더 작은 모델은 세부 사항을 채우고 형식 증명을 완료하는 데 사용됩니다.
형식적 추론 데이터 합성: 자연스러운 경로
이 세심하게 설계된 아키텍처는 높은 수준의 수학적 추론과 형식 검증의 엄격하고 엄격한 요구 사항을 완벽하게 병합하여 형식적 추론 데이터를 합성하기 위한 자연스럽고 직관적인 경로를 효과적으로 설정합니다. 이 통합은 시스템 결과의 신뢰성과 신뢰성을 보장하는 데 필수적입니다.
"7B 증명기 모델에서 종단 간 방식으로 해결되지 않은 어려운 문제의 하위 집합을 선별하지만 분해된 모든 하위 목표가 성공적으로 해결된 문제가 있습니다. 모든 하위 목표에 대한 증명을 작성하여 원래 문제에 대한 완전한 형식 증거를 구성합니다."라고 연구자들은 설명했습니다.
이 접근 방식을 통해 시스템은 실수로부터 배우고 복잡한 문제를 해결하는 능력을 향상시킬 수 있습니다. 어려움을 야기하는 특정 하위 목표를 식별함으로써 시스템은 해당 영역에서 성능을 향상시키는 데 노력을 집중할 수 있습니다.
우려 사항 및 과제: 구현 세부 사항에 대한 조사
DeepSeek-Prover-V2가 입증한 부인할 수 없는 기술적 성과에도 불구하고 해당 분야의 일부 전문가들은 특정 구현 세부 사항에 대한 관련 우려를 제기했습니다. Epoch AI의 존경받는 수석 수학자인 Elliot Glazer는 추가 조사가 필요한 잠재적인 문제를 지적했습니다.
DeepSeek-Prover-V2 논문에 대한 몇 가지 우려 사항. 잠재적으로 잘못 공식화된 예제와 Lean zulip에 대한 논의는 PutnamBench 증명이 넌센스이며 읽기-평가-인쇄 루프에 보고되지 않은 apply? 전략에 암시적 sorry가 숨어 있을 수 있음을 시사합니다.
이러한 우려는 형식 검증 공간에 내재된 지속적인 과제를 생생하게 강조합니다. 여기서 가장 미세하고 사소해 보이는 구현 세부 사항조차도 결과의 전반적인 타당성과 신뢰성에 불균형적으로 큰 영향을 미칠 수 있습니다. 형식 검증 프로세스는 세부 사항에 대한 변함없는 주의와 확립된 표준의 세심한 준수를 요구합니다.
잘못 공식화된 예제의 가능성과 PutnamBench 증명에 숨겨진 "sorry" 전략의 가능성은 검증 프로세스의 엄격성과 완전성에 대한 중요한 질문을 제기합니다. 이러한 우려는 결과에 대한 지속적인 조사와 독립적인 검증의 필요성을 강조합니다.
가용성 및 리소스: 형식 정리 증명에 대한 접근성 민주화
DeepSeek는 다양한 컴퓨팅 리소스 및 연구 목표를 충족하기 위해 두 가지 개별 모델 크기로 Prover-V2를 제공했습니다. 첫 번째 버전은 이전 Prover-V1.5-Base를 기반으로 구축된 7B 매개변수 모델로, 최대 32K 토큰의 확장된 컨텍스트 길이를 제공합니다. 두 번째 버전은 DeepSeek-V3-Base에서 훈련된 훨씬 더 큰 671B 매개변수 모델입니다. 두 모델 모두 현재 기계 학습 모델을 공유하고 협업하기 위한 주요 플랫폼인 HuggingFace에서 쉽게 액세스할 수 있습니다.
모델 자체 외에도 DeepSeek는 평가 목적으로 325개의 세심하게 공식화된 문제를 포함하는 전체 ProverBench 데이터 세트를 HuggingFace에서 사용할 수 있도록 했습니다. 이 포괄적인 데이터 세트는 연구원과 개발자에게 모델 성능을 평가하고 DeepSeek-Prover-V2와 비교하기 위한 귀중한 리소스를 제공합니다.
DeepSeek는 이러한 리소스를 무료로 제공함으로써 형식 정리 증명 기술에 대한 접근성을 민주화하고 연구 커뮤니티 내에서 협업을 촉진하고 있습니다. 이 오픈 소스 접근 방식은 해당 분야의 진전을 가속화하고 자동화된 추론 및 검증에서 새로운 획기적인 발전을 이끌어낼 가능성이 높습니다.
이 릴리스는 연구원과 개발자가 이 기술의 기능과 한계를 탐구하는 데 필요한 리소스를 제공합니다. DeepSeek는 모델과 ProverBench 데이터 세트에 대한 공개 액세스를 제공함으로써 해당 분야의 전문가가 제기한 우려 사항을 해결하기 위한 추가 탐색과 협력을 장려합니다. 이 협력적인 접근 방식은 형식 정리 증명의 복잡성을 풀고 이러한 획기적인 발전의 신뢰성을 강화하는 데 핵심입니다.