Leanstral 1.5

 (docs.mistral.ai)
1 Punkte von GN⁺ 3 시간 전 | 1 Kommentare | Auf WhatsApp teilen
  • Leanstral 1.5 ist ein aktualisiertes Modell, das auf formales Beweis-Engineering mit Lean 4 zugeschnitten ist und auf automatisierte Theorembeweise sowie automatische Formalisierung abzielt
  • Die Modellgröße besteht aus insgesamt 119B Parametern und 6.5B aktiven Parametern und ist auf die Verarbeitung langer Beweis- und Dokumentkontexte ausgelegt
  • Die bereitgestellte Kennung ist labs-leanstral-1-5, in der Dokumentation als Labs v1.5 ausgewiesen
  • Die Kontextlänge beträgt 256k, der Preiseintrag ist mit $0 angegeben, was die Zugänglichkeit für Experimente und Evaluierungen betont
  • Kann zusammen mit Chat Completions, Function Calling, Agents, Structured Outputs, OCR, Document QnA, FIM, Embeddings, Moderations, Audio und Batch-Processing-APIs verwendet werden

Modell für formale Beweise mit Lean 4

  • Leanstral 1.5 ist eine aktualisierte Version des Modells für formales Beweis-Engineering mit Lean 4
  • Die zentrale Optimierung zielt auf automatisierte Theorembeweise und automatische Formalisierung
  • Die Modellkennung wird als labs-leanstral-1-5 bereitgestellt

Modellgröße und Grundeigenschaften

  • Die Parameterkonfiguration ist als 119B total parameters, 6.5B active angegeben
  • Die Kontextlänge beträgt 256k
  • Der Preiseintrag ist mit $0 angegeben
  • Die Release-Kategorie ist Labs v1.5

APIs für Dialoge, Agents und strukturierte Ausgaben

Dokumentverarbeitung, Code-Vervollständigung und Embeddings

Sicherheit, Audio und Batch-Verarbeitung

Verwandte Beiträge

1 Kommentare

 
GN⁺ 3 시간 전
Meinungen auf Hacker News

  • Aus Neugier registriert, Geld auf das Konto eingezahlt und versucht, es zu nutzen – ging nicht. Weil es ein Labs-Modell sein sollte, wollte ich Labs aktivieren, doch diesmal kam ein unbekannter Fehler. Als ich mich wie angegeben an den Kundensupport wenden wollte, gab es keinen Kundensupport, nur eine schnell zusammengeschusterte FAQ
    Die FAQ sieht aus, als wäre sie vibe-coded, und die Suche ist miserabel: Egal welche Anfrage man eingibt, es kommen völlig irrelevante Antworten. Dann wurde mir klar: Wenn AI gut im Kundensupport ist, warum bieten dann AI-Unternehmen ihren Kundensupport nicht mit ihrer eigenen AI an?

    • Tun sie tatsächlich. Zum Beispiel Cursor. Siehe die frühere Diskussion „Cursor IDE support hallucinates lockout policy, causes user cancellations“[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Niemand dachte, dass AI gut im Kundensupport sei. Sie liefert nur billigen Kundensupport, und weil vielen Unternehmen die Qualität des Kundensupports ohnehin egal ist und sie schon bisher miesen Support angeboten haben, freut sie daran, die Kosten weiter senken zu können
      Aus Sicht eines Unternehmens, das es nervt, Geld für die Behebung echter Probleme ausgeben zu müssen, ist das eben „guter“ Kundensupport
    • Bei diesem Kommentar musste ich lachen und war gleichzeitig gerührt. Es fühlt sich so unglaublich EU-typisch an. Es hat 18 Monate gedauert, einen Vertrag mit einem EU-Unternehmen zu bekommen; heute habe ich unterschrieben und zurückgeschickt, und als automatische Antwort kam: „Leider bin ich bis Ende Juli im Urlaub ...“
      In dem Jahr, in dem ich mit dieser Person in Kontakt stand, ist das schon die vierte Urlaubs-Abwesenheitsnotiz
    • Seltsam und frustrierend, aber ich kann dieses Modell kostenlos nutzen, obwohl ich nie irgendeine Zahlungsmethode verknüpft habe
    • Diese Leute antworten nicht auf E-Mails. Bei qwant war es genauso
      Die Stichprobe besteht zwar nur aus zwei Fällen, aber sie bringt mich zu der Annahme, dass französische Unternehmen nicht besonders gern auf Englisch kontaktiert werden

  • Etwas anderes Thema, aber es ist ziemlich traurig, dass die EU im tatsächlichen Frontier-LLM-Markt nichts vorzuweisen hat. Besonders wenn man bedenkt, dass die USA kürzlich den Zugang zu echten Frontier-Modellen vollständig eingeschränkt haben
    Lag das wirklich nur an fehlendem Kapital und fehlender Infrastruktur?

    • Mistral gewinnt in den Bereichen, in denen sie sich entschieden haben zu kämpfen, im Großen und Ganzen, und genau das wird im Moment gebraucht
      Statt zu betrachten, wie viel die gesamte EU-Wirtschaft zu Frontier-Modellen beitragen kann, ist es treffender zu schauen, wie viel die französische Wirtschaft beitragen kann, und das mit den USA oder China zu vergleichen. Die Größenordnung passt nicht. Besser ist es, darauf zu schauen, was mit dieser geringeren Größenordnung erreicht wird; Nischenprodukte wie Leanstral und Voxtral sind genau solche Ergebnisse
    • Im Großen und Ganzen stimmt das
      Frankreich und Deutschland sind die größten Volkswirtschaften der EU; Frankreich hat Mistral, und Deutschland hat eine Einrichtung mit dem Charakter eines staatlich unterstützten Venture-Capital-Fonds. Diese Einrichtung ist sehr stolz darauf, ganze 125 Mio. Euro (<150 Mio. Dollar) bereitzustellen, um europäischen Forschern zu helfen, mit souveränen Modellen den neuen Stand der Technik zu erreichen[1]
      Das Geld geht nicht einmal an einen einzigen Gewinner, sondern wird auf mehrere Empfänger verteilt. Als erster Schritt ist das nett, aber genau genommen wäre es vor drei bis vier Jahren ein passender erster Schritt gewesen. Wirklich schade
      [1] (Deutsch) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Software insgesamt und auch AI sind Märkte, in denen die Reichen reicher und die Armen ärmer werden. Große US-Konzerne haben die Mittel, europäische Talente und aufstrebende europäische Unternehmen aufzukaufen, und sie tun das auch. Wenn sie nicht kaufen wollen, können sie sie auch über den Preis unter Druck setzen und in die Insolvenz treiben
      Wir leben in einer Kolonialwirtschaft, in der Humankapital als Rohstoff dient, und alles fließt in die USA. Um dem zu entgehen, müssten wir aufhören, das aktuelle Spiel mitzuspielen, und wie China mit einer ernsthaften Industriepolitik wettbewerbsfähige Industrien aufbauen. In den letzten Jahrzehnten gab es diesen Willen nicht, aber Trump zeigt die Rückkehr des Staates sehr deutlich, und Europa erkennt das langsam an
    • Mistral hat über 4 Mrd. Dollar eingesammelt, also durchaus viel Geld, aber nicht auf dem Niveau von OpenAI/Anthropic/xAI
      Der schwierige Teil ist, reine LLM-Entwicklung finanziell zu rechtfertigen. Die Modelle sind einander sehr ähnlich. OpenAI rechtfertigte sich anfangs als „Wohltätigkeitsorganisation“ für reine Forschung, und Anthropic spaltete sich ab mit der Begründung, OpenAI kümmere sich nicht ausreichend um Sicherheit. Elon sagte, wenn er Grok nicht baue, werde AI so tun, als sei sie woke, und nicht wahrhaftig sein; Google baute Gemini, weil sie ursprünglich der Ausgangspunkt waren und AI-Forschung zu der Kernmission gehörte, die Larry und Sergey dem Unternehmen bei der Gründung gegeben hatten. Aus finanziellen Gründen hatten sie das allerdings eine Zeit lang liegen lassen
      Die Motivation der chinesischen Modelle ist ehrlich gesagt unklar. Ich habe keine gute Erklärung gesehen, nur Hypothesen. Aber wenn man sieht, dass sie kostenlos veröffentlicht oder viel zu billig angeboten werden, scheint diese Motivation ebenfalls nicht finanziell zu sein
      Mistral dagegen ist ein normales Unternehmen. Ohne wohlhabende Unterstützer, die an eine kosmische Schicksalserzählung glauben und Geld hineinwerfen, müssen sie ihre Arbeit über den Return on Investment rechtfertigen. Damit fällt groß angelegtes LLM-Training praktisch aus
      Auch EU-Regulierung muss man berücksichtigen. Als ich früher dazu recherchiert habe, gab es viele seltsame Regeln, die die Chancen einer europäischen Tech-Industrie zunichtemachen. In Großbritannien gab es sogar eine Vorschrift, nach der man das Internet nur zu Forschungszwecken crawlen darf
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Und ohne den First Amendment ist das Risiko viel größer, wegen etwas, das ein Modell gesagt hat, strafrechtlich verfolgt zu werden. Man denke an den Fall, in dem Deutschland Google wegen Inhalten vor Gericht brachte, die ein Modell in eine Suchergebnisseite eingefügt hatte
      Deshalb sind die Gewinne unklar und die rechtlichen Risiken sehr groß
    • Die EU hat keinen funktionierenden gemeinsamen Markt, insbesondere nicht bei den Kapitalmärkten. Selbst wenn sie mehr Einwohner und eine größere Gesamtwirtschaft als die USA hat, bedeutet das wenig, wenn sie Ressourcen nicht effizient bündeln kann
      Wäre es in Europa möglich, 100 Mrd. Dollar für ein neues Forschungslabor aufzubringen? Wenn nicht, ist die Sache erledigt, und man kann aufgeben

  • Zufall. Ich habe heute Morgen gerade OpenATP veröffentlicht. OpenATP ist ein Open-Source-Python-Paket und CLI für agentische automatische Theorembeweiser.
    Unterstützung für Leanstral über Mistrals Vibe-Harness ist ebenfalls enthalten. Das frühere Production-Leanstral-Modell wurde am 22. Mai eingestellt, und ich werde das Paket so schnell wie möglich aktualisieren, damit es auf Leanstral 1.5 verweist.
    GitHub: https://github.com/henryrobbins/open-atp
    Doku: https://open-atp.henryrobbins.com

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

  • Ich verstehe die Gewichtungsrichtlinie nicht ganz. Auf der Website heißt es, die Gewichte stünden unter Apache-Lizenz, was nach offenen Gewichten aussieht, aber ich finde keinen Download-Link.
    Im Hugging-Face-Profil scheinen nur ältere Snapshots verfügbar zu sein[0]. Weiß jemand, ob man die Gewichte herunterladen kann, und wenn ja, wo?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Bei mir kommt auch „Page not found“. Konntest du darauf zugreifen? Worum geht es hier?

  • Diskussion zu Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 und Idris 2 werden unterschätzt und könnten, da sie zusätzliche Garantien bieten, sehr gut für LLMs zum Coden geeignet sein.

  • Aktuell gibt es einen 404.

  • Ich habe mich wegen dieser Meldung angemeldet, aber muss man eine GitHub-Verknüpfung einrichten, um „Code“ zu nutzen? Wirkt sehr restriktiv.