La alineación nunca será suficiente.

En los modelos de lenguaje, la alineación es el entrenamiento que sigue al preentrenamiento: ajuste por instrucciones y, después, aprendizaje por refuerzo a partir de retroalimentación humana o de IA (RLHF, DPO y sus variantes).^{1, 2} Se recompensa al modelo por las respuestas que prefieren los evaluadores: útiles, corteses y dentro de las reglas que se le dieron. Es lo que convirtió simples predictores de texto en asistentes utilizables, y sigue mejorando.

Pero la alineación actúa sobre tendencias, no sobre respuestas concretas. Hace más probable una buena respuesta sin decirle si esta en particular es correcta. Y como los evaluadores recompensan las respuestas que parecen correctas, un modelo puede aprender a mostrarse seguro, o a dar la razón a quien pregunta, cuando no debería: es el problema conocido como complacencia (sycophancy).³ Un modelo bien alineado es más agradable de usar, pero sigue sin poder demostrar que una cifra es correcta.

La confianza no funciona así en ningún otro ámbito. No confiamos en un departamento de contabilidad porque su personal esté bien formado, sino por sus procedimientos: la auditoría, la segunda firma, unas cuentas que tienen que cuadrar.

La confianza a gran escala se basa en poder comprobar, no en lo bien que se haya entrenado un sistema.

El lenguaje natural es la forma en que pensamos en voz alta, y es ambiguo por naturaleza. Cada vez que aumentaba lo que estaba en juego, las personas construían algo más estricto por encima. Los números y la contabilidad, para que una deuda significara lo mismo para ambas partes. El álgebra, para que alguien que no confiaba en el autor de un resultado pudiera volver a obtenerlo. El derecho escrito, la lógica, la demostración y, finalmente, los lenguajes de programación.

Ninguno de ellos sustituyó a la intuición. Un matemático sigue intuyendo el teorema antes de demostrarlo. Lo que nos dieron los sistemas formales es una manera de comunicarnos sin necesidad de que nos crean: el razonamiento acompaña a la conclusión, y un desconocido puede comprobarlo.

Los modelos de lenguaje están en la situación en la que estábamos nosotros antes de ese paso. Fluidos, rápidos, a menudo acertados, y sin ningún medio para transmitir su razonamiento de una forma que cualquiera pueda verificar.

Los sistemas formales permiten a las personas comunicarse sin necesidad de que se las crea.

Esto es lo que entendemos por IA neurosimbólica. La parte neuronal hace lo que sabe hacer bien: entender una pregunta formulada con palabras corrientes, en el contexto de un negocio. La parte simbólica hace lo que el lenguaje no puede: enuncia la respuesta como una regla que se puede leer, verificar, volver a ejecutar y comparar.

La capa formal da a la máquina el instrumento que las personas construyeron para sí mismas. Un modelo que escribe una regla en un lenguaje lógico tiene que comprometerse: qué pedidos cuentan, en qué periodo, sobre qué columna. Ese compromiso puede comprobarlo después un verificador, los datos y la persona responsable de la cifra.

Una regla, además, perdura. Un párrafo de explicación generada desaparece con la conversación. Una regla se conserva, recibe un nombre y sirve de base para otras, igual que los matemáticos conservan un lema: un resultado pequeño que se guarda para que argumentos mayores puedan apoyarse en él. Y se conserva en git, de modo que el historial del razonamiento de una empresa puede auditarse como el historial de su código: quién decidió qué, y cuándo.

El modelo traduce. La capa formal razona. Eso es lo que hace auditable el razonamiento.

Lo serán, y ese es el argumento más sólido a favor de una capa formal. A un modelo más capaz se le confían tareas más amplias y más autonomía, y produce más conclusiones de las que nadie puede revisar leyéndolas. La distancia entre lo que un modelo puede producir y lo que una persona puede comprobar crece con cada generación.

Leer la explicación del modelo es la primera comprobación que deja de funcionar. Cuando un sistema razona mejor que la persona que lo revisa, esa persona ya no puede distinguir un argumento sólido de uno convincente. Las únicas comprobaciones que siguen el ritmo son las que no dependen de la inteligencia de quien comprueba: un verificador que aplica reglas fijas, una consulta que se ejecuta sobre los datos, un contraejemplo que existe o no existe.

Las matemáticas ya han pasado por esto. La demostración del teorema de los cuatro colores de Appel y Haken, de 1976, se basaba en cálculos por ordenador demasiado largos para comprobarlos a mano. En 2005, Georges Gonthier y Benjamin Werner la verificaron formalmente en el asistente de demostración Coq, de modo que solo hay que confiar en el pequeño núcleo de Coq.⁴ Samuel Ferguson y Thomas Hales demostraron la conjetura de Kepler en 1998, pero la demostración completa no se publicó hasta 2006, porque sus revisores no podían verificar la parte informática. El proyecto Flyspeck la verificó después formalmente en los asistentes de demostración HOL Light e Isabelle, y sus comprobaciones concluyeron en 2014.⁵ A medida que las demostraciones superaban lo que las personas podían leer, la verificación formal fue ganando importancia.

Comprobar también es más barato que encontrar. Un verificador no necesita ser tan inteligente como el modelo; solo tiene que confirmar, paso a paso, lo que el modelo afirma. Por eso, un modelo más inteligente no compite con la capa formal. Escribe mejores reglas, más deprisa, y la capa convierte cada una de ellas en un resultado en el que cualquiera puede confiar.

Cuanto más capaz es el modelo, más necesita su trabajo una comprobación que no dependa de confiar en él.

Que un segundo modelo pueda juzgar al primero. Es una opinión más, con los mismos puntos débiles. La verificación tiene que venir de algo de naturaleza distinta a lo que se verifica.

Que basten las salvaguardas añadidas a posteriori. Filtrar lo que ha dicho un modelo no equivale a limitar lo que puede afirmar. La comprobación tiene que hacerse antes de dar la respuesta.

A empresas cuyo conocimiento ya no está disperso entre personas, cuadros de mando y documentos que se contradicen, sino escrito una sola vez como definiciones que se ejecutan. A agentes que comparten una memoria hecha de reglas verificadas y que pueden sustituirse sin perder lo aprendido. A una IA que se adopta como cualquier instrumento serio: porque se puede ver cómo llega a su resultado.

Estamos construyendo las piezas de esa capa en abierto, junto con el producto que las pone a trabajar.