Leanstral 1.5

 (docs.mistral.ai)
1 pontos por GN⁺ 3 시간 전 | 1 comentários | Compartilhar no WhatsApp
  • Leanstral 1.5 é um modelo atualizado voltado para engenharia de provas formais em Lean 4, com foco em prova automática de teoremas e formalização automática
  • A escala do modelo é composta por 119B de parâmetros no total e 6.5B de parâmetros ativos, partindo do pressuposto de processamento de contextos longos de provas e documentos
  • O identificador fornecido é labs-leanstral-1-5, e na documentação ele aparece como modelo Labs v1.5
  • O comprimento de contexto é 256k, e o item de preço aparece como $0, enfatizando a acessibilidade para experimentação e avaliação
  • Pode ser usado com as APIs de Chat Completions, chamada de função, agentes, saídas estruturadas, OCR, Document QnA, FIM, embeddings, moderação, áudio e processamento em lote

Modelo voltado para provas formais em Lean 4

  • Leanstral 1.5 é uma versão atualizada de um modelo de engenharia de provas formais em Lean 4
  • Os principais alvos de otimização são prova automática de teoremas e formalização automática
  • O identificador do modelo é fornecido como labs-leanstral-1-5

Escala do modelo e atributos básicos

  • A configuração de parâmetros é indicada como 119B total parameters, 6.5B active
  • O comprimento de contexto é 256k
  • O item de preço aparece como $0
  • A classificação da versão é Labs v1.5

API de conversa, agentes e saídas estruturadas

Processamento de documentos, completamento de código e embeddings

Segurança, áudio e processamento em lote

Leituras relacionadas

1 comentários

 
GN⁺ 3 시간 전
Comentários do Hacker News

  • Fiquei curioso, me cadastrei, coloquei dinheiro na conta e tentei usar, mas não funcionou. Como dizia que era um modelo Labs, tentei ativar o Labs, e aí apareceu um erro desconhecido. Tentei entrar em contato com o suporte como orientado, mas não existe suporte ao cliente, só um FAQ feito de qualquer jeito
    O FAQ parece ter sido feito em vibe coding e a busca é péssima, então não importa o que você pesquise, só aparecem respostas totalmente sem relação. Aí me toquei: se a IA é boa em atendimento ao cliente, por que as empresas de IA não usam a própria IA para oferecer suporte?

    • Na prática usam, sim. Por exemplo, a Cursor. Veja a discussão anterior: “Cursor IDE support hallucinates lockout policy, causes user cancellations”[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Ninguém achava que a IA fosse boa em atendimento ao cliente. Ela só cria um suporte barato, e como muitas empresas já não ligavam para a qualidade do suporte e sempre ofereceram um atendimento ruim, gostam da ideia de poder cortar ainda mais custos
      Do ponto de vista de uma empresa que acha irritante gastar dinheiro para resolver o problema de verdade, isso é um suporte “bom”
    • Ri e ao mesmo tempo fiquei meio emocionado com esse comentário. Parece tão europeu. Levei 18 meses para fechar um contrato empresarial na UE, e hoje, logo depois de assinar e devolver, recebi uma resposta automática dizendo “desculpe, estou de férias até o fim de julho...”
      Esta já é a quarta resposta automática de férias que recebo dessa pessoa no último ano em que estivemos em contato
    • É estranho e frustrante, mas eu consigo usar esse modelo de graça mesmo sem nunca ter vinculado nenhum meio de pagamento
    • Eles não respondem e-mails. A qwant também era assim
      A amostra é de apenas dois casos, mas isso me faz supor que empresas francesas não gostam muito de ser contatadas em inglês

  • Mudando um pouco de assunto, é bem triste que a UE não tenha praticamente nada no mercado de LLMs de ponta. Ainda mais quando se pensa no fato de que, recentemente, os EUA restringiram completamente o acesso aos modelos realmente de ponta
    Será que isso foi puramente por falta de financiamento e infraestrutura?

    • A Mistral geralmente vence nos segmentos em que decidiu competir, e no momento é disso que há necessidade
      Em vez de comparar com EUA ou China olhando para o quanto a economia da UE como um todo pode contribuir para modelos de ponta, faz mais sentido olhar para o quanto a economia francesa pode contribuir. A escala simplesmente não existe. Em vez disso, vale observar o que conseguem fazer com essa escala menor, e produtos de nicho como Leanstral e Voxtral são o resultado disso
    • Em linhas gerais, sim
      França e Alemanha são as maiores economias da UE; a França tem a Mistral, e a Alemanha tem uma instituição com perfil de venture capital apoiado pelo governo. Essa instituição se orgulha muito de oferecer nada menos que 125 milhões de euros (<150 milhões de dólares) para ajudar pesquisadores europeus a alcançar um novo estado da arte em modelos soberanos[1]
      E esse dinheiro não vai para um único vencedor, mas será dividido entre vários beneficiários. Como primeiro passo, é ótimo, mas para ser exato, teria sido um primeiro passo adequado há 3 ou 4 anos. Uma pena
      [1] (alemão) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Em software em geral, e em IA também, o mercado é de ricos ficam mais ricos. As big techs americanas têm recursos para absorver talentos europeus e empresas europeias promissoras, e de fato fazem isso. Se não quiserem comprar, podem quebrá-las pressionando por preço
      Vivemos em uma economia colonial em que o capital humano é a matéria-prima, e tudo isso flui para os EUA. Para evitar isso, precisamos parar de jogar o jogo atual e, como a China, desenvolver indústrias competitivas com uma política industrial de verdade. Não houve vontade para isso nas últimas décadas, mas Trump está mostrando de forma muito clara o retorno do Estado, e a Europa está reconhecendo isso lentamente
    • A Mistral levantou mais de 4 bilhões de dólares, então é bastante dinheiro, mas não está no nível de OpenAI/Anthropic/xAI
      A parte difícil é justificar financeiramente o desenvolvimento de LLMs puros. Os modelos são muito parecidos entre si. A OpenAI justificou isso no começo com a ideia de ser uma “instituição de caridade” para pesquisa pura; a Anthropic surgiu da separação de pessoas que diziam que a OpenAI não se preocupava o suficiente com segurança. Elon disse que, se não criasse o Grok, a IA fingiria ser woke e não seria sincera, e o Google criou o Gemini porque eles estavam na origem disso tudo e porque a pesquisa em IA era uma missão central dada por Larry e Sergey na fundação da empresa. Só que isso ficou engavetado por um tempo por motivos financeiros
      No caso dos modelos chineses, a motivação honestamente não está clara. Nunca vi uma grande explicação, só hipóteses. Mas, considerando que são liberados de graça ou a preços absurdamente baixos, essa motivação também não parece ser financeira
      Já a Mistral é uma empresa comum. Não tem um patrono bilionário despejando dinheiro por acreditar numa narrativa de destino cósmico, então precisa justificar o que faz em termos de retorno sobre investimento. Isso praticamente elimina o treinamento de LLMs em larga escala
      Também é preciso considerar a regulação da UE. Da última vez que procurei, havia muitas regras estranhas que acabavam com o potencial da indústria tecnológica europeia. No Reino Unido, havia até uma regra segundo a qual a internet só podia ser rastreada para fins de pesquisa
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      E sem a Primeira Emenda, o risco de processo por causa do que um modelo disse é muito maior. Basta ver o caso em que a Alemanha levou o Google aos tribunais por conteúdo inserido por um modelo numa página de resultados de busca
      Então os lucros são incertos e o risco jurídico é muito alto
    • A UE não tem um verdadeiro mercado comum, especialmente em mercados de capitais. Mesmo com mais população e uma economia total maior do que a dos EUA, isso não significa muita coisa se não for possível reunir recursos de forma eficiente
      A Europa conseguiria levantar 100 bilhões de dólares para um novo laboratório de pesquisa? Se não, então acabou e é melhor desistir

  • Que coincidência. Acabei de lançar o OpenATP hoje de manhã. O OpenATP é um pacote Python open source e também uma CLI para provadores automáticos de teoremas com agentes
    Ele também inclui suporte ao Leanstral por meio do harness Vibe da Mistral. O modelo Leanstral anterior de produção foi descontinuado em 22 de maio, e pretendo atualizar o pacote para apontar para o Leanstral 1.5 o quanto antes
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • É 404?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • Não entendo bem a política de pesos. Este site faz parecer que os pesos são públicos, já que diz que eles usam licença Apache, mas não consigo encontrar um link para download
    No perfil do Hugging Face, parece que só há o snapshot anterior[0]. Alguém sabe se é possível baixar os pesos e, se sim, de onde?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Para mim também aparece “Page not found”. Você conseguiu acessar? Sobre o que era isso?

  • Discussão sobre o Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 e Idris 2 são subestimados e, por oferecerem garantias adicionais, têm grande potencial para serem ótimos para LLMs programarem

  • Agora está dando 404

  • Criei uma conta por causa dessa notícia, mas para usar o “Code” preciso conectar o GitHub? Parece restritivo demais