Maxwell reescribe el binario mientras el programa corre y demuestra que es equivalente
Maxwell: A new kind of model that sits between code and hardware
doubleAI presenta Maxwell, el primer modelo de ejecución de código: observa un programa en marcha, detecta sus cuellos de botella y sustituye las instrucciones por versiones optimizadas para esa máquina y esos datos concretos, sin tocar el código fuente. Cada mejora se acompaña de una prueba formal de equivalencia semántica. En LTX-2.5 logró generar vídeo 4K en casi la mitad de tiempo, y también acelera kernels de inferencia y pipelines de datos en CPU y GPU.
Para Maxwell, la verificación formal toma la forma de pruebas formales de equivalencia semántica.
- epsylon
Hay mucha afirmación y muy pocos detalles técnicos en esa página.
¿Cómo se logró la formalización de Python? ¿Qué framework de prueba formal usas?
¿Cómo reproduces las optimizaciones a través de varias instancias / ejecuciones del programa? (ya que el código fuente no cambia... asumiendo que no rehaces el mismo trabajo una y otra vez?)
¿Qué visibilidad, seguimiento y registro hay sobre el código real que se ejecuta? La depuración es una parte extremadamente importante de la construcción de software, especialmente si hay un demonio intercambiando código binario constantemente por debajo. Incluso si el recompilador es perfecto (no lo será), el código de usuario nunca lo es.
¿Por qué la superoptimización y la visibilidad de los datos no se muestran al nivel del código fuente? Esto parece un desperdicio.
- gavinray
Esto fue mucho más emocionante de lo que esperaba.
La página de inicio no hace un muy buen trabajo explicando qué estamos viendo:
Parece ser una combinación de dos cosas:
1) Una formalización del lenguaje Python
2) Un LLM que se conecta a programas en ejecución e intercambia código en caliente con comportamiento verificablemente equivalente pero mejor rendimiento en tiempo de ejecución, encontrado mediante superoptimización y luego verificado mediante las reglas de formalización
Esto es brillante, y en retrospectiva es una de esas cosas del tipo "No puedo creer que nadie haya pensado en esto todavía".
- mccoyb
Déjame decir que me gusta la idea:
- verificación
- superoptimización especializada para una pieza particular de hardware
- parchear binarios mientras se ejecutan
todo genial
Dicho esto, me están dando algunas vibras extrañas la prosa en este sitio. Pequeñas frases y afirmaciones que parecen destinadas a fines de marketing, pero que confunden cosas con un significado técnico claro de maneras confusas.
Por ejemplo: vi el video ("un modelo de ejecución de código tiene que ser correcto cada vez") que implícitamente comunica algo como "el modelo no puede alucinar" ... por supuesto, el LM agéntico sigue siendo probabilístico, pero está envuelto con herramientas de verificación (para razonar sobre equivalencia semántica), y probablemente está post-entrenado para ser bueno usando esas herramientas.
Esto me parece una confusión entre el modelo y el arnés que está destinada a marcar un punto de marketing (como: "no alucina") pero que es claramente una afirmación ridícula de hacer (cayendo por la pendiente: cualquier arnés que haga corrección de errores para llamadas de herramientas incorrectas también podría ser un "modelo que no comete errores")
También: "código que se auto-mejora"
Eso no es realmente así, ¿verdad? El código que se auto-mejora sería código que se ejecuta a sí mismo y se mejora a sí mismo. Este es código que yo ejecuto, que Maxwell observa y mejora ... ¿no?
Relacionado: no me gusta el uso de la palabra "modelo" en las discusiones anteriores en el sitio. ¿Queremos llamar a todo "modelo" ahora? ¿Puede alguien inventar un nuevo "modelo" de frontera post-entrenando un LM agéntico con herramientas?
Además, digamos […]