DeepSeek 오픈 소스 대규모 수학적 모델, 고등학교 및 대학교 정리 증명을 위한 새로운 SOTA-일체 포함-php.cn

DeepSeek-Prover-V1.5는 강화 학습과 몬테카를로 트리 검색을 결합하여 증명 생성의 효율성과 정확성을 크게 향상시킵니다.

AI 기술의 발전과 수학적 발견은 이전과는 전혀 다른 방식으로 얽혀 있습니다.

얼마 전, 유명한 수학자 테레사 타오(Teresa Tao)가 옥스퍼드 수학 공개 강연에서 "과학과 수학에서 AI의 잠재력"이라는 주제로 연설을 했습니다. 그는 AI를 수학에 통합하면 (오류가 발생하기 쉬운) 인간 증명보다 형식적 증명을 더 빠르게 작성할 수 있다고 언급했습니다. 이는 중요한 전환점이 될 것입니다. 즉, 형식 증명의 사용이 기존 증명을 검증하는 데 국한되지 않고 새로운 수학적 지식을 창출하는 데에도 사용될 것임을 의미합니다. 이는 인간과 AI 수학자 간의 광범위한 협력을 통해 달성될 것입니다. 우리는 곧 "큰 수학" 시대를 맞이할 것입니다!

DeepSeek 오픈 소스 대규모 수학적 모델, 고등학교 및 대학교 정리 증명을 위한 새로운 SOTA

테렌스 타오(Terence Tao)가 말했듯이 AI를 형식적 정리 증명에 적용하는 것은 수학자들의 일상적인 작업이 되었습니다. 한편, AI 과학자들은 DeepSeek에서 최근 출시한 새로운 모델인 DeepSeek-Prover-V1.5와 같은 형식적 정리 증명에서 AI의 성능과 효율성을 향상시키기 위해 열심히 노력하고 있습니다.

DeepSeek-Prover-V1.5는 70억 개의 매개변수를 갖춘 오픈 소스 모델입니다. 강화 학습(증명 보조 피드백 기반 강화 학습, RLPAF)과 몬테카를로 트리 검색(특히 제안된 RMaxTS 변형)을 결합하여 증명 생성의 효율성과 정확성을 크게 향상시킵니다. DeepSeek-Prover-V1.5는 Lean 4의 공식 정리 증명에서 모든 오픈 소스 모델보다 성능이 뛰어납니다.

다음은 기술보고서의 내용입니다.

기술 보고서 개요

보고서 제목: DeepSeek-Prover-V1.5: 강화 학습 및 몬테카를로 트리 검색을 위한 증명 보조 피드백 활용
Re 포트 링크: https://arxiv.org/pdf/2408.08152
GitHub 링크: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

최근에는 대규모로 -규모 언어 모델 분야의 발전은 수학적 추론 및 정리 증명 분야의 인공 지능 개발을 크게 촉진했습니다. 그러나 언어 모델은 형식 정리 증명에서 여전히 심각한 문제에 직면해 있습니다. 예를 들어 Lean 및 Isabelle과 같은 시스템을 사용하는 증명에서는 검증 시스템의 형식 사양을 충족하기 위해 엄격한 파생이 필요합니다. GPT-4와 같은 고급 모델조차도 복잡한 형식 증명을 처리할 수 없습니다. 이는 형식 증명의 코딩 및 수학적 추론의 복잡성을 강조합니다. 효율적인 형식 정리 증명 모델을 위해서는 Lean Proof Assistant와 같은 형식 시스템의 구문과 의미를 이해해야 할 뿐만 아니라 추상적인 수학적 추론과 정확한 형식 표현을 결합해야 합니다.

정식 증명에서 언어 모델은 일반적으로 증명 단계 생성과 전체 증명 생성이라는 두 가지 전략을 채택합니다.

증명 단계는 각 전략을 예측 및 검증하고, 공식 검증기를 사용하여 현재 전략 상태에 대한 업데이트된 정보를 얻고, 종종 트리 검색 기술을 결합하여 효과적인 증명을 구축함으로써 생성됩니다. 전체 증명 생성은 정리문을 기반으로 한 번에 전체 증명 코드를 생성하여 증명 모델과 형식 정리 검증기 간의 조정에 필요한 통신량을 줄여 계산적으로 더 효율적입니다.

DeepSeek-Prover-V1이 완전한 증명 생성을 통해 Lean 4에서 SOTA 결과를 달성했지만 이 접근 방식에는 고유한 과제도 있습니다. 중간 정책 상태 정보 없이 장기적인 순서 예측이 필요하며, 미래 정책은 이러한 숨겨진 결과에 의존합니다. Lean의 전략 패턴에서는 증명의 상태를 변경하는 일련의 전략을 통해 증명이 구성됩니다. 이러한 순차적성으로 인해 오류가 누적될 수 있으며, 작은 오류로 인해 증명이 올바른 경로에서 벗어날 수 있습니다. 특히, 자기회귀 모델은 성장 증거를 생성할 때 중간 정책 상태에 대해 잘못된 인식을 가질 수 있습니다.

완전한 증명 생성의 단순성과 계산 효율성을 희생하지 않고 중간 정책 상태를 원활하게 통합하기 위해 연구원들은 DeepSeek-Prover-V1.5에서 통합 접근 방식을 개발했습니다.이 접근 방식은 잘라내기 및 재개 메커니즘을 통해 증명 단계 생성과 완전한 증명 생성의 장점을 결합합니다.

프로세스는 표준 완전 증명 생성으로 시작됩니다. 여기서 언어 모델은 정리 문 접두사를 기반으로 증명 코드를 완성한 다음 Lean 증명자가 이를 확인합니다. 올바른 것으로 입증되면 프로세스가 종료됩니다. 오류가 발견되면 첫 번째 오류 메시지에서 코드가 잘리고 후속 코드가 삭제됩니다. 그런 다음 성공적으로 생성된 증명 코드를 힌트로 사용하여 다음 증명 세그먼트를 생성합니다.

새로 완성된 모델 부분의 정확도를 높이기 위해 연구원은 프롬프트 마지막에 Lean 4 증명자의 최신 상태를 주석으로 추가했습니다. 이 접근 방식은 마지막으로 성공적으로 적용된 전략에서 다시 시작하는 것으로 제한되지 않는다는 점은 주목할 가치가 있습니다. 연구진은 잘림 및 다시 시작 메커니즘을 MCTS(Monte Carlo Tree Search)에 통합했으며, 트리 검색 전략은 잘림 지점을 정렬합니다. 또한, 증명 탐색에서 보상 희소성 문제를 해결하기 위해 새로운 보상 없는 탐색 알고리즘을 제안했습니다. 이는 정책 상태 공간을 광범위하게 탐색할 수 있는 본질적인 원동력, 즉 호기심을 트리 검색 에이전트에 부여합니다. 이러한 알고리즘 모듈은 전체 증명 생성 모델을 증명 보조자의 피드백을 효과적으로 활용하여 다양한 솔루션을 생성할 수 있는 유연하고 대화형 정리 증명 도구로 확장합니다.

핵심 기여

연구원들은 언어 모델을 기반으로 한 형식적인 수학적 증명 도구를 개발하기 위한 포괄적인 프레임워크를 제안했습니다. 그들은 대규모 수학적 사전 훈련, 형식적 사전 훈련, 구축 및 향상과 같은 몇 가지 핵심 구성 요소를 통합했습니다. 수학 말뭉치, 증명 보조 피드백 기반 온라인 강화 학습, 정리 증명의 장기 계획을 위한 트리 검색 방법론. 사전 훈련된 모델, 감독된 미세 조정 모델, 강화 학습 모델 및 몬테카를로 트리 검색 알고리즘에 대한 코드는 추가 연구 및 적용을 위해 공개적으로 제공됩니다.

1. 사전 훈련

연구원들은 Lean 및 코드 데이터에 중점을 두고 고품질 수학과 코드 데이터에 대한 추가 사전 훈련을 통해 형식 정리 증명 및 수학적 추론에서 기본 모델의 기능을 향상시켰습니다. Isabelle Metamath 및 Metamath와 같은 형식 언어는 증명 보조 도구로 널리 사용됩니다.

2. 감독된 미세 조정

연구원들은 두 가지 데이터 증대 기술을 구현하여 Lean 4 코드 완성 데이터 세트를 개선했습니다. 먼저 그들은 DeepSeek-Coder V2 236B를 사용하여 Lean 4 코드와 함께 CoT(생각의 사슬) 주석에 주석을 달고 공식 정리 증명을 자연어 추론과 일치시켰습니다. 둘째, Lean 4 증명 코드에 중간 정책 상태 정보를 삽입하여 모델이 컴파일러 피드백을 보다 효율적으로 활용할 수 있도록 합니다. 그런 다음 이 데이터 세트를 사용하여 사전 훈련된 모델을 미세 조정했습니다.

3. 강화 학습

연구원들은 GRPO 알고리즘을 사용하여 지도 미세 조정 모델에 대해 RLPAF(증명 보조 피드백을 기반으로 한 강화 학습)를 수행했습니다. Lean Prover의 검증 결과는 보상 감독 역할을 하여 검증 시스템의 공식 사양과 모델의 일관성을 향상시킵니다.

4. 몬테카를로 트리 검색

연구원들은 새로운 추상화와 이에 대응하는 검색 알고리즘을 도입하여 정형 정리 증명의 트리 검색 방법을 발전시켰습니다. 잘림 및 다시 시작 메커니즘은 트리 검색 프로세스를 완전한 증명 생성 프레임워크에 원활하게 통합하는 상태-작업 추상화 역할을 합니다. 그들은 증명 검색 문제에서 희소 보상의 탐색 문제를 해결하기 위해 RMax 전략을 활용하는 혁신적인 몬테카를로 트리 검색 알고리즘인 RMaxTS를 제시합니다. 본질적인 보상을 할당함으로써 이 알고리즘은 증명 에이전트가 다양한 계획 경로를 생성하도록 장려하여 증명 공간의 광범위한 탐색을 촉진합니다.

평가 및 지표

1. 고등학교 수준 miniF2F 데이터 세트

싱글 패스 방식 전체 증명 생성 설정에서 DeepSeek-Prover-V1.5 테스트 세트 miniF2F 합격률 60.2%를 달성했는데, 이는 DeepSeek-Prover-V1의 50.0%보다 10.2%포인트 높은 수치입니다. 트리 검색 기술과 결합하면 합격률이 더욱 향상되어 새로운 SOTA 63.5%에 도달합니다.

2. 학부 수준 ProofNet 데이터 세트

DeepSeek-Prover-V1.5는 ProofNet의 단일 채널 방식 완전 증명 생성 설정에서도 강력한 성능을 보여 검증 세트에서 100% 합격률을 기록했습니다. 테스트 세트에서는 21.6%, 23.7%입니다. 트리 검색 기술과 결합하면 이러한 결과가 더욱 향상되어 검증 세트에서 25.4%, 테스트 세트에서 25.3%의 새로운 SOTA에 도달합니다.

모델 훈련

수학적 언어를 통해 형식적 증명과 추론을 생성하는 언어 모델의 능력을 향상시키기 위해 연구진은 기본 모델을 추가로 사전 훈련하고 이 개선된 모델을 DeepSeek -ProverV1로 명명했습니다. 5-베이스.

그런 다음 기사에서는 DeepSeek-Prover-V1.5의 SFT(지도 미세 조정)와 관련된 방법과 프로세스에 대해 설명합니다. 특히 연구원들은 자세한 설명 주석을 추가하여 DeepSeekProver-V1 증명 데이터세트를 강화했습니다. 이 개선 사항은 자연어 설명과 Lean 4 코드 간의 일관성을 향상시켜 더 나은 공식적인 수학적 추론을 촉진하기 위한 것입니다. 또한 연구원들은 몬테카를로 트리 검색 프로세스에 사용되는 잘림 및 다시 시작 메커니즘을 지원하기 위해 중간 정책 상태 정보를 보조 예측 작업으로 통합하고 결과 모델을 DeepSeek-ProverV1.5-SFT라고 불렀습니다.

증명 보조 피드백 기반 강화 학습

DeepSeek-Prover-V1.5-SFT의 성능을 더욱 향상시키기 위해 연구에서는 강화 학습 단계를 도입하여 DeepSeek-Prover-V1을 구현했습니다. .5-RL 모델. 이 단계에서는 강화 학습(RL)을 활용하여 Lean 4 증명자의 검증 피드백을 기반으로 성능을 향상시킵니다. 다음은 이 RL 프로세스의 구체적인 세부정보입니다.

교육 팁. 강화 학습 단계에서 연구는 감독된 미세 조정 데이터 세트의 부분 정리 설명을 훈련 단서로 사용합니다. 필터링 후에도 약 4,500개의 고유한 정리 문이 유지되었습니다. 각 정리에는 CoT 및 비CoT 지침 힌트가 함께 제공되어 두 모드 모두에서 모델의 증명 생성 기능을 향상시킵니다.

보상. RL을 통해 LLM을 훈련할 때 훈련된 보상 모델은 피드백 신호를 제공하는 경우가 많습니다. 대조적으로, 형식 정리 증명은 증명 보조자가 생성된 증명을 엄격하게 검증함으로써 이점을 제공하므로 상당한 이점을 제공합니다. 구체적으로, 생성된 각 증명은 올바르게 검증되면 1의 보상을 받고 그렇지 않으면 0의 보상을 받습니다. 이 이진 보상 신호는 정확하지만 특히 감독되는 미세 조정 모델에 어려운 정리의 경우 희박합니다. 이러한 희소성을 완화하기 위해 위에서 설명한 대로 모델의 감독된 미세 조정을 위해 달성하기 어렵지만 달성 가능한 훈련 단서를 선택했습니다.

강화 학습 알고리즘. 본 연구에서는 본 논문의 RL 알고리즘으로 GRPO(Group Relative Policy Optimization)를 채택했는데, 이는 PPO에 비해 더 높은 효과성과 효율성을 보인다. 구체적으로 GRPO는 각 정리 힌트에 대한 후보 증명 세트를 추출하고 세트 내 출력의 상대적 보상을 기반으로 모델을 최적화합니다.

평가. 그림 3은 miniF2F 및 ProofNet 데이터 세트의 각 교육 단계에 대한 비교 분석을 제공합니다. CoT 모드는 대부분의 설정에서 지속적으로 비CoT 모드보다 성능이 뛰어납니다.

탐색 지향 몬테카를로 트리 검색

전체적인 증명 생성 설정에서 트리 검색 접근 방식을 구현하기 위해 이 연구에서는 사용자 정의된 상태 및 동작 공간을 정의하기 위한 증명 트리 추상화를 도입하고 절단을 활용합니다. 메커니즘을 다시 시작합니다. 연구자들은 먼저 불완전한 증명을 각 증명 단계에 해당하는 일련의 트리 노드로 분해한 다음 이러한 트리 노드에 저장된 부분 콘텐츠를 사용하여 증명 생성 프로세스를 계속합니다. 그림 4는 전체 증명 생성에서 증명 검색 트리를 구축하는 과정을 보여줍니다.

절단: 이 연구는 정책 수준에서 증명 검색 트리를 구축합니다. 여기서 각 트리 가장자리는 정책 상태의 단일 전환 단계를 나타냅니다. 먼저, 연구에서는 모델에서 생성된 전체 증명을 Lean 증명자에게 제출하고 이를 정책으로 구문 분석했습니다. 그런 다음 가장 빠른 검증 오류가 발생하면 증명이 잘려 모든 후속 전략 코드가 성공적으로 적용되어 필요한 정리에 대한 증명이 진행될 수 있습니다. 전략 코드는 여러 코드 조각으로 분할되며 각 코드 조각에는 전략 상태 전환을 나타내는 단일 트리 가장자리에 해당하는 유효한 전략 코드 및 관련 사고 체인 주석이 포함되어 있습니다. 이 추상화를 통해 각 정책 코드는 일련의 트리 노드로 변환되어 루트에서 특정 노드까지의 경로를 형성합니다.

다시 시작: Lean 4에서는 서로 다른 전략이 동일한 전략 상태로 이어질 수 있습니다. 이는 증명 트리의 각 노드가 동일한 결과를 달성할 수 있는 여러 전략 코드에 해당할 수 있음을 의미합니다. 이 문제를 해결하기 위해 연구원들은 각 노드에 이러한 동등한 정책 코드 세트를 저장합니다.트리 검색 에이전트는 노드를 확장할 때 언어 모델에 대한 힌트로 정책을 무작위로 선택합니다.

몬테카를로 트리 탐색의 내재적 보상

다음 글에서는 내재적 보상 중심 탐색 알고리즘인 RMax가 트리 탐색에 적용된 RMaxTS(Reward-free 탐색이 증명에 통합됨)를 소개합니다. 검색 문제.

MCTS에 RMax를 적용했습니다. 이 연구에서는 고전적인 탐색 메커니즘인 RMax를 사용하여 몬테카를로 트리 탐색의 본질적인 보상을 구축합니다. 증명이 완료될 때까지 외부 보상이 제공되지 않는 증명 검색의 맥락에서 이 알고리즘 프로세스는 에이전트의 탐색이 내재적 보상, 즉 설정 DeepSeek 오픈 소스 대규모 수학적 모델, 고등학교 및 대학교 정리 증명을 위한 새로운 SOTA

에 의해서만 구동되는 ZeroRMax와 유사합니다. 트리 확장 단계의 본질적인 보상은 새 노드가 검색 트리에 추가되는지 여부에 따라 달라집니다.

이 휴리스틱은 잠재적으로 중복 생성을 줄이고 샘플 효율성을 높일 수 있습니다.

실험 결과

이 섹션에서 연구원들은 두 벤치마크 miniF2F와 ProofNet을 사용하여 DeepSeek-Prover-V1.5의 정리 증명 능력을 평가합니다. 전자에는 고등학교 수준의 연습과 경쟁 문제가 포함되고, 후자에는 학부 수준의 정리가 포함됩니다.

일관성을 보장하기 위해 연구원들은 평가에서와 동일한 훈련 모델과 추론 구성을 사용하여 전체 증명 생성 및 몬테카를로 트리 탐색 방법의 결과를 보여주었습니다.

우선, 본 논문에서는 DeepSeek-Prover-V1.5와 일부 이전 SOTA 모델의 성능과 진행 상황을 중심으로 비교 분석을 소개합니다.

일반 모델

GPT-3.5 및 GPT-4는 OpenAI에서 개발한 고급 생성 AI 모델로, 코드 생성을 포함한 다양한 작업에서 효율성을 인정받은 것으로 유명합니다. 이러한 모델은 정리 증명을 위해 특별히 설계된 것은 아니지만 광범위한 매개변수 범위는 중요한 기능을 제공합니다.

COPRA는 공식 정리 증명에서 이러한 모델의 평가를 용이하게 하며 이러한 대규모 언어 모델을 활용하여 전술적 적용을 제안하는 상황별 학습 에이전트입니다.

또한 연구원들은 형식 정리 증명을 위한 기본 모델로 자주 사용되는 광범위한 일반 수학 말뭉치에 대해 훈련된 언어 모델 계열인 Llemma에 대해서도 논의합니다.

정식 수학을 위한 특수 모델

GPT-f는 정리 증명 작업을 위한 증명 단계 생성에 Transformer를 적용하려는 초기 시도로, 최선의 검색 모듈을 활용하여 구축합니다. 완전한 증명. 후속 개발에는 ReProver, LLMStep 및 Lean-STaR이 포함됩니다.

Hypertree Proof Search는 Lean을 사용한 공식 정리 증명에서 Monte Carlo 트리 검색의 적용을 탐구합니다. 같은 기간 InternLM2-Math와 InternLM2-StepProver도 우수한 성능을 보였습니다.

그런 다음 연구원들은 이 모델을 DeepSeek-Prover-V1.5와 비교했습니다.

miniF2F 결과

표 1은 miniF2F 테스트 데이터 세트에 대한 다양한 정리 증명 방법에 대한 비교 분석을 제공합니다.

단일 채널 완전 증명 생성 설정에서 DeepSeekProver-V1.5-RL은 60.2%에 도달하여 가장 높은 통과율을 보이며 이는 DeepSeek-Prover-V1의 50.0%보다 10.2% 포인트 더 높습니다. DeepSeek-Prover-V1.5-RL은 샘플링 예산을 128회 시도로 제한하고 문제의 51.6%를 증명하여 다른 전체 증명 생성 방법보다 훨씬 뛰어난 성능을 발휘하며 주요 트리 검색 방법과 동등합니다. 트리 탐색 방법 부문에서는 DeepSeek-Prover-V1.5-RL + RMaxTS가 62.7%의 합격률로 선두를 달리며 새로운 SOTA 수준을 확립하며 기존 방법과의 격차를 넓혔다.

DeepSeek-Prover-V1.5-RL은 54.9%의 합격률을 달성하기 위해 3200개의 완전한 증명 샘플만 필요하며 이는 64번의 실행이 필요했던 InternLM2-StepProver의 이전 SOTA 수준을 초과합니다. 54.5%의 합격률을 달성하려면 3200번의 트리 검색이 필요합니다.

ProofNet 결과

표 2에는 ProofNet 데이터 세트에 대한 다양한 정리 증명 방법의 비교 분석이 나와 있습니다. 전체 ProofNet 데이터 세트에서 DeepSeek-Prover-V1.5-RL의 통과율은 각각 22.6%와 25.3%에 도달했습니다.이는 기존 SOTA 방식인 ReProver(13.8%)와 InternLM2-StepProver(18.1%)를 능가하는 결과입니다. 완전한 증명 생성 시도 횟수가 3200으로 제한되는 경우 DeepSeek-Prover-V1.5는 정리의 21.7%를 증명하며 이는 이전 최첨단 InternLM2-StepProver에 비해 3.6% 향상된 수치입니다.

대규모 샘플링에서 훈련 전략의 효과 재검토

연구원들은 단일 채널 완전 증명 생성에 초점을 맞춰 대규모 샘플링 환경에서 여러 훈련 모듈의 효과를 재검토했습니다. 및 몬테 캐롤 트리 검색.

표 3은 miniF2F 테스트 데이터 세트에서 두 세대 모드인 비CoT와 CoT의 성능을 비교하여 샘플 예산이 증가함에 따라 비CoT 모드에 비해 CoT의 이점이 증폭된다는 것을 보여줍니다.

Ablation Experiment

Ablation 실험에서 연구진은 RMaxTS의 알고리즘 설계를 테스트했습니다. 실험은 miniF2F 테스트 데이터 세트에서 DeepSeek-Prover-V1.5-RL을 사용하여 CoT 모드에서 수행됩니다. 그림 5에서 볼 수 있듯이 왼쪽은 6400개의 생성된 샘플 내에서 Pass@K 정확도 곡선을 보여주고, 오른쪽은 더 큰 샘플 크기의 결과를 보여줍니다.