Leanstral 1.5

 (docs.mistral.ai)
1 puntos por GN⁺ 3 시간 전 | 1 comentarios | Compartir por WhatsApp
  • Leanstral 1.5 es un modelo actualizado, orientado a la ingeniería de pruebas formales con Lean 4, enfocado en la demostración automática de teoremas y la formalización automática
  • La escala del modelo se compone de 119B parámetros totales y 6.5B parámetros activos, asumiendo el manejo de contextos largos de pruebas y documentos
  • El identificador disponible es labs-leanstral-1-5, y en la documentación aparece como modelo Labs v1.5
  • La longitud de contexto es de 256k, y el precio figura como $0, destacando su accesibilidad para experimentación y evaluación
  • Puede usarse junto con las API de Chat Completions, llamadas a funciones, agentes, salidas estructuradas, OCR, Document QnA, FIM, embeddings, moderación, audio y procesamiento por lotes

Modelo orientado a pruebas formales con Lean 4

  • Leanstral 1.5 es una versión actualizada del modelo de ingeniería de pruebas formales para Lean 4
  • Sus optimizaciones principales apuntan a la demostración automática de teoremas y la formalización automática
  • El identificador del modelo se ofrece como labs-leanstral-1-5

Escala del modelo y propiedades básicas

  • La configuración de parámetros se muestra como 119B total parameters, 6.5B active
  • La longitud de contexto es de 256k
  • El precio figura como $0
  • La clasificación de lanzamiento es Labs v1.5

API de conversación, agentes y salidas estructuradas

Procesamiento de documentos, completado de código y embeddings

Seguridad, audio y procesamiento por lotes

Lecturas relacionadas

1 comentarios

 
GN⁺ 3 시간 전
Opiniones de Hacker News

  • Me dio curiosidad, me registré, puse dinero en la cuenta y cuando intenté usarlo, no funcionó. Como decía que era un modelo de Labs, intenté activar Labs, pero esta vez me salió un error desconocido. Quise contactar a soporte como indicaban, pero no había soporte, solo una FAQ hecha a la rápida.
    La FAQ parecía vibe-coded y la búsqueda era pésima: sin importar qué consulta pusiera, solo devolvía respuestas totalmente irrelevantes. Entonces caí en cuenta: si la IA es buena para atención al cliente, ¿por qué las empresas de IA no ofrecen soporte al cliente con su propia IA?

    • De hecho sí la usan. Por ejemplo, Cursor. Puedes ver la discusión anterior “Cursor IDE support hallucinates lockout policy, causes user cancellations”[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Nadie pensó que la IA fuera buena para atención al cliente. Solo permite crear soporte barato, y como muchas empresas ya no se preocupan por la calidad del soporte y venían dando una atención pésima, les gusta porque pueden reducir aún más los costos.
      Para una empresa a la que le molesta tener que gastar dinero en arreglar problemas reales, eso cuenta como “buen” soporte al cliente.
    • Este comentario me hizo reír y a la vez me dio un nudo en la garganta. Se siente demasiado a la UE. Me tomó 18 meses cerrar un contrato con una empresa de la UE; hoy lo firmé y lo envié de vuelta, y recibí una respuesta automática que decía: “Disculpe, estoy de vacaciones hasta fines de julio...”.
      En el último año, esta es la cuarta respuesta automática de vacaciones que recibo de esta persona.
    • Es raro y frustrante, pero yo puedo usar este modelo gratis aunque nunca haya vinculado ningún método de pago.
    • Esta gente no responde correos. Con qwant fue igual.
      La muestra es de solo dos casos, pero me hace asumir que a las empresas francesas no les gusta mucho que las contacten en inglés.

  • Es un tema un poco distinto, pero es bastante triste que la UE no tenga nada en el mercado de LLM realmente de frontera. Sobre todo considerando que hace poco EE. UU. restringió por completo el acceso a los modelos verdaderamente de frontera.
    ¿Será solo por falta de financiamiento e infraestructura?

    • Mistral, en general, está ganando en el terreno en el que decidió competir, y por ahora eso es lo que hace falta.
      Más que mirar cuánto puede aportar toda la economía de la UE a los modelos de frontera, es más preciso mirar cuánto puede aportar la economía francesa y compararla con EE. UU. o China. No da la escala. En cambio, conviene mirar qué logra con esa escala menor, y productos de nicho como Leanstral y Voxtral son resultado de eso.
    • En general, de acuerdo.
      Francia y Alemania son las economías más grandes de la UE; Francia tiene a Mistral, y Alemania tiene una institución con carácter de venture capital respaldado por el gobierno. Esa institución se muestra muy orgullosa de poner nada menos que 125 millones de euros (<150 millones de dólares) para ayudar a investigadores europeos a lograr un nuevo estado del arte en modelos soberanos[1].
      Ese dinero ni siquiera va a un único ganador, sino que se reparte entre varios beneficiarios. Como primer paso está bien, pero, para ser exactos, habría sido un primer paso aceptable hace 3 o 4 años. Una verdadera lástima.
      [1] (en alemán) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • El software en general, y también la IA, son mercados donde los ricos se hacen más ricos y los pobres más pobres. Las grandes empresas estadounidenses tienen la capacidad de absorber talento europeo y empresas europeas emergentes, y de hecho lo hacen. Si no quieren comprarlas, también pueden asfixiarlas con precios hasta llevarlas a la quiebra.
      Vivimos en una economía colonial donde el capital humano es la materia prima, y todo fluye hacia EE. UU. Para evitarlo, hay que dejar de jugar el juego actual y, como China, desarrollar industrias competitivas con una política industrial en serio. En las últimas décadas no hubo voluntad para eso, pero Trump está mostrando con mucha claridad el regreso del Estado, y Europa lo está reconociendo lentamente.
    • Mistral ha levantado más de 4.000 millones de dólares, así que es bastante dinero, pero no está al nivel de OpenAI/Anthropic/xAI.
      Lo difícil es justificar financieramente el desarrollo puro de LLM. Los modelos son muy parecidos entre sí. OpenAI se justificó al principio como una “organización benéfica” dedicada a la investigación pura, y Anthropic se separó diciendo que OpenAI no se preocupaba lo suficiente por la seguridad. Elon dijo que, si él no creaba Grok, la IA fingiría estar despierta y no sería veraz; y Google creó Gemini porque originalmente ellos fueron el punto de partida y la investigación en IA era una misión central que Larry y Sergey le dieron a la empresa al fundarla. Aunque, por razones financieras, la dejaron en pausa durante un tiempo.
      La motivación de los modelos chinos, sinceramente, no está clara. No he visto una buena explicación, solo hipótesis. Pero viendo que los liberan gratis o los ofrecen a precios demasiado bajos, tampoco parece que su motivación sea financiera.
      En cambio, Mistral es una empresa normal. No tiene un patrocinador rico que crea en una narrativa de destino cósmico y meta dinero a raudales, así que tiene que justificar lo que hace por retorno de inversión. Eso prácticamente descarta entrenar LLM a gran escala.
      También hay que considerar la regulación de la UE. Cuando lo revisé hace un tiempo, había muchas reglas extrañas que eliminaban las posibilidades de la industria tecnológica europea. En Reino Unido incluso había una norma que permitía rastrear la web solo con fines de investigación.
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Y sin la Primera Enmienda, el riesgo de ser procesado por algo que dijo un modelo es mucho mayor. Basta ver el caso en que Alemania llevó a Google a los tribunales por contenido que el modelo había incluido en una página de resultados de búsqueda.
      Así que las ganancias son inciertas y el riesgo legal es muy alto.
    • La UE no tiene un mercado común real, especialmente en los mercados de capitales. Aunque tenga más población que EE. UU. y una economía agregada más grande, eso no significa mucho si no puede reunir recursos de manera eficiente.
      ¿Sería posible levantar 100.000 millones de dólares para un nuevo laboratorio en Europa? Si no, se acabó, y mejor rendirse.

  • Qué casualidad. Esta mañana acabo de lanzar OpenATP. OpenATP es un paquete de Python open source y una CLI para demostradores automáticos de teoremas de tipo agente.
    También incluye soporte para Leanstral mediante el harness Vibe de Mistral. El modelo Leanstral de producción anterior se retiró el 22 de mayo, y voy a actualizar el paquete lo antes posible para que apunte a Leanstral 1.5.
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

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

  • No entiendo bien la política de pesos. Este sitio dice que los pesos tienen licencia Apache, así que parecen pesos abiertos, pero no encuentro un enlace de descarga.
    El perfil de Hugging Face parece ofrecer solo snapshots anteriores[0]. ¿Alguien sabe si se pueden descargar los pesos y, de ser así, de dónde?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • A mí también me aparece “Page not found”. ¿Lograste acceder? ¿De qué trata?

  • Discusión sobre Leanstral 1: https://news.ycombinator.com/item?id=47404796

  • Lean 4 e Idris 2 están subvalorados y, como ofrecen garantías adicionales, tienen muchas posibilidades de ser excelentes para que los LLM programen.

  • Ahora mismo da 404.

  • Me registré por esta noticia, pero para usar “Code”, ¿hay que hacer una conexión con GitHub? Se ve demasiado restrictivo.