Mistral AI, da França, lança o modelo de código aberto de baixo custo Leanstral 1.5, com capacidade matemática em nível utilizável

De acordo com pt.wedoany.com-A empresa europeia de Inteligência Artificial Mistral AI anunciou, no dia 2 deste mês, o lançamento do modelo Leanstral 1.5, voltado para a linguagem de programação de prova formal matemática Lean 4. O modelo possui um total de 119B parâmetros, com 6B parâmetros ativados, e é de código aberto sob a licença Apache-2.0.

A Mistral AI afirma que o modelo Leanstral 1.5 alcançou uma taxa de conclusão de 100% nos conjuntos de validação e teste do benchmark matemático formal miniF2F; resolveu 587 dos 672 problemas Lean 4 do conjunto de problemas de competição matemática PutnamBench; e, para os benchmarks de álgebra abstrata da série FATE, obteve uma taxa de sucesso de 87% no FATE-H de nível de mestrado e 34% no FATE-X de nível de doutorado, ambos os melhores desempenhos. Esses testes indicam que a capacidade matemática do modelo já atingiu um nível utilizável.

A Mistral AI destacou a vantagem de custo do novo modelo: para os problemas do conjunto de dados PutnamBench, o custo médio de resolução do Leanstral 1.5 é de apenas 4 dólares, enquanto o Seed-Prover 1.5 requer mais de 300 dólares, e o Aleph Prover também precisa de 54 a 68 dólares.

Em aplicações de cenários reais, o Leanstral 1.5 sinalizou 47 propriedades violadas em 57 repositórios de código testados, das quais 11 apontaram para defeitos reais, incluindo 5 problemas que não haviam sido relatados anteriormente no GitHub.