Leanstral 1.5

 (docs.mistral.ai)
1 points par GN⁺ 3 시간 전 | 1 commentaires | Partager sur WhatsApp
  • Leanstral 1.5 est un modèle mis à jour, conçu pour l’ingénierie de preuves formelles Lean 4, visant la démonstration automatique de théorèmes et la formalisation automatique
  • La taille du modèle est de 119B paramètres au total avec 6.5B paramètres actifs, en partant du principe d’un traitement de longs contextes de preuves et de documentation
  • L’identifiant fourni est labs-leanstral-1-5, et il est présenté dans la documentation comme le modèle Labs v1.5
  • La longueur de contexte est de 256k, et le tarif est indiqué à $0, ce qui met l’accent sur son accessibilité pour l’expérimentation et l’évaluation
  • Il peut être utilisé avec les API Chat Completions, Function Calling, agents, sorties structurées, OCR, Document QnA, FIM, embeddings, modération, audio et traitement par lots

Un modèle adapté aux preuves formelles Lean 4

  • Leanstral 1.5 est une version mise à jour du modèle d’ingénierie de preuves formelles Lean 4
  • Les optimisations principales visent la démonstration automatique de théorèmes et la formalisation automatique
  • L’identifiant du modèle est fourni sous la forme labs-leanstral-1-5

Taille du modèle et propriétés de base

  • La configuration des paramètres est indiquée comme 119B total parameters, 6.5B active
  • La longueur de contexte est de 256k
  • Le tarif est indiqué à $0
  • La classification de publication est Labs v1.5

API de conversation, d’agents et de sorties structurées

Traitement de documents, complétion de code et embeddings

Sécurité, audio et traitement par lots

À lire aussi

1 commentaires

 
GN⁺ 3 시간 전
Avis sur Hacker News

  • Par curiosité, je me suis inscrit, j’ai mis de l’argent sur mon compte, puis j’ai essayé de l’utiliser : impossible. Comme c’était censé être un modèle Labs, j’ai voulu activer Labs, mais cette fois j’ai eu une erreur inconnue. En suivant les instructions, j’ai voulu contacter le support client, mais il n’y en a pas, seulement une FAQ bricolée
    La FAQ ressemble à du vibe coding, et la recherche est tellement mauvaise que, quelle que soit la requête, elle renvoie des réponses sans aucun rapport. Et là, j’ai réalisé : si l’IA est si bonne pour le support client, pourquoi les entreprises d’IA ne fournissent-elles pas leur support client avec leur propre IA ?

    • En réalité, certaines le font. Par exemple Cursor. Voir l’ancienne discussion « Cursor IDE support hallucinates lockout policy, causes user cancellations »[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Personne n’a jamais pensé que l’IA faisait bien le support client. Elle ne fait que produire du support client bon marché, et comme beaucoup d’entreprises ne se soucient déjà pas de la qualité du support et fournissaient une assistance médiocre, elles aiment surtout l’idée de réduire encore les coûts
      Du point de vue d’une entreprise que ça agace de devoir dépenser de l’argent pour corriger de vrais problèmes, c’est donc un « bon » support client
    • Ce commentaire m’a fait rire tout en me donnant envie de pleurer. Ça fait tellement UE. Il m’a fallu 18 mois pour décrocher un contrat avec une entreprise de l’UE, et quand je l’ai signé et renvoyé aujourd’hui, j’ai reçu une réponse automatique : « Désolé, je suis en congé jusqu’à fin juillet... »
      Sur l’année écoulée, c’est déjà le quatrième message automatique de congé que je reçois de cette personne
    • C’est étrange et frustrant, mais moi je peux utiliser ce modèle gratuitement alors que je n’ai jamais associé aucun moyen de paiement
    • Ces gens ne répondent pas aux e-mails. qwant, c’était pareil
      L’échantillon ne compte que deux cas, mais ça me pousse à supposer que les entreprises françaises n’aiment pas trop être contactées en anglais

  • C’est un peu un autre sujet, mais c’est assez triste que l’UE n’ait rien sur le véritable marché des LLM de pointe. Surtout quand on pense au fait que les États-Unis ont récemment restreint complètement l’accès aux modèles vraiment à la pointe
    Est-ce que c’était uniquement dû à un manque de financement et d’infrastructures ?

    • Mistral gagne globalement dans les domaines où ils ont choisi de se battre, et c’est ce dont on a besoin en ce moment
      Il est plus juste de regarder ce que l’économie française peut apporter, puis de comparer aux États-Unis ou à la Chine, plutôt que de considérer ce que l’ensemble de l’économie de l’UE peut apporter aux modèles de pointe. L’échelle n’est pas la bonne. En revanche, il faut regarder ce qui peut être accompli à cette échelle plus modeste, et des produits de niche comme Leanstral ou Voxtral en sont le résultat
    • C’est globalement vrai
      La France et l’Allemagne sont les deux plus grandes économies de l’UE : la France a Mistral, et l’Allemagne a un organisme à mi-chemin avec le capital-risque public. Cet organisme est très fier de mettre pas moins de 125 millions d’euros (<150 millions de dollars) pour aider des chercheurs européens à atteindre un nouveau niveau de pointe avec des modèles souverains[1]
      Et cette somme ne va même pas à un seul gagnant, elle est répartie entre plusieurs bénéficiaires. Comme premier pas, c’est sympa, mais pour être exact, cela aurait été un premier pas acceptable il y a 3 ou 4 ans. C’est vraiment dommage
      [1] (en allemand) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Le logiciel en général, et l’IA aussi, sont des marchés où les riches deviennent plus riches et les pauvres plus pauvres. Les grandes entreprises américaines ont les moyens d’aspirer les talents européens et les entreprises européennes émergentes, et elles le font effectivement. Si elles ne veulent pas acheter, elles peuvent aussi les écraser par les prix jusqu’à les faire faillite
      Nous vivons dans une économie coloniale où le capital humain sert de matière première, et tout cela part vers les États-Unis. Pour y échapper, il faut cesser de jouer au jeu actuel et développer des industries compétitives avec une vraie politique industrielle, comme la Chine. Il n’y a pas eu cette volonté au cours des dernières décennies, mais Trump montre très clairement le retour de l’État, et l’Europe commence lentement à l’admettre
    • Mistral a levé plus de 4 milliards de dollars, ce qui est déjà une somme importante, mais pas au niveau d’OpenAI/Anthropic/xAI
      La difficulté, c’est de justifier financièrement le développement pur de LLM. Les modèles se ressemblent énormément. OpenAI s’est d’abord justifiée comme une « organisation caritative » dédiée à la recherche pure, et Anthropic s’est séparée en affirmant qu’OpenAI ne se préoccupait pas assez de la sécurité. Elon a dit que, s’il ne créait pas Grok, l’IA ferait semblant d’être woke et ne dirait pas la vérité, et Google a créé Gemini parce qu’ils étaient à l’origine du domaine et que la recherche en IA faisait partie de la mission centrale donnée par Larry et Sergey à la fondation de l’entreprise. Simplement, ils l’ont laissée de côté pendant un moment pour des raisons financières
      Les motivations des modèles chinois sont franchement floues. Je n’ai jamais vu de bonne explication, seulement des hypothèses. Mais vu qu’ils les publient gratuitement ou à des prix excessivement bas, leurs motivations ne semblent pas non plus financières
      Mistral, en revanche, est une entreprise ordinaire. Comme elle n’a pas de riche mécène prêt à y engloutir de l’argent en croyant à un récit de destin cosmique, elle doit justifier ce qu’elle fait par le retour sur investissement. Et dans ce cas, l’entraînement de LLM à grande échelle est quasiment exclu
      Il faut aussi tenir compte de la réglementation de l’UE. Quand j’avais regardé, il y avait beaucoup de règles étranges qui éliminaient les perspectives de l’industrie technologique européenne. Au Royaume-Uni, il existait même une règle selon laquelle on ne pouvait crawler Internet qu’à des fins de recherche
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Et sans Premier amendement, le risque d’être poursuivi pour ce qu’un modèle a dit est beaucoup plus élevé. Il suffit de voir le cas où l’Allemagne a traîné Google en justice à cause de contenu inséré par un modèle dans une page de résultats de recherche
      Donc les bénéfices sont incertains et le risque juridique est très élevé
    • L’UE n’a pas de véritable marché commun, en particulier sur les marchés de capitaux. Même si sa population est plus nombreuse que celle des États-Unis et que son économie totale est plus grande, cela ne signifie pas grand-chose si elle ne peut pas mutualiser efficacement ses ressources
      En Europe, serait-il possible de lever 100 milliards de dollars pour un nouveau labo ? Si la réponse est non, alors c’est terminé, autant abandonner

  • Quelle coïncidence. J’ai justement publié OpenATP ce matin. OpenATP est un package Python open source et une CLI pour les démonstrateurs automatiques de théorèmes agentiques
    Il inclut aussi la prise en charge de Leanstral via le harness Vibe de Mistral. Le précédent modèle Leanstral de production a été retiré le 22 mai, et je mettrai le package à jour dès que possible pour qu’il pointe vers Leanstral 1.5
    GitHub : https://github.com/henryrobbins/open-atp
    Docs : https://open-atp.henryrobbins.com

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

  • Je ne comprends pas bien la politique sur les poids. Le site indique que les poids sont sous licence Apache, donc ça ressemble à des poids ouverts, mais je ne trouve pas de lien de téléchargement
    Le profil Hugging Face semble ne proposer que d’anciens snapshots[0]. Quelqu’un sait-il si les poids peuvent être téléchargés et, si oui, où les obtenir ?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Moi aussi j’ai « Page not found ». Tu as réussi à y accéder ? Ça disait quoi ?

    • D’après Web Archive : Leanstral 1.5 - 30 juin 2026
      Un modèle d’ingénierie de preuves formelles Lean 4 mis à jour et optimisé pour la démonstration automatique de théorèmes et la formalisation automatique. 119B de paramètres au total, 6,5B actifs
      https://web.archive.org/web/20260630223430/https://docs.mist...

  • Discussion sur Leanstral 1 : https://news.ycombinator.com/item?id=47404796

  • Lean 4 et Idris 2 sont sous-estimés et, comme ils offrent des garanties supplémentaires, ils pourraient être très adaptés au codage par les LLM

  • Ça renvoie une 404 maintenant

  • Je me suis inscrit à cause de cette annonce, mais faut-il connecter GitHub pour utiliser « Code » ? Ça paraît très restrictif