Leanstral 1.5: abundância de provas para todos

 (mistral.ai)
1 pontos por GN⁺ 4 시간 전 | 1 comentários | Compartilhar no WhatsApp
  • Em meio ao movimento para aproximar a verificação formal do trabalho real de desenvolvimento, a Mistral AI lançou o Leanstral 1.5, um modelo Apache-2.0 para Lean 4
  • O modelo ativa apenas 6B de um total de 119B parâmetros e, após pré-treinamento intermediário, ajuste fino supervisionado e aprendizado por reforço CISPO, aprende tanto a escrever provas quanto a trabalhar em repositórios de código
  • Registrou 100% no miniF2F, 587/672 no PutnamBench, 87% no FATE-H e 34% no FATE-X, demonstrando forte desempenho em benchmarks de provas matemáticas e em avaliações reais de engenharia de provas
  • Na verificação de código real, provou a complexidade de tempo O(log n) de árvores AVL e, por meio de um pipeline de Rust para Lean, encontrou 11 bugs reais em 57 repositórios
  • Os pesos e a API gratuita leanstral-1-5 foram disponibilizados, permitindo aplicação imediata em engenharia de provas prática, como prova de teoremas, depuração de provas e contribuições a repositórios

Lançamento do Leanstral 1.5 e características do modelo

  • Leanstral 1.5 é um modelo criado para realizar engenharia de provas em Lean 4
  • A licença é Apache-2.0, e o modelo tem escala de 119B parâmetros totais e 6B parâmetros ativos
  • Ele eleva o desempenho em verificação formal, podendo ser usado não só em benchmarks matemáticos, mas também na verificação de propriedades de código real
  • Saturou o miniF2F, resolveu 587 dos 672 problemas do PutnamBench e atingiu 87% no FATE-H e 34% no FATE-X

Treinamento em 3 etapas com feedback de provas

  • O treinamento é composto por três etapas: pré-treinamento intermediário, ajuste fino supervisionado e aprendizado por reforço baseado em CISPO
  • Duas modalidades de ambiente são usadas no aprendizado por reforço
    • Ambiente multirrodadas: o modelo recebe a proposição de um teorema, tenta prová-la ou refutá-la e revisa a prova repetidamente com base no feedback do compilador Lean
    • Quando a prova compila, há sucesso; caso contrário, o loop continua até resolver o problema ou esgotar o orçamento
    • Ambiente de agente de código: em um sistema de arquivos bruto, ele edita arquivos como um desenvolvedor, executa comandos bash e verifica em tempo real metas, erros e informações de tipos via Lean language server
  • O ambiente de agente de código lida com tarefas longas, como completar provas parciais dentro de repositórios, escrever lemas auxiliares e continuar o trabalho mesmo após várias compressões de contexto
  • A correção final é verificada no fork SafeVerify da Mistral, com base na lista de teoremas-alvo

Benchmarks de matemática e engenharia de provas

  • A avaliação usou miniF2F, PutnamBench, FATE-H/FATE-X e FLTEval
    • miniF2F é um benchmark de matemática formal que inclui desde problemas elementares até problemas de nível IMO
    • PutnamBench é composto por 672 problemas da Putnam Mathematical Competition
    • FATE-H e FATE-X são benchmarks de álgebra abstrata em nível de pós-graduação e doutorado, respectivamente
    • FLTEval avalia a dificuldade de engenharia de provas com base em pull requests reais do repositório do Fermat’s Last Theorem
  • No miniF2F, atingiu 100% tanto no conjunto de validação quanto no conjunto de teste
  • No PutnamBench e no FATE-H/X, foi comparado com Goedel-Architect, Seed-Prover 1.5 high e AxProverBase sem guias de prova em linguagem natural
  • Desempenho no FATE-H/X: {b:87,34}
  • O FATE-H atingiu 87% e o FATE-X, 34%, estabelecendo um novo melhor desempenho
  • No PutnamBench, resolveu 7 problemas a mais que o Seed-Prover 1.5 high, com custo de cerca de US$ 4 por problema
    • A configuração high do Seed-Prover usa um orçamento de 10 H20-days por problema, com custo estimado acima de US$ 300
    • Alguns provadores com posições mais altas recebem guias de prova em linguagem natural ou operam em outras condições, como o Aleph Prover, que custa US$ 54 a US$ 68 por problema

Escalabilidade com orçamento longo de inferência e FLTEval

  • No PutnamBench, o desempenho Pass@8 do Leanstral 1.5 sobe de forma suave e monotônica conforme o orçamento de tokens aumenta
  • Em um experimento que elevou o orçamento de tokens por tentativa de 25k para 4M, o número de problemas resolvidos aumentou assim
    • 50k tokens: 44 problemas
    • 200k tokens: 244 problemas
    • 1M tokens: 493 problemas
    • 4M tokens: 587 problemas
  • A capacidade de continuar inferindo, editando arquivos e corrigindo ao longo de milhões de tokens, sem interromper provas longas, leva a ganhos de desempenho
  • O FLTEval também foi lançado como totalmente open source
  • No FLTEval, o Leanstral 1.5 elevou o pass@1 de 21,9 para 28,9 e o pass@8 de 31,9 para 43,2
  • O pass@8 de 43,2 supera os 39,6 do Opus 4.6, com custo cerca de 7 vezes menor
  • Também supera modelos open source de 3 a 10 vezes maiores

Casos de verificação de código real

  • Prova de complexidade de tempo de árvore AVL

    • Árvores AVL são árvores binárias de busca auto-balanceadas que mantêm altura O(log n) por meio de rebalanceamento durante inserções e remoções
    • O Leanstral 1.5 verificou que inserções e remoções são O(log n) em uma implementação real
    • Essa tarefa exigiu indução estrutural refletindo a estrutura recursiva da árvore, tratamento de rastreamento de tempo baseado em mônadas e análise exaustiva de casos para os caminhos de rebalanceamento
    • A prova prosseguiu por mais de 2,7 milhões de tokens e 22 compressões de contexto
    • O Leanstral expandiu sistematicamente cada camada da mônada TimeM, expondo cálculos misturados ao fluxo de controle
    • Para inserção, estabeleceu um limite de 48 passos por unidade de altura, mais um termo quase constante, e conectou a altura ao tamanho da árvore por uma relação logarítmica

  • Encontrando bugs em código Rust

    • O experimento de detecção de bugs consiste em um pipeline no qual o Aeneas converte código Rust para Lean, e o Leanstral infere a intenção do usuário a partir do código para gerar propriedades de consistência
    • O Leanstral tenta provar cada propriedade 4 vezes e, se todas falharem, tenta provar sua negação mais 4 vezes
    • Em 57 repositórios, 47 propriedades violadas foram sinalizadas, das quais 11 apontavam para bugs reais
    • Entre os bugs reais, 5 ainda não haviam sido relatados no GitHub
    • Um caso foi encontrado na função de sinal de zigzag decoding da biblioteca datrs/varinteger
    • Quando a entrada é Std.U64.MAX, a expressão (value + 1) sofre overflow
    • No modo debug, ocorre crash; no modo release, ocorre corrupção silenciosa de dados
    • Esse edge case é um tipo de caso que testes comuns e fuzzing tendem a deixar passar

Distribuição e como usar

  • Os pesos foram publicados no Hugging Face
  • O endpoint gratuito da API está disponível no model card com o nome leanstral-1-5
  • O ambiente recomendado para uso é o Mistral Vibe
  • O processo inicial segue a ordem: configurar o Mistral Vibe, instalar o Leanstral 1.5, executar o agente, instalar opcionalmente o Lean LSP MCP e iniciar o trabalho de prova
  • Recomenda-se instalar o Lean LSP MCP adicionando-o a ~/.vibe/config.toml
  • Se não houver servidores MCP existentes, talvez seja necessário remover mcp_servers = []
  • O Leanstral pode ser usado para resolver teoremas, depurar provas e contribuir com repositórios

Leituras relacionadas

1 comentários

 
GN⁺ 4 시간 전
Opiniões no Hacker News

  • A crítica de que é difícil para a Mistral competir com modelos grandes é válida, mas, na prática, vejo a empresa focada em oferecer funções específicas com alta qualidade em modelos pequenos
    Uso a Mistral para tarefas como OCR ou análise de arquivos e, se coloco US$ 100 na conta, dá para rodar por um ano sem me preocupar com volume de requisições
    O custo é extremamente baixo, então, mesmo que não concorra com o Opus 4.8, ainda tem bastante valor

    • Fico curioso para saber quão competitiva ela realmente é em OCR
      Qualidade decente a preço baixo parece mais um nicho do que pagar 10 vezes mais pela melhor qualidade para reduzir erros depois
    • Esses idiotas europeus estão otimizando para criar um bom produto, não para ganhar o máximo de dinheiro possível /s
    • Não sei se “processar documentos de um ano por menos de US$ 100/ano” é tão excelente quanto parece. Pelo menos do ponto de vista da competitividade europeia, isso significa que a Mistral está colocando um teto de receita baixo demais
      OCR já é quase uma commodity, e também é oferecido como recurso básico por modelos open source ou por lugares como a AWS
      Além disso, com uma etiqueta de US$ 100/ano, é difícil criar fidelidade, e não há custo de troca; se aparecer um preço mais baixo, o cliente pode sair imediatamente
      Se não há lock-in de cliente em uma ferramenta barata e fácil de replicar, isso parece mais uma funcionalidade do que um negócio
      É bom para o comprador, mas, se a intenção é que uma empresa europeia concorra no longo prazo com competidores globais em capacidade de produto, parece uma estratégia ruim

  • O trabalho em si é bom, mas o exemplo de descoberta de bug me pareceu estranho
    Disseram que, na função sign da decodificação zigzag, com a entrada Std.U64.MAX, (value + 1) estoura, causando crash em modo debug e corrupção silenciosa em modo release; mas não sei se dá para chamar isso de caso de borda que testes “normalmente deixam passar”
    Testes ruins deixariam passar, mas uma pessoa cuidadosa ou um sistema de codificação baseado em machine learning é bem capaz de pensar “preciso testar valores extremos”. Especialmente se for código que faz parsing de entrada do usuário
    Fico pensando se eles também encontraram bugs mais interessantes, mas usaram esse exemplo por ser difícil explicá-los rapidamente

    • Especialmente a parte de que “até fuzzing deixa passar” é estranha. O fuzzing que eu vi normalmente explora valores de borda de propósito
      Para uma biblioteca de encoding dessas, fuzzing é uma expectativa básica para código decente, e quase certamente teria encontrado isso em poucos segundos
      Na prática, fiz um teste round-trip muito simples com proptest e, em menos de 1 segundo, apareceram dezenas de falhas e o resultado abaixo:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • É difícil dizer que isso “normalmente passa batido”, mas, como de fato existia, é um bug que às vezes passa batido
      A vantagem de usar Lean aparece no fato de que você precisa menos escolher de forma esperta quais exemplos testar
    • Isso é garantia de qualidade básica. Se os testes deixam passar esse tipo de coisa, eles são muito mais limitados do que normalmente esperamos
      Fico curioso sobre o histórico dos autores
    • Isso é simplesmente marketing lixo
      Todo sistema de testes baseados em propriedades inventado por volta de 1980 explora valores de borda
      Testes reais podem ser difíceis por causa da semântica de C e C++, ou da falta dela. Afinal, o compilador pode dizer “teste passou” para qualquer entrada que leve a comportamento indefinido

  • No meio do texto aparecem várias comparações com LLMs de fronteira, mas todos são modelos de meio ano atrás
    Ficou bem engraçado, tipo “nosso modelo novo é melhor que modelos chineses de três gerações atrás”

    • Este é um modelo de 6 bilhões de parâmetros, então é uma categoria completamente diferente. Na verdade, “modelo de linguagem pequeno de fronteira” gera mais expectativa
    • Concordo, mas só o fato de ter pesos abertos e ser relativamente pequeno já vale manchete. Esse modelo roda muito bem

  • A biblioteca é https://github.com/datrs/varinteger
    Uma semana antes da publicação do paper, o mesmo problema já tinha sido aberto nesse repositório, então provavelmente é isso mesmo: https://github.com/datrs/varinteger/issues/8
    Não sei se essa pessoa é funcionária da Leanstral, ou se a Leanstral simplesmente pegou essa issue
    A biblioteca é pequena, tem testes surpreendentemente fracos e está praticamente intocada há 8 anos: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    Os downloads parecem baixos, cerca de 1 mil por dia: https://crates.io/crates/varinteger
    Então é difícil ver isso como um sucesso grande o bastante para ser apresentado como o único exemplo. A detecção automática é útil, sim, mas não sei se é um resultado notável nessa subárea
    Nunca usei um LLM para escrita de provas, mas, como os dados de treinamento tendem a ser escassos, não seria surpreendente se ele fosse mais bruto que modelos gerais de programação
    Como referência, https://crates.io/crates/varinteger mostra https://github.com/mafintosh/varinteger-rs, mas esse endereço redireciona para https://github.com/datrs/varinteger, então, apesar da aparência, parece ser a mesma biblioteca

    • O problema das provas é que às vezes é difícil comunicar seu valor
      O ponto central não é encontrar bugs, mas provar que certos tipos de bug não existem sob certas suposições
      Mas essa história é difícil de vender, então o marketing frequentemente acaba indo para o lado de “encontramos este bug”

  • Poderia ser útil até para alguém que não sabe nada de Lean? Quero verificar um software em que estou trabalhando, mas não tenho experiência com verificação formal
    Fico curioso para saber se dá para obter resultados úteis apenas com a especificação, o código e um tempo limitado de aprendizado

    • É preciso entender a parte que se quer provar, mas não é necessário entender todo o processo de prova
      Parece mais próximo de ler tipos de Haskell do que de matemática; a sensação é que o vocabulário é que toma muito emprestado da matemática
    • Ao ler a seção “Bug Discovery: Finding Hidden Flaws” do texto, parece que eles começaram apenas com código Rust e usaram o modelo para encontrar problemas em Rust open source
      Talvez também dê para receber ajuda conversando com ele para escrever código Lean para verificar uma aplicação, mas não tenho certeza
    • No mínimo, é preciso entender que teorema você quer provar sobre o código e como expressá-lo em Lean
      Caso contrário, não dá para verificar a saída
      Mecanicamente, ele pode ter provado alguma proposição verificada como correta, mas, se você não sabe o que essa proposição significa nem se ela cobre o que de fato quer verificar, isso não tem valor
    • Comecei sem saber nada de Lean4 e, em cerca de 6 meses, cheguei ao ponto de fazer a maior parte da programação em Lean4; esse processo foi bastante acelerado pela assistência de IA
      É impressionante como os modelos são consistentemente fluentes em Lean4. Isso vale não só para modelos de ponta, mas também para modelos locais pequenos; parece que LLMs simplesmente entendem bem Lean4
      Ainda falta um bom caminho para eu me chamar de especialista em Lean4, mas agora não preciso necessariamente de assistência para criar programas úteis
      Mesmo com pouquíssimo conhecimento, poder confiar em partes que você ainda não entende completamente acelera muito o aprendizado. Conseguir programas confiáveis mesmo com conhecimento incompleto é prático e também motivador
      A sensação é que o limite não é todo o conjunto de etapas intermediárias da prova, mas sim a parte da linguagem que descreve seus axiomas e a superfície das suas proposições. Com o tempo, para fazer mais coisas, você precisa entender mais, mas, em certo sentido, dá para trabalhar com segurança no nível N+1
      Além de seu papel como provador de teoremas, Lean4 também é uma linguagem de programação agradável, e é surpreendentemente rápida
      Estou usando junto com io_uring e, em muitos casos, é muito mais rápida que C++/libuv ou Rust/Tokio
      Às vezes, quando aparece uma cauda grande em algo como latência p99.99, é preciso fazer ajustes, como trocar números para largura fixa, mas C++ e Rust também exigem tuning

  • É interessante ver Lean 4 sendo promovido para verificação formal
    Eu achava que essa área era mais de Isabelle/HOL e TLA+
    Eu teria esperado um modelo treinado para usar pelo menos os três. Isabelle/Isar também parece melhor para derivações diretas em álgebra linear; alguém poderia explicar?

    • É verdade que Lean teve menos adoção em verificação de software do que Isabelle ou Rocq, o antigo Coq
      Nessa área, até Agda foi mais usada
      Dito isso, Lean hoje está ganhando bastante tração como alternativa, especialmente por sua capacidade como linguagem funcional de uso geral
      Pessoalmente, acho mais práticos os enfoques baseados em lógica de Hoare ou lógica de separação, que facilitam alinhar requisitos e especificações. Gosto de Dafny e F*

  • Achei divertido os desenvolvedores insinuarem Le Chaton Fat no anúncio do Twitter
    Independentemente de eles terem realmente envolvimento com o Le Chaton Fat, parece que um verdadeiro “novo grande modelo de uso geral” deve chegar em breve
    Como eles o mencionaram diretamente mesmo depois do alvoroço na mídia, fico na expectativa. Espero que o nome seja mais criativo que “Large 4”

  • Dá para experimentar o Leanstral 1.5 no OpenATP mais recente
    O OpenATP é um pacote Python e uma CLI open source para provadores automáticos de teoremas agentivos, com suporte nativo para execução local em Docker ou execução remota em um sandbox da Modal
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com