Comment la logique peut aider les modèles d'IA être plus exacts, selon AWS - ZDNET

Byron Cook, éminent scientifique d'AWS, plaide en faveur du "raisonnement automatisé". Amazon AWS

Le terme "raisonnement" est une métaphore familière dans la technologie de l'intelligence artificielle (IA) d'aujourd'hui. Elle est souvent utilisée pour décrire les résultats parfois très verbeux générés par les modèles d'IA dits de raisonnement tels que o1 d'OpenAI ou R1 de DeepSeek AI.

Mais un autre type de raisonnement prend discrètement racine dans les applications les plus avancées. Et cette approche est peut-être plus proche du raisonnement réel.

Qu'est ce que le raisonnement automatisé ?

Récemment, Byron Cook, éminent scientifique d'Amazon AWS, a plaidé en faveur de ce que l'on appelle le "raisonnement automatisé", également connu sous le nom d'"IA symbolique" ou, de manière plus absconse, de "vérification formelle".

Il s'agit d'un domaine d'étude aussi ancien que celui de l'intelligence artificielle. Et, selon M. Cook, il fusionne rapidement avec l'IA générative pour former un nouvel hybride passionnant, parfois appelé "IA neuro-symbolique". De quoi combiner le meilleur du raisonnement automatisé et des grands modèles de langage.

AWS

M. Cook a donné une conférence sur le raisonnement automatisé lors du AWS Financial Services Symposium qui s'est tenu à New York en mai dernier.

Toute connaissance est rigoureusement étayée par ce qui peut être logiquement affirmé

Quel que soit le nom qu'on lui donne, le raisonnement automatisé fait référence à des algorithmes qui recherchent des déclarations ou des affirmations dont la véracité peut être vérifiée à l'aide de la logique. L'idée est que toute connaissance est rigoureusement étayée par ce qui peut être logiquement affirmé.

Comme le dit Cook, "le raisonnement prend un modèle et nous permet de parler avec précision de toutes les données possibles qu'il peut produire".

M. Cook a donné comme exemple un bref extrait de code qui montre comment le raisonnement automatisé permet d'obtenir cette validation rigoureuse.

La logique plus que les incessants essais et erreurs

Il est possible, dit-il, de prédire avec certitude qu'une boucle d'instructions dans un code informatique cessera de fonctionner à un moment donné, sur la base des conditions établies dans ses déclarations. L'analyse logique permet donc de répondre à la question "Cette boucle peut-elle fonctionner indéfiniment ?

AWS

Dans l'exemple de Cook, deux variables, X et Y, sont des entiers ; ...
[Courte citation de 8% de l'article original]