L'alignement ne suffira jamais.

Pour les modèles de langage, l'alignement est l'entraînement qui suit le pré-entraînement : ajustement sur des instructions, puis apprentissage par renforcement à partir de retours humains ou d'autres modèles (RLHF, DPO et leurs variantes).^{1, 2} Le modèle est récompensé pour les réponses que les évaluateurs préfèrent : utiles, polies, conformes aux règles qu'on lui a données. C'est ce qui a fait de simples prédicteurs de texte des assistants utilisables, et cela continue de progresser.

Mais l'alignement agit sur des tendances, pas sur des réponses individuelles. Il rend une bonne réponse plus probable sans dire si celle-ci est juste. Et comme les évaluateurs récompensent les réponses qui ont l'air justes, un modèle peut apprendre à paraître sûr de lui, ou à donner raison à la personne qui demande, quand il ne le devrait pas : c'est ce qu'on appelle la complaisance (sycophancy).³ Un modèle bien aligné est plus agréable à utiliser, et il ne peut toujours pas montrer qu'un chiffre est juste.

La confiance ne fonctionne nulle part ailleurs de cette façon. Nous ne faisons pas confiance à un service comptable parce que son personnel est bien formé, mais grâce à des procédures : l'audit, la double signature, des comptes qui doivent tomber juste.

À grande échelle, la confiance repose sur la possibilité de vérifier, pas sur la qualité de l'entraînement d'un système.

Le langage naturel est notre façon de penser à voix haute, et il est ambigu par nature. Chaque fois que les enjeux ont monté, les humains ont construit par-dessus quelque chose de plus strict. Les nombres et la comptabilité, pour qu'une dette signifie la même chose pour les deux parties. L'algèbre, pour qu'un résultat puisse être retrouvé par quelqu'un qui ne fait pas confiance à son auteur. Le droit écrit, la logique, la preuve, et plus tard les langages de programmation.

Aucun de ces systèmes n'a remplacé l'intuition. Un mathématicien devine toujours le théorème avant de le démontrer. Ce que les systèmes formels nous ont donné, c'est une façon de communiquer sans avoir à être cru : le raisonnement voyage avec la conclusion, et un inconnu peut le vérifier.

Les modèles de langage en sont là où nous en étions avant ce pas. Éloquents, rapides, souvent justes, et sans moyen de transmettre leur raisonnement sous une forme que quiconque puisse vérifier.

Les systèmes formels sont la façon dont les humains communiquent sans avoir à être crus.

Voilà ce que nous entendons par IA neuro-symbolique. La partie neuronale fait ce qu'elle sait faire : comprendre une question posée avec des mots ordinaires, dans le contexte d'un métier. La partie symbolique fait ce que le langage ne peut pas : elle énonce la réponse sous forme de règle, que l'on peut lire, vérifier, rejouer et comparer.

La couche formelle donne à la machine l'instrument que les humains ont construit pour eux-mêmes. Un modèle qui écrit une règle dans un langage logique doit s'engager : sur les commandes qui comptent, sur la période, sur la colonne. Cet engagement peut alors être contrôlé par un vérificateur, par les données, et par la personne qui répond du chiffre.

Une règle, elle, est durable. Un paragraphe d'explication généré disparaît avec la conversation. Une règle est conservée, nommée, et l'on bâtit dessus, comme les mathématiciens le font d'un lemme : un petit résultat démontré, gardé pour que de plus grands raisonnements s'y appuient. Conservée dans git, aussi, pour que l'histoire du raisonnement d'une entreprise s'audite comme celle de son code : qui a décidé quoi, et quand.

Le modèle traduit. La couche formelle raisonne. C'est ce qui rend le raisonnement auditable.

Ils progresseront, et c'est l'argument le plus fort en faveur d'une couche formelle. Un modèle plus capable se voit confier des tâches plus larges et plus d'autonomie, et il produit plus de conclusions que quiconque ne peut en relire. L'écart entre ce qu'un modèle peut produire et ce qu'une personne peut contrôler se creuse à chaque génération.

La relecture de l'explication du modèle est le premier contrôle à cesser de fonctionner. Quand un système raisonne mieux que la personne qui le relit, celle-ci ne peut plus distinguer un argument juste d'un argument convaincant. Les seuls contrôles qui suivent sont ceux qui ne dépendent pas de l'intelligence du contrôleur : un vérificateur qui applique des règles fixes, une requête exécutée sur les données, un contre-exemple qui existe ou n'existe pas.

Les mathématiques sont déjà passées par là. La preuve du théorème des quatre couleurs donnée par Appel et Haken en 1976 reposait sur des calculs informatiques trop longs pour être vérifiés à la main. En 2005, Georges Gonthier et Benjamin Werner l'ont vérifiée formellement avec l'assistant de preuve Coq, si bien qu'il ne reste qu'à faire confiance au petit noyau de Coq.⁴ Samuel Ferguson et Thomas Hales ont démontré la conjecture de Kepler en 1998, mais la preuve complète n'a été publiée qu'en 2006, faute pour les rapporteurs de pouvoir en vérifier la partie informatique. Le projet Flyspeck l'a ensuite vérifiée formellement avec les assistants de preuve HOL Light et Isabelle, et ces vérifications se sont achevées en 2014.⁵ À mesure que les preuves dépassaient ce que l'on pouvait lire, la vérification formelle est devenue plus importante.

Vérifier coûte aussi moins cher que trouver. Un vérificateur n'a pas besoin d'être aussi habile que le modèle : il lui suffit de confirmer, étape par étape, ce que le modèle affirme. Un modèle plus intelligent n'entre donc pas en concurrence avec la couche formelle. Il écrit de meilleures règles, plus vite, et la couche fait de chacune un résultat sur lequel tout le monde peut s'appuyer.

Plus le modèle est capable, plus son travail a besoin d'un contrôle qui ne suppose pas de lui faire confiance.

Qu'un second modèle puisse juger le premier. C'est un avis de plus, avec les mêmes faiblesses. La vérification doit venir de quelque chose d'une autre nature que ce qui est vérifié.

Que des garde-fous ajoutés après coup suffisent. Filtrer ce qu'un modèle a dit n'est pas contraindre ce qu'il peut affirmer. Le contrôle doit avoir lieu avant que la réponse soit donnée.

À des entreprises dont la connaissance n'est plus dispersée entre des têtes, des tableaux de bord et des documents qui se contredisent, mais écrite une fois, en définitions qui s'exécutent. À des agents qui partagent une mémoire faite de règles vérifiées, et que l'on remplace sans perdre ce qui a été appris. À une IA que l'on adopte comme tout instrument sérieux : parce que l'on voit comment elle arrive à son résultat.

Nous construisons les pièces de cette couche au grand jour, et le produit qui les met au travail.