Mistral Lança Leanstral 1.5 para Provas Formais, Reduz Custo para ~$4 por Problema
De acordo com a OneMillionAI, a Mistral AI lançou recentemente o Leanstral 1.5, um modelo de demonstração formal para o Lean 4 com 119 mil milhões de parâmetros totais e 65 mil milhões de parâmetros ativos. O modelo é lançado sob a licença Apache-2.0 com acesso gratuito à API. No PutnamBench, o Leanstral 1.5 alcança um custo médio de aproximadamente 4 dólares por problema para resolver, significativamente mais baixo do que sistemas anteriores que custavam dezenas a centenas de dólares por proble
GateNews·07-04 02:53
