Hay personas que son tan difíciles de encasillar que ni la extensa creatividad de los cargos protocolarios es capaz de contener su valía. Pongamos el ejemplo de Byron Cook quien, sobre el papel, es vicepresidente y científico distinguido de Amazon Web Services; además de fundador y líder del Automated Reasoning Group (ARG). Es obvio que esa consideración es bastante vaga y genérica, para un investigador e intelectual cuya aventura vital pasa por el desarrollo de modelos matemáticos muy alejados de la moda del momento.

Cook es viejo conocido de Microsoft y también del University College London. Su disciplina de origen, el razonamiento formal, se ha dedicado históricamente a demostrar teoremas y verificar la corrección absoluta de sistemas críticos. Hoy, sin embargo, su campo de estudio se ha convertido en la pieza faltante del puzle más complejo de la computación moderna: cómo confiar en unas máquinas que, por diseño, alucinan.

En ese sentido, Cook plantea el fin de la dicotomía histórica entre las dos grandes fuerzas de la IA: la estadística (representada por el deep learning y los modelos bayesianos) y la lógica (basada en reglas y símbolos).

“En el mundo de la IA hay diferentes ramas. Yo soy de la lógica, pero ahora existe un interés creciente en la IA neurosimbólica, que es básicamente la combinación de la visión simbólica y la cognitiva”, explica en entrevista con DISRUPTORES - EL ESPAÑOL. Y es que, dice el científico, la era de la fuerza bruta estadística está dando paso a una etapa de hibridación, donde la flexibilidad creativa de las redes neuronales se somete al rigor binario de las matemáticas.

¿Puede traducirse esa convergencia técnica con una analogía culinaria? Si nuestro interlocutor es un ‘científico distinguido’, todo es posible. Cook habla del efecto “chocolate y mantequilla de cacahuete”, donde la mezcla supera a los ingredientes por separado. Así pues, el problema histórico de la verificación formal siempre fue la barrera humana: escribir las especificaciones matemáticas necesarias para probar que un software es correcto resulta extremadamente difícil y costoso.

“Tradicionalmente, teníamos herramientas de razonamiento increíbles, pero necesitábamos que alguien definiera qué quería probar. Esa es, con diferencia, la parte más difícil”, admite el investigador. Empero, justo ahí, la IA generativa ha demostrado ser sorprendentemente hábil leyendo documentación y redactando borradores de formalización lógica. No son perfectos, pero rompen la barrera de entrada.

“Puedes pedirle a la IA que lea documentos y formule una formalización en lógica temporal”, detalla. A partir de ahí, los motores de razonamiento formal toman el relevo para validar matemáticamente si esa especificación se cumple o no.

Cambiar cómo ‘piensa’ la IA

Esta visión va más allá de corregir errores; está cambiando la forma en que las propias inteligencias artificiales “piensan”. En esta línea, Byron Cook señala una tendencia fascinante en el entrenamiento de modelos fundacionales: el uso de asistentes de demostración matemática (theorem provers) como fuente de datos.

“Un enfoque muy popular actualmente es entrenar modelos de lenguaje sobre los outputs de asistentes de demostración como Lean, una herramienta muy popular entre matemáticos como Terence Tao”, revela el científico.

La industria ha descubierto un fenómeno de transferencia de aprendizaje (transfer learning): cuando un modelo se entrena leyendo y generando pruebas matemáticas rigurosas, mejora su capacidad de razonamiento general en tareas que no tienen nada que ver con las matemáticas.

“Se vuelven más lógicos; son mejores diseñando recetas o razonando si han sido entrenados sobre lógica matemática probada”. Esto permite generar “cantidades ilimitadas de datos de alta calidad”, rompiendo la dependencia de los datos humanos escasos y cada vez más limitados.

Rigidez para ser flexibles

En el plano de la ingeniería de software, esta visión neurosimbólica ha encontrado un aliado inesperado en el lenguaje de programación Rust. Según Cook, la rigidez del sistema de tipos de Rust actúa como un carril guía para la creatividad desbordada de la IA generativa.

“Rust es básicamente una separación de la lógica dentro del sistema de tipos”, argumenta a este periodista. “A las herramientas de IA les gusta mucho usar Rust porque los mensajes de error son un enfoque más estático y preciso”. Esto crea un bucle de retroalimentación en tiempo real: el modelo genera código, el compilador (la lógica) le devuelve un error específico, y el modelo aprende y corrige.

“La herramienta de IA puede ver el error y volver a intentarlo. Hay un feedback neurosimbólico que no sería posible si usaran una disciplina de tipado débil como C”.

Este ciclo permite una nueva metodología de desarrollo desatendido. Llegado el caso, los ingenieros pueden incluso delegar tareas complejas a la inteligencia artificial, irse a una reunión y volver con el trabajo no solo hecho, sino “probado y con un mejor trabajo de validación del que un humano podría haber hecho”.

Hacia la IA agéntica

La urgencia de esta arquitectura híbrida se dispara con la llegada de la IA agéntica (sistemas que ejecutan acciones autónomas). Cook advierte que no se puede confiar en la probabilidad cuando un agente mueve dinero o gestiona infraestructuras críticas. La solución técnica que propone es el uso de lenguajes de políticas verificables para definir los límites del terreno de juego.

“Podemos razonar sobre la composición de los agentes”, explica Cook sobre la visión de futuro. “Puedes tomar múltiples agentes y deducir: 'Colectivamente, dado que están haciendo estas cosas, estas son las cosas malas que no pueden ocurrir'". Se trata de convertir la gobernanza ética y operativa en una propiedad matemática computable, asegurando que los sistemas autónomos operen dentro de una “zona de verdad” inquebrantable.

A pesar de estos avances, Cook no peca de excesos ni de optimismos exacerbados. Recuerda que la verificación formal no es magia, pues siempre depende de axiomas que deben asumirse como ciertos y que la gran batalla pendiente es la “brecha semántica”: la dificultad de traducir la ambigüedad del lenguaje humano a una verdad matemática.

“La sociedad está empezando a entender qué es la noción de verdad”, concluye.