A DeepSeek lançou um modelo especializado na área de demonstração de teoremas matemáticos chamado Prover-V2, com o objetivo de usar IA para provar automaticamente teoremas matemáticos no sistema de verificação formal Lean 4.
Por que esta direção é importante?
A demonstração de teoremas matemáticos é um campo de teste extremo para as capacidades da IA. Isso porque a matemática não aceita "quase certo" – uma prova ou está completamente correta, ou está errada. Não existe "prova 95% correta".
Sistemas de verificação formal (como o Lean 4) verificam cada etapa do raciocínio lógico da mesma forma que um compilador verifica a sintaxe. Se uma etapa estiver errada, toda a prova apresenta um erro. Este é o teste mais rigoroso para a capacidade de raciocínio lógico da IA.
Desempenho do Prover-V2
No benchmark miniF2F, o Prover-V2 alcançou resultados próximos ou iguais aos melhores resultados atuais. O método que ele utiliza é a decomposição de subobjetivos – dividir uma prova complexa em uma série de subobjetivos menores e resolvê-los um por um.
Isso é muito semelhante à forma de pensar dos matemáticos humanos: diante de um problema difícil, primeiro pensam "para provar A, preciso primeiro provar B e C, e para provar B, preciso primeiro confirmar D…"
Diferença dos modelos de raciocínio de uso geral
Modelos de uso geral (GPT, Claude, Gemini) realizam raciocínio matemático com base em Chain-of-Thought – essencialmente "raciocinar passo a passo em linguagem natural". Essa abordagem funciona bem para problemas simples, mas em provas complexas é fácil surgir uma falha lógica em alguma etapa.
O Prover-V2 segue o caminho formal, onde cada etapa é verificada pelo Lean 4. A vantagem é que não há "alucinações"; a desvantagem é que o escopo de aplicação é muito restrito – só funciona dentro de sistemas formais.
Significado
A demonstração de teoremas matemáticos é uma direção que parece muito nichada, mas tem um impacto profundo. Se a IA realmente conseguir provar de forma confiável teoremas complexos em sistemas formais, ela poderá ser aplicada em áreas como verificação de software, verificação de hardware, provas criptográficas e uma série de outros campos críticos.
O investimento da DeepSeek nesta direção mostra que eles não estão apenas competindo em benchmarks de modelos grandes de uso geral – mas também construindo seriamente ferramentas científicas fundamentais.
Fonte de referência: CocoLoop, artigo do DeepSeek Prover-V2