Lanyon AI revela ronda de $10.6M para código científico verificado formalmente
El laboratorio con sede en Princeton empareja un LLM con un compilador simbólico para generar código científico y pruebas verificables por máquina a partir de una sola especificación.
By RuntimeWire Staff · Published
Primary source: PR Newswire
Why it matters
Formal verification can make AI-generated scientific software auditable, but its value depends on whether the certified specification captures the engineer's real intent.
Jonathan Gorard, Ammar Hakim, and James "Jimmy" Juno revelaron una ronda inicial de recaudación de fondos de 10.6 millones de dólares para Lanyon AI el 17 de agosto, respaldando su intento de hacer que el software científico generado por IA demuestre que hace lo que su especificación requiere.
Dimension lideró la financiación, con la participación de Industrious Ventures, según el anuncio de Lanyon AI. El laboratorio de investigación en Princeton, Nueva Jersey, está orientado a aeroespacial, propulsión, energía nuclear, simulaciones de física, optimización para GPU e inferencia de IA, donde una respuesta plausible aún puede ser peligrosa.
La ronda pone capital detrás de un equipo fundador reunido desde matemáticas formales y física computacional de plasmas. Gorard, CEO de Lanyon AI, trabajó previamente en demostración automática de teoremas y computación cuántica en Wolfram Research y cofundó el Wolfram Physics Project con Stephen Wolfram. Hakim, CTO de Lanyon AI, es docente en Princeton y físico investigador principal cuyo trabajo incluye fusión, plasmas espaciales, turbulencia en tokamaks y aprendizaje automático para ecuaciones diferenciales parciales. Juno, el científico en jefe, es investigador del Princeton Plasma Physics Laboratory y desarrollador principal del marco de simulación de plasmas Gkeyll.
Su apuesta es que los agentes de codificación de propósito general parten del lenguaje equivocado. "¿Por qué los agentes siguen razonando y programando en lenguas humanas imperfectas?" preguntó Gorard en el anuncio del 17 de agosto. En su lugar, Lanyon AI quiere que su agente razone mediante un lenguaje formal condensado construido para matemáticas, física y computación científica.
One source for the code and the proof
La arquitectura de Lanyon AI asigna el trabajo creativo a un modelo de lenguaje subyacente, que propone una especificación formal en el lenguaje específico del dominio de Lanyon AI. Un compilador simbólico luego expande esa especificación en código de implementación y en una prueba verificable por máquina al mismo tiempo. Si la especificación no puede ser probada, Lanyon AI dice que el sistema retiene el código y vuelve a intentarlo.
Ese diseño apunta a una debilidad específica en los sistemas de autoformalización. Un agente convencional puede escribir código y luego producir una prueba en Lean que pasa la verificación de tipos mientras describe una implementación distinta. Lanyon AI llama a esa falla "misformalización". Derivar ambos artefactos desde una sola fuente pretende evitar que la prueba se aleje del código que supuestamente certifica.
La evidencia más sólida disponible hasta ahora proviene del propio Lanyon AI. En pruebas comparativas realizadas por la compañía publicadas en julio, Juno probó modelos de vanguardia en solucionadores de advección lineal y ecuaciones de Maxwell, usando tres ensayos para cada modelo e indicaciones detalladas y concisas. Lanyon AI reportó que su solucionador de advección lineal de referencia tardó alrededor de siete segundos y unos 800 tokens de salida para generarse, mientras que su solucionador de Maxwell tardó cerca de 23 segundos y unos 600 tokens.
Esas cifras respaldan una afirmación más limitada que la comparación amplia del anuncio de agosto con modelos de vanguardia. Las pruebas fueron diseñadas, ejecutadas y calificadas por Lanyon AI en torno a problemas científicos que se ajustan a su arquitectura. La replicación independiente aún no ha establecido cómo rinde el enfoque en un conjunto más amplio de trabajos de ingeniería.
Lanyon AI también ha publicado seis repositorios de solucionadores en GitHub, que cubren advección-difusión, ecuaciones de Maxwell, ecuaciones de Maxwell relativistas generales, la ecuación de Burgers, ecuaciones de Euler compresibles y la ecuación electrostática de Vlasov. Los repositorios usan C y Lean, dando a los investigadores ejemplos inspeccionables del trabajo de verificación formal detrás de las afirmaciones de Lanyon AI.
The specification remains the boundary
La verificación formal establece que una implementación se ajusta a una especificación formal. No puede establecer automáticamente que la especificación capture la intención científica real del usuario, las suposiciones físicas o las condiciones de despliegue.
Gorard reconoció ese límite en la introducción de Lanyon AI en julio. Distinguió la garantía sintáctica de que código, pruebas y especificaciones coinciden del problema semántico de traducir la solicitud en lenguaje natural de un usuario a la especificación correcta. Lanyon AI describió la corrección semántica como un área de investigación abierta.
Esa distinción importa en las industrias en las que Lanyon AI está incursionando. Una prueba puede certificar un solucionador dejando sin responder si un ingeniero seleccionó las ecuaciones gobernantes correctas, las condiciones de frontera, las propiedades del material o los umbrales de fallo. El desafío de producto de Lanyon AI está, por lo tanto, concentrado en la interfaz entre el ingeniero y el lenguaje formal. El compilador simbólico solo puede controlar todo lo que viene después una vez que esa interfaz produce la especificación correcta.
El mercado ya está atrayendo a equipos con ambición técnica. Axiomatic AI reveló una ronda semilla de 18 millones de dólares en marzo de 2026 para IA de ingeniería centrada en la verificación, mientras que Harmonic ha concentrado su sistema Aristotle en razonamiento matemático formal y software verificado. Lanyon AI está labrando una posición más cercana a simulaciones ejecutables y métodos numéricos, aprovechando directamente la experiencia de Hakim y Juno en la construcción de software para física de plasmas.
La alineación de inversionistas sigue esa dirección industrial. Dimension describe su mandato como invertir en ciencia y computación. Industrious Ventures se enfoca en aeroespacial, energía, manufactura y otras industrias físicas donde los errores de software chocan con los costos de hardware y los requisitos de seguridad.
Lanyon AI sigue presentando un programa de investigación más que un negocio comercial totalmente documentado. Sus materiales públicos no establecen precios, adopción por parte de clientes ni un lanzamiento general del producto. La página de la compañía está reclutando científicos e ingenieros de investigación en verificación formal, física computacional, matemáticas aplicadas e infraestructura de IA.
Los fundadores han producido una tesis técnica coherente y han expuesto suficiente código como para que partes de ella sean inspeccionables. Su próxima prueba es convertir esa arquitectura en un sistema que los ingenieros puedan usar sin trasladar el error más difícil del código generado a la especificación que lo controla.