Forja y búsqueda que ganan su prueba
El viejo problema del truco
Todo sistema de software serio tiene unas pocas piezas de código que importan mucho más de lo que su tamaño sugiere. Un bucle que se ejecuta millones de veces. Una operación de bits en una ruta de compresión. Una pequeña rutina de matrices. Un núcleo de aritmética modular. El tipo de cosa que parece inofensiva en la revisión de código y luego decide silenciosamente la factura de energía, el presupuesto de latencia o el número de máquinas que necesitas comprar. Muy democrático, el software. Una pequeña función puede arruinar la reunión para todos.
Históricamente, esos núcleos se mejoran con personas. Un ingeniero senior recuerda un truco de un artículo. Alguien rebusca en una publicación antigua de un foro. Se escribe una suite de benchmarks. Se prueban algunos candidatos. El más rápido gana si todavía parece correcto. Entonces la organización lo congela, porque tocarlo de nuevo se siente como pinchar a un transformador dormido con un tenedor.
Forge es una investigación sobre una versión mejor de ese proceso. Es un motor de síntesis de programas para implementaciones pequeñas y críticas: dale una especificación tipada y propiedades, deja que busque programas candidatos, mide y compara las compensaciones, verifica la equivalencia, y luego reduce la implementación descubierta a los objetivos que importan. La palabra importante no es búsqueda. La palabra importante es todavía. Todavía tiene que ser correcto.
Por eso Forge vive en la investigación. No es un botón de producto público donde alguien escribe hazlo más rápido y recibe un milagro. Es un banco de trabajo de síntesis para experimentos con socios, descubrimiento de núcleos e investigación sobre hasta dónde puede llegar la búsqueda automatizada cuando está atada a la verificación en lugar de al teatro de benchmarks.
Una especificación es la línea de salida
Optimizar sin una especificación es solo apostar con nombres de variables más bonitos. En el momento en que aparece un candidato ingenioso, el equipo necesita saber qué se supone que debe preservar. ¿Maneja todas las entradas o solo las amigables del benchmark? ¿Respeta el comportamiento de desbordamiento? ¿Es válida la identidad algebraica bajo la representación realmente utilizada? ¿Mantiene la misma semántica cuando se reduce a un backend diferente?
Forge comienza con expresiones tipadas y propiedades porque la búsqueda necesita un límite. El límite dice qué cuenta como equivalente. Sin él, el motor puede encontrar algo asombrosamente rápido eliminando la mitad del trabajo. Las computadoras son excelentes en el cumplimiento malicioso cuando el contrato es vago.
El lado de la búsqueda es deliberadamente plural. La búsqueda enumerativa es útil cuando el espacio es lo suficientemente pequeño para cubrirlo. CEGIS es útil cuando los contraejemplos pueden guiar el refinamiento. La programación genética y MCTS exploran de manera diferente. La búsqueda guiada por ML puede aprender modelos de costos y priorizar regiones prometedoras. Ninguno de estos es universalmente el mejor. Eso no es una debilidad. Es cómo se comporta la búsqueda en el mundo real. Si un martillo resolviera cada núcleo, las cajas de herramientas serían muy aburridas y los proveedores de hardware estarían desempleados.
La pregunta de investigación es cómo combinar esos motores con suficiente presión de prueba para que el resultado no sea meramente ingenioso. Un núcleo sintetizado tiene que sobrevivir tanto al benchmark del camino feliz como al verificador del camino infeliz. De lo contrario, la mejora no es ingeniería. Es un truco de magia con un costo de mantenimiento.
El verificador es el adulto en la sala
Forge utiliza una pila de verificación porque ninguna comprobación por sí sola es suficiente para todos los dominios. Los ejemplos rápidos son baratos y útiles. Los tests de propiedades detectan clases amplias de errores y reducen los contraejemplos a algo que una persona pueda leer. Los solvers SMT como Z3 y CVC5 pueden demostrar equivalencia cuando la codificación es tratable. La comprobación exhaustiva es práctica para dominios pequeños. La saturación de igualdad con e-graphs ofrece otra vía para la equivalencia algebraica.
La pila importa porque los kernels fallan de maneras molestas. Un candidato puede superar todos los benchmarks ordinarios y aun así fallar en un caso límite. Puede ser correcto para entradas sin signo y erróneo para entradas con signo. Puede ser correcto en un campo matemático y erróneo después de que la representación elegida se desborde. Puede ser correcto antes del lowering y sutilmente erróneo después de una decisión de selección de instrucciones. El verificador existe porque el optimismo no es una estrategia de prueba. Lo comprobamos. Repetidamente. Y sigue siendo cierto.
También hay una razón práctica para mantener varias vías de demostración. Los métodos formales son potentes, pero no son gratuitos. Algunas codificaciones agotan el tiempo. Algunos dominios son demasiado grandes para la comprobación exhaustiva. Algunas propiedades son más fáciles de probar probabilísticamente primero y demostrar después. Forge trata la verificación como un embudo, no como un ritual de pureza. Las comprobaciones baratas rechazan disparates evidentes. Las comprobaciones más sólidas protegen al candidato final.
Rápido no es un solo número
El trabajo de rendimiento se vuelve absurdo cuando una métrica domina todas las conversaciones. La latencia importa. El número de operaciones importa. El uso de memoria importa. La presión de registros importa. El tiempo de compilación a veces importa. La portabilidad importa cuando el mismo kernel debe vivir en más de un backend. Un candidato que gana en latencia quemando registros como una pequeña hoguera puede ser erróneo para el objetivo real. Un candidato pequeño pero lento puede ser útil en otro lugar. El contexto sigue invicto.
Por eso Forge plantea la optimización como un problema de Pareto. El motor puede buscar entre objetivos en lugar de fingir que existe una puntuación universal entregada por una hoja de cálculo muy segura de sí misma. El resultado útil no siempre es el candidato más rápido. A veces es una familia de candidatos con compensaciones visibles, para que una ingeniera pueda elegir el que se ajuste a la restricción de despliegue.
Esta es también la razón por la que no me gustan las afirmaciones desnudas de aceleración en las entradas de blog. La página de investigación puede describir expectativas internas y objetivos experimentales, pero las afirmaciones públicas necesitan ejecuciones recientes, hardware actual, flags de compilador actuales y un contexto de carga de trabajo exacto. De lo contrario, el número se convierte en un recuerdo. Los recuerdos son agradables. No son arquitectura.
La afirmación honesta es más fuerte de todos modos: Forge consiste en hacer la búsqueda reproducible, comparable y comprobable. Cuando un candidato gana, deberíamos saber en qué objetivo ganó, a qué candidatos venció, qué verificador lo aceptó y a qué backend se dirige. Eso es mucho más útil que un número flotando por una presentación aparentando ser caro.
El lowering es donde las pruebas se ponen a prueba
Una implementación descubierta solo es útil si sobrevive al viaje hasta los objetivos reales. La investigación de Forge cubre el descenso a backends como x86-64, RISC-V, WASM, rutas de GPU Vulkan, C y Verilog. Esa lista de objetivos no es decorativa. Cada backend tiene sus propias restricciones, formas de instrucciones, comportamiento de memoria y modos de fallo. La misma especificación tiene que mantener su significado mientras la implementación se convierte en algo que el objetivo pueda ejecutar realmente.
Aquí es donde la síntesis se conecta con el resto de la pila de Dweve. Core quiere bucles internos eficientes. Numerus se preocupa por los núcleos numéricos deterministas. BitWeave quiere operaciones binarias de vectores y matrices que no desperdicien la CPU. Kera se ocupa de bajar grafos de cálculo a hardware real. Forge solo puede alimentar esas capas si la implementación generada es más que rápida. Debe ser equivalente, lo bastante portátil para el objetivo elegido e inspeccionable cuando algo cambia.
Qué supone esto para los equipos
Para un equipo, el cambio interesante no es que una máquina pueda descubrir un núcleo más rápido. Es que el trabajo con núcleos dependa menos del folclore. En lugar de que un experto recuerde el truco adecuado, el proceso pasa a ser: enunciar el contrato, explorar el espacio, medir los candidatos, demostrar la equivalencia, registrar la compensación y generar el código del objetivo. Los humanos siguen decidiendo. Solo dejan de hacer todo el descubrimiento a mano.
Eso importa para las operaciones, porque la deuda de rendimiento es cara de una manera que las organizaciones suelen ocultar. Un núcleo lento se convierte en más servidores. Más servidores se convierten en más coste, más energía, más complejidad de despliegue y más ruido en la planificación. Una optimización incorrecta se convierte en incidentes. Un truco correcto pero sin documentar se convierte en un riesgo de migración futuro. Forge es investigación para reducir esa pila de tonterías evitables.
También hay un cambio cultural. El trabajo manual de rendimiento suele premiar las heroicidades. Alguien desaparece en la cueva y vuelve con un truco ingenioso. Todos aplauden, nadie lo entiende del todo y la empresa ha adquirido un pequeño objeto sagrado. Forge empuja el proceso hacia la evidencia: aquí está la especificación, aquí está la ruta de búsqueda, aquí están los candidatos rechazados, aquí está el verificador, aquí está el backend seleccionado. Menos mitología. Más recibos.
Dónde sigue siendo difícil el trabajo
Nada de esto hace que la síntesis sea fácil. Las especificaciones son difíciles. Si la especificación es incorrecta, el motor puede descubrir fielmente lo incorrecto. Los espacios de búsqueda pueden explotar. Los solvers pueden agotar el tiempo. Los modelos de coste pueden inducir a error. Los backends pueden exponer detalles que la expresión abstracta no tenía en cuenta. La verificación puede ser sólida en un dominio y torpe en otro. Quien venda la síntesis de programas como una máquina expendedora de código óptimo o se salta las partes difíciles o cobra un extra por la decepción.
Forge es interesante precisamente porque se enfrenta directamente a esas partes difíciles. Combina varias estrategias de búsqueda. Mantiene la verificación cerca. Trata los objetivos como compensaciones. Apunta a backends reales. Sigue siendo un programa de investigación porque todavía estamos aprendiendo dónde está el límite entre el descubrimiento automatizado, el juicio humano, los límites de los solvers y la realidad del despliegue.
Ese límite merece la pena explorarse. La industria del software tiene demasiados bucles calientes pequeños, demasiado folclore de rendimiento duplicado y demasiadas optimizaciones que nadie quiere volver a tocar. Si Forge puede convertir aunque sea parte de ese trabajo en un proceso de evidencia repetible, el resultado no es solo código más rápido. Es código más tranquilo. El código tranquilo está infravalorado, sobre todo por quienes no han sido avisados a las 02:17.
Qué necesita una buena ejecución de Forge
Un experimento serio con Forge comienza antes de que el motor se ejecute. El equipo debe aportar un kernel real, no una queja vaga sobre el rendimiento. Se necesitan entradas representativas, casos límite conocidos, hardware objetivo, benchmarks actuales y la razón de negocio por la que este kernel importa. De lo contrario, el motor de síntesis puede dedicar mucho tiempo a resolver un problema que nadie tiene realmente. Las herramientas de investigación no son inmunes a la basura de entrada. Solo hacen que la basura sea más cara de inspeccionar.
La entrada más útil es un contrato pequeño y preciso. ¿Qué se supone que debe calcular la función? ¿Qué leyes algebraicas importan? ¿Qué comportamiento de desbordamiento es intencional? ¿Qué rangos son imposibles por construcción y cuáles simplemente no ocurrieron en la última ejecución de pruebas? ¿Qué salidas pueden tolerar aproximaciones y cuáles no? Un equipo que no puede responder a esas preguntas probablemente todavía no tiene un problema de optimización. Tiene un problema de clarificación de producto disfrazado de compilador.
Una buena ejecución también necesita una postura objetivo. x86-64 y RISC-V no son lo mismo. WASM tiene restricciones diferentes. Las rutas de GPU de Vulkan se preocupan por las formas y el movimiento de memoria. Verilog plantea cuestiones de hardware que los equipos de aplicaciones normales rara vez disfrutan antes del café. Forge puede explorar la bajada a objetivos, pero no puede decidir prioridades organizativas. Si la portabilidad importa más que la velocidad en un objetivo, dígalo. Si la latencia supera a la memoria, dígalo. Si la presión de registros es el límite práctico, dígalo también. El motor es potente, no psíquico.
La salida debe tratarse como un paquete de evidencia. Candidato, objetivo, ruta de prueba, contraejemplos rechazados, backend, contexto de benchmark y salvedades abiertas. Ese paquete es lo que permite a los humanos tomar una decisión sensata. A veces la jugada ganadora es adoptar el candidato. A veces es mantener el kernel antiguo porque la compensación de portabilidad no merece la pena. A veces el descubrimiento es que la especificación era demasiado laxa. Los tres resultados son útiles. Solo uno de ellos parece emocionante en una demo, por eso las demos son un mal sustituto de la ingeniería.
La lección
La lección de Forge es simple: el rendimiento no debe superar a la prueba. La búsqueda es potente, pero un motor de búsqueda sin verificación es solo una forma muy enérgica de crear errores. La verificación es potente, pero sin búsqueda espera a que los humanos le traigan candidatos. Forge une ambas cosas y pregunta qué kernels podemos descubrir cuando a la máquina se le permite explorar, pero no se le permite mentir.
Esa es la investigación que merece la pena. Especificaciones tipadas, búsqueda de candidatos, embudos de prueba, objetivos de Pareto y bajada a backend. No magia. No un atajo de producto. Una forma de hacer mejor código pequeño con evidencia adjunta.