A DeepSeek introduziu o DeepSeek-Prover-V2, um modelo de linguagem grande (LLM) open-source inovador e meticulosamente criado para o intrincado domínio da prova formal de teoremas dentro da estrutura Lean 4. Este novo modelo alavanca um pipeline recursivo de prova de teoremas, aproveitando o poder do modelo de fundação DeepSeek-V3 de última geração da DeepSeek. Lean 4, a mais recente iteração do provador de teoremas Lean, destaca-se como um assistente de prova interativo desenvolvido pela Microsoft Research. Esta sofisticada linguagem de programação funcional e sistema interativo de prova de teoremas capacita matemáticos e cientistas da computação a construir provas formais com verificação automática incomparável.
O projeto representa um passo monumental em direção à colmatação da lacuna entre o raciocínio matemático formal e informal. Ao capitalizar as capacidades inerentes dos LLMs de propósito geral, procura abordar eficazmente o domínio altamente estruturado da prova formal de teoremas. A equipe de pesquisa da DeepSeek postula que sua abordagem inovadora espelha os processos cognitivos empregados por matemáticos humanos ao construir provas, dissecando meticulosamente teoremas complexos em componentes mais gerenciáveis e compreensíveis.
Expandindo a Estrutura de Avaliação: Apresentando o ProverBench
Num movimento significativo para melhorar o rigor de sua pesquisa, a equipe DeepSeek expandiu significativamente sua estrutura de avaliação com a introdução do ProverBench, uma coleção de benchmark totalmente nova meticulousamente projetada especificamente para a avaliação abrangente das capacidades formais de prova de teoremas. Esta coleção abrangente serve como um recurso valioso para avaliar o desempenho dos LLMs no contexto da matemática formal.
"Além dos benchmarks convencionais, apresentamos orgulhosamente o ProverBench, uma coleção meticulosamente curada de 325 problemas formalizados, para enriquecer nosso processo de avaliação. Esta coleção inclui 15 problemas cuidadosamente selecionados provenientes diretamente das recentes competições do American Invitational Mathematics Examination (AIME), especificamente dos anos 24-25," os pesquisadores elaboraram.
A inclusão de problemas AIME no conjunto de dados ProverBench é particularmente notável, pois introduz um conjunto de problemas matemáticos desafiadores e bem estabelecidos, amplamente reconhecidos dentro da comunidade matemática. Isso fornece uma base padronizada e rigorosa para avaliar o desempenho do DeepSeek-Prover-V2 e compará-lo com outras abordagens.
Resultados Iniciais Promissores: Enfrentando Problemas AIME
Os resultados iniciais decorrentes de testes rigorosos nesses desafiadores problemas AIME revelaram um desempenho excepcionalmente promissor de seu modelo de prova de teoremas especializado meticulosamente projetado. A equipe DeepSeek relata orgulhosamente que o DeepSeek-Prover-V2 demonstrou sua proeza ao resolver com sucesso impressionantes 6 dos 15 problemas AIME apresentados a ele. Em comparação, o modelo DeepSeek-V3 de propósito geral, ao empregar técnicas de votação majoritária, conseguiu resolver com sucesso 8 problemas.
Essas descobertas destacam o potencial de LLMs especializados e de propósito geral para lidar com problemas matemáticos complexos. Embora o modelo de propósito geral tenha exibido uma taxa de sucesso ligeiramente maior neste benchmark em particular, o modelo especializado de prova de teoremas demonstrou sua proficiência no raciocínio matemático formal.
Imitando a Construção Humana de Provas: Uma Abordagem Chain-of-Thought
"Dadas as bem documentadas dificuldades que os modelos de propósito geral muitas vezes encontram ao tentar produzir provas Lean completas, instruímos estrategicamente o DeepSeek-V3 para gerar apenas um esboço de prova de alto nível, omitindo deliberadamente os detalhes intrincados. A resultante cadeia de pensamento culmina em um teorema Lean composto por uma sequência de declarações have, cada uma meticulosamente concluída com um espaço reservado sorry, indicando efetivamente uma submeta que precisa ser resolvida. Esta abordagem inovadora espelha elegantemente o estilo humano de construção de provas, em que um teorema complexo é incrementalmente reduzido a uma sequência de lemas mais gerenciáveis," a equipe DeepSeek elaborou.
Esta abordagem inovadora de gerar esboços de prova de alto nível alinha-se com a forma como os matemáticos muitas vezes abordam provas complexas. Ao focar na estrutura geral e nos passos principais, o modelo pode efetivamente guiar o subsequente refinamento e conclusão da prova.
Uma Estratégia Metódica: Abordando Cada Componente da Prova Individualmente
O sistema então emprega meticulosamente uma estratégia metódica e estruturada para abordar cada componente individual da prova. Esta abordagem sistemática garante que cada aspecto da prova seja cuidadosamente considerado e abordado de forma lógica e coerente. O sistema cria uma abordagem altamente estruturada para a prova de teoremas, construindo sobre resultados previamente estabelecidos para garantir uma base sólida para cada passo subsequente.
"Aproveitando as submetas geradas pelo DeepSeek-V3, adotamos uma estratégia de resolução recursiva para resolver sistematicamente cada passo de prova intermediário. Extraímos expressões de submetas de declarações have para substituí-las pelas metas originais nos problemas fornecidos e então incorporamos as submetas precedentes como premissas. Esta construção permite que as submetas subsequentes sejam resolvidas usando os resultados intermediários de passos anteriores, promovendo assim uma estrutura de dependência mais localizada e facilitando o desenvolvimento de lemas mais simples," os pesquisadores detalharam.
A estratégia de resolução recursiva é um aspecto fundamental da capacidade do sistema de lidar com provas complexas. Ao decompor o problema em submetas menores e mais gerenciáveis, o sistema pode efetivamente aplicar suas capacidades de raciocínio a cada componente individual.
Otimizando Recursos Computacionais: Um Modelo Especializado de 7B Parâmetros
Para otimizar efetivamente os recursos computacionais e garantir um processamento eficiente, o sistema emprega estrategicamente um modelo menor e altamente especializado de 7B parâmetros para processar os lemas decompostos. Esta abordagem é crucial para gerenciar efetivamente as demandas computacionais associadas a buscas extensivas de provas, garantindo que o sistema possa operar eficientemente sem ser dominado pela complexidade do espaço de busca. A abordagem culmina, em última análise, em uma prova completa derivada automaticamente quando todos os passos decompostos são resolvidos com sucesso.
"A estrutura algorítmica opera em dois estágios distintos, aproveitando dois modelos complementares: DeepSeek-V3 para decomposição de lemas e um modelo de provador de 7B para completar os detalhes formais correspondentes da prova," os pesquisadores descreveram.
Esta abordagem em dois estágios permite que o sistema aproveite os pontos fortes tanto de um grande modelo de propósito geral quanto de um modelo especializado menor. O grande modelo é usado para gerar esboços de prova de alto nível, enquanto o modelo menor é usado para preencher os detalhes e completar a prova formal.
Sintetizando Dados de Raciocínio Formal: Um Caminho Natural
Esta arquitetura meticulosamente projetada estabelece efetivamente um caminho natural e intuitivo para sintetizar dados de raciocínio formal, fundindo perfeitamente o raciocínio matemático de alto nível com os requisitos rigorosos e estritos da verificação formal. Esta integração é essencial para garantir a confiabilidade e credibilidade dos resultados do sistema.
"Curamos um subconjunto de problemas desafiadores que permanecem não resolvidos pelo modelo de provador de 7B de forma completa, mas para os quais todas as submetas decompostas foram resolvidas com sucesso. Ao compor as provas de todas as submetas, construímos uma prova completa-formal para o problema original," os pesquisadores explicaram.
Esta abordagem permite que o sistema aprenda com seus erros e melhore sua capacidade de resolver problemas complexos. Ao identificar as submetas específicas que estão causando dificuldades, o sistema pode focar seus esforços em melhorar seu desempenho nessas áreas.
Preocupações e Desafios: Detalhes da Implementação Sob Escrutínio
Apesar das inegáveis conquistas técnicas demonstradas pelo DeepSeek-Prover-V2, alguns especialistas na área levantaram preocupações pertinentes em relação a certos detalhes de implementação. Elliot Glazer, um respeitado matemático líder na Epoch AI, apontou potenciais problemas que justificam uma investigação mais aprofundada.
Algumas preocupações sobre o artigo DeepSeek-Prover-V2. Exemplos potencialmente mal formalizados, e a discussão no Lean zulip sugere que as provas do PutnamBench são um absurdo e usam um sorry implícito (possivelmente escondido na tática apply?) não relatado em seu read-eval-print-loop.
Essas preocupações destacam vividamente os desafios contínuos inerentes ao espaço da verificação formal, onde mesmo os detalhes de implementação mais minuciosos e aparentemente insignificantes podem exercer um impacto desproporcionalmente grande na validade e confiabilidade geral dos resultados. O processo de verificação formal exige atenção inabalável aos detalhes e adesão meticulosa aos padrões estabelecidos.
O potencial para exemplos mal formalizados e a possibilidade de táticas "sorry" ocultas nas provas do PutnamBench levantam questões importantes sobre o rigor e a integridade do processo de verificação. Essas preocupações ressaltam a necessidade de escrutínio contínuo e verificação independente dos resultados.
Disponibilidade e Recursos: Democratizando o Acesso à Prova Formal de Teoremas
A DeepSeek disponibilizou seu Prover-V2 em dois tamanhos de modelo distintos, atendendo a uma gama diversificada de recursos computacionais e objetivos de pesquisa. A primeira versão é um modelo de 7B parâmetros construído sobre seu Prover-V1.5-Base anterior, apresentando um comprimento de contexto estendido de até 32K tokens. A segunda versão é um modelo significativamente maior de 671B parâmetros treinado no DeepSeek-V3-Base. Ambos os modelos estão agora prontamente acessíveis no HuggingFace, uma plataforma líder para compartilhar e colaborar em modelos de aprendizado de máquina.
Além dos próprios modelos, a DeepSeek também disponibilizou no HuggingFace o conjunto de dados ProverBench completo, contendo 325 problemas meticulosamente formalizados para fins de avaliação. Este conjunto de dados abrangente fornece aos pesquisadores e desenvolvedores um recurso valioso para avaliar o desempenho de seus modelos e compará-los com o DeepSeek-Prover-V2.
Ao tornar esses recursos disponíveis gratuitamente, a DeepSeek está democratizando o acesso à tecnologia de prova formal de teoremas e fomentando a colaboração dentro da comunidade de pesquisa. Esta abordagem open-source provavelmente acelerará o progresso no campo e levará a novos avanços em raciocínio e verificação automatizados.
Este lançamento capacita pesquisadores e desenvolvedores com os recursos necessários para investigar as capacidades e limitações desta tecnologia. Ao fornecer acesso aberto aos modelos e ao conjunto de dados ProverBench, a DeepSeek incentiva uma maior exploração e esforços colaborativos para abordar as preocupações levantadas por especialistas na área. Esta abordagem colaborativa detém a chave para desvendar as complexidades da prova formal de teoremas e solidificar a confiabilidade desses avanços inovadores.