A Deepseek AI anunciou o lançamento do Deepseek-Prover-V2, um modelo de linguagem de grande fonte de código aberto projetado especificamente para o teorema formal que prova no ambiente Lean 4. Esta iteração mais recente se baseia em trabalhos anteriores, introduzindo um pipeline inovador e recursivo de teorema, aproveitando o poder do Deepseek-V3 para gerar seus próprios dados de inicialização de alta qualidade. O modelo resultante atinge o desempenho de ponta no teorema neural provando e é acompanhado pela introdução do Proverbench, uma nova referência para avaliar os recursos de raciocínio matemático.
Uma inovação importante do DeepSeek-Prover-V2 reside em seu procedimento exclusivo de treinamento a frio. Esse processo começa solicitando o poderoso modelo Deepseek-V3 a decompor teoremas matemáticos complexos em uma série de subgoals mais gerenciáveis. Simultaneamente, o DeepSeek-V3 formaliza essas etapas de prova de alto nível no Lean 4, criando efetivamente uma sequência estruturada de subproblemas.
Para lidar com a pesquisa de prova intensiva computacional para cada subgoal, os pesquisadores empregaram um modelo de parâmetros 7B menor. Uma vez que todas as etapas decompostas de um problema desafiador são comprovadas com sucesso, a prova formal passo a passo completa é combinada com o correspondente raciocínio da cadeia de pensamento do Deepseek-V3. Essa abordagem engenhosa permite que o modelo aprenda com um conjunto de dados sintetizado que integra o raciocínio matemático informal e de alto nível e provas formais rigorosas, fornecendo um forte começo de frio para o aprendizado de reforço subsequente.
Com base nos dados sintéticos de partida fria, a equipe Deepseek selecionou uma seleção de problemas desafiadores que o modelo do 7B Prover não conseguiu resolver o de ponta a ponta, mas para o qual todos os subgnos foram abordados com sucesso. Ao combinar as provas formais desses subgesia, uma prova completa para o problema original é construída. Essa prova formal está então ligada à cadeia de pensamento do Deepseek-V3, descrevendo a decomposição do lema, criando um exemplo de treinamento unificado de raciocínio informal seguido de formalização.
O modelo Prover é então ajustado nesses dados sintéticos, seguido por um estágio de aprendizado de reforço. Este estágio utiliza feedback binário correto ou incorreto como o sinal de recompensa, refinando ainda mais a capacidade do modelo de preencher a lacuna entre a intuição matemática informal e a construção precisa de provas formais.
O culminar desse processo de treinamento inovador é Deepseek-Prover-V2-671B, um modelo com 671 bilhões de parâmetros. Esse modelo alcançou resultados notáveis, demonstrando desempenho de ponta no teorema neural. Alcançou um impressionante 88,9% de taxa de aprovação no teste minif2f e resolvido com sucesso 49 dos 658 problemas de Putnambench. As provas geradas pelo DeepSeek-Prover-V2 para o conjunto de dados MINIF2F estão disponíveis ao público para download, permitindo um escrutínio e análise adicionais.
Além do lançamento do modelo, a Deepseek AI introduziu Proverbenchum novo conjunto de dados de benchmark compreendendo 325 problemas. Esta referência foi projetada para oferecer uma avaliação mais abrangente dos recursos de raciocínio matemático em diferentes níveis de dificuldade.
Proverbench inclui 15 Problemas formalizados a partir de competições recentes de Aime (American Invitational Mathematics Examination) (Aime 24 e 25)proporcionando desafios autênticos no nível da competição do ensino médio. O restante 310 problemas são extraídos de exemplos de livros didáticos e tutoriais educacionais com curadoriaoferecendo uma coleção diversificada e pedagogicamente sólida de problemas matemáticos formalizados que abrangem várias áreas:
O Proverbench visa facilitar uma avaliação mais completa dos provadores do teorema neural em problemas desafiadores de concorrência e matemática fundamental de graduação.
O Deepseek AI está lançando Deepseek-Prover-V2 em dois tamanhos de modelo para atender a diferentes recursos computacionais: um modelo de parâmetros 7B e o modelo maior de parâmetros 671B. Deepseek-Prover-V2-671b é construído com base na base robusta da Base Deepseek-V3. O menor Deepseek-Prover-V2-7b é construído com base na base do Deepseek-Prover-V1.5 e apresenta um comprimento de contexto estendido de até 32k tokens, permitindo que ele processe sequências de raciocínio mais longas e mais complexas.
A liberação do Deepseek-Prover-V2 e a introdução do Proverbench marcam um passo significativo no campo do teorema neural. Ao alavancar um pipeline de busca de prova recursiva e introduzir um novo benchmark desafiador, a AI Deepseek está capacitando a comunidade a desenvolver e avaliar sistemas de IA mais sofisticados e capazes para matemática formal.
Link ： https: //huggingface.co/deepseek-ai/deepseek-prover-v2-671b