Durante o Primeiro de maio, o DeepSeek mais uma vez trouxe grandes novidades para o campo da IA - o lançamento do novo modelo DeepSeek-Prover-V2. Apesar dos recentes rumores que circulam na Web sobre o lançamento iminente do DeepSeek-R2, o DeepSeek foi em frente e lançou este poderoso modelo focado na prova de teoremas matemáticos, e continua a manter o seu habitual espírito de código aberto.

Dois modelos poderosos sincronizados com a fonte aberta

Desta vez, o DeepSeek abriu duas versões do modelo DeepSeek-Prover-V2.

• DeepSeek-Prover-V2-671B: Construído sobre o DeepSeek-V3-Base, com 671 mil milhões de parâmetros, é atualmente o rei do desempenho na prova de teoremas
• Procura Profunda-V2-7BDeepSeek-Prover-V1.5-Base, com 7 mil milhões de parâmetros, suportando comprimentos de contexto até 32K tokens

Ambos os modelos foram oficialmente lançados na Hugging Face:

• DeepSeek-Prover-V2-7B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
• DeepSeek-Prover-V2-671B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

O que é o DeepSeek-Prover-V2?

O DeepSeek-Prover-V2 é um modelo de linguagem grande de código aberto para a "linguagem de programação matemática de IA" Lean 4, com foco na prova formal de teoremas. Simplificando, ele pode transformar teoremas matemáticos abstratos em provas rigorosas verificáveis por computador, trazendo uma ferramenta revolucionária para a pesquisa matemática.

A sua melhor caraterística é a capacidade de combinar perfeitamente o raciocínio matemático não formal (ou seja, normalmente utilizado pelos seres humanos) com provas formais rigorosas, permitindo ao modelo pensar de forma tão flexível como um ser humano e argumentar de forma tão rigorosa como um computador, alcançando uma mistura integrada de raciocínio matemático.

Desempenho espantoso: bater muitos recordes

O DeepSeek-Prover-V2-671B mostra uma força sem precedentes em vários testes de prova de teoremas:

• Atingiu uma taxa de aprovação recorde de 88,9% no conjunto de testes MiniF2F
• Resolveu com êxito 49 das 658 perguntas do conjunto de dados PutnamBench
• Tem também um bom desempenho em problemas difíceis de concursos de matemática, como os AIME 24 e 25

Muitos internautas testaram o modelo e disseram que era ainda mais capaz de resolver problemas complexos de matemática do que modelos de topo como o o4-mini da OpenAI e o Grok-3 da XAI. Alguns estudantes que participaram nas Olimpíadas de Matemática exclamaram: "As Olimpíadas nunca foram tão fáceis!"

Inovação tecnológica: combinar a aprendizagem recursiva e a aprendizagem por reforço

No relatório técnico, a equipa DeepSeek revela a metodologia de formação principal do Prover-V2, que se baseia numa combinação inovadora de aprendizagem recursiva + reforço. O processo de treinamento do modelo é dividido em várias etapas principais:

1) Pesquisa recursiva de provas através da decomposição de objectivos secundários

O DeepSeek-Prover-V2 utiliza uma forma de pensar semelhante à de um matemático humano - decompondo teoremas complexos numa série de lemas mais pequenos para provar. O processo de implementação específico inclui:

• O DeepSeek-V3 começa por gerar esboços de provas em linguagem natural e formalizá-los como enunciados de teoremas em linguagem Lean
• Os objectivos parciais decompostos são então resolvidos recursivamente utilizando o modelo de prova 7B
• Finalmente, as provas destes objectivos secundários são combinadas para construir uma prova formal completa do problema complexo original

Esta abordagem não só melhora a eficiência da prova, como também alarga o leque de teoremas que o modelo pode tratar.

2. harmonizar o raciocínio não formal com as provas formais

A equipa do DeepSeek combinou inteligentemente o raciocínio de alto nível em linguagem natural com processos de prova exacta de baixo nível:

• Escolha os problemas que são particularmente difíceis de resolver e divida-os em objectivos mais pequenos
• Quando cada um dos mini-objectivos é provado, são combinados para formar uma prova rigorosa completa
• Adicione esta prova completa à "cadeia de pensamento" gerada pelo DeepSeek-V3, criando dados de formação que combinam o pensamento humano e a verificação da máquina.

Desta forma, a equipa recolheu centenas de dados de formação de alta qualidade, proporcionando uma base de aprendizagem sólida para o modelo.

3. aprendizagem reforçada para melhorar as capacidades de raciocínio

Após um ajuste inicial, a equipa introduziu o algoritmo de aprendizagem por reforço Group Relative Policy Optimization (GRPO):

• Amostragem de várias provas candidatas para cada pergunta e otimização da estratégia através de recompensas relativas
• Utilizar um mecanismo de recompensa binário: Lean atribui a pontuação 1 a uma verificação bem sucedida e 0 a um insucesso
• O bónus de consistência estrutural foi especificamente concebido para garantir que as provas geradas pelo modelo são consistentes com a ideia de decomposição da cadeia de pensamento

Este método de formação melhora consideravelmente a precisão do modelo na prova de teoremas complexos.

ProverBench: um novo conjunto de testes de referência em matemática

Para além do próprio modelo, o DeepSeek lançou o ProverBench - um conjunto de dados de referência com 325 perguntas:

• 15 perguntas sobre teoria dos números e álgebra dos últimos concursos de matemática, como o AIME 24 e 25
• 310 perguntas selecionadas a partir de exemplos de manuais e tutoriais, cobrindo uma vasta gama de níveis de dificuldade e domínios.

Este conjunto de dados destina-se a fornecer uma avaliação exaustiva dos modelos, tanto ao nível da competição no ensino secundário como ao nível da licenciatura em matemática, e a fornecer uma plataforma de teste mais sistemática para a investigação em IA matemática.

Ligação ProverBench:https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

Resultados experimentais e conclusões destacadas

No decurso do estudo, a equipa descobriu vários fenómenos interessantes:

Modelos CoT vs. modelos não-CoT

O DeepSeek-Prover-V2 suporta dois modos complementares de geração de provas:

• Modelo não-CoT (não-Chain of Thought) altamente eficienteGeração rápida de código Lean sem etapas de inferência intermédias
• Modelo de Cadeia de Pensamento (CoT) de alta precisãorepresentação sistemática do processo de raciocínio e construção gradual de provas logicamente claras

As experiências mostram uma vantagem significativa no desempenho do modelo CoT em relação ao modelo não-CoT no raciocínio matemático formal, confirmando a eficácia da pista da cadeia de pensamento no domínio da prova de teoremas.

Capacidades inesperadas dos modelos pequenos

Surpreendentemente, o DeepSeek-Prover-V2-7B teve um desempenho além das expectativas ao usar o modelo não-CoT no conjunto de dados PutnamBench. Ele até resolveu 13 questões que o modelo 671B não conseguiu resolver!

A análise revelou que o modelo 7B adquiriu uma técnica única - a utilização frequente de Cardinal.toNat e Cardinal.natCast_inj para problemas que envolvem bases finitas - que é rara no modelo 671B. Esta constatação sugere que a aprendizagem por reforço não só melhora o desempenho global, como também permite que o modelo desenvolva técnicas especializadas de resolução de problemas.

Guia de início rápido

Quer experimentar o DeepSeek-Prover-V2? Aqui está um exemplo simples que mostra como usar a biblioteca Transformers da Hugging Face para inferência de modelo:

from transformers import AutoModelForCausalLM, AutoTokenizer
importar torch

torch.manual_seed(30)
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # ou deepseek-ai/DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
importar Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topologia Rat
/-- Qual é a diferença positiva entre $120\%$ de 30 e $130\%$ de 20? Mostre que é 10.-/
Teorema mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
    lamenta
"""".strip()

prompt = """
Complete o seguinte código Lean 4.
 ``lean4
{}

perspectivas futuras

A equipa do DeepSeek afirma que o trabalho futuro se centrará na extensão desta estrutura a sistemas do tipo AlphaProof. O objetivo final é resolver puzzles matemáticos de nível IMO que representam a vanguarda do campo da prova automática de teoremas. Com o lançamento do DeepSeek-Prover-V2, podemos estar a assistir a uma grande mudança na forma como a matemática é estudada. Mais do que um mero avanço tecnológico, este modelo representa um novo paradigma para os humanos colaborarem com a IA na resolução de problemas complexos.

Entretanto, a expetativa pelo DeepSeek-R2 tornou-se mais forte. Como disse um internauta: "Bate nesta pequena baleia azul, quando é que o R2 vai ser lançado!

Se quiser utilizar a conta exclusiva paga oficial GPT Plus, Claude Pro, Grok Super, pode contactar a nossa equipa de profissionais (wx: abch891) se não souber como carregar a sua conta.