Raisonnement automatisé

Le raisonnement automatisé est un domaine de l'informatique et de l'intelligence artificielle, consacré à la conception de systèmes capables de produire de nouvelles informations ou de valider des conclusions à partir de faits et de règles logiques préétablis. Il s'appuie sur des formalismes mathématiques (exemple : logique propositionnelle ; logique du premier ordre…) pour exécuter des démonstrations de théorèmes ou résoudre des problèmes complexes sans intervention humaine constante^[1].

Selon la Stanford Encyclopedia of Philosophy, il « est comparable à la démonstration de théorèmes mécaniques. Construire un programme de raisonnement automatisé signifie fournir un algorithme description à un calcul formel afin qu’il puisse être implémenté sur un ordinateur pour démontrer efficacement les théorèmes du calcul ». Il contribue à mieux comprendre certains aspects du raisonnement, avec pour objectif la création de logiciels et d'algorithmes permettant aux ordinateurs de « raisonner » de manière automatique et autonome ou presque, ce qui en a fait un sous-domaine de l'intelligence artificielle de pointe (modèles frontière), très connecté à l'informatique théorique, voire à la philosophie^[2].

Parmi les sous-domaines les plus développés du raisonnement automatisé figurent l'assistant de preuve (qui, en pratique, est plus pragmatique mais moins automatisé que sa théorie), la démonstration automatique de théorèmes et la vérification de preuve (procédé qui garantit un raisonnement correct en se basant sur l'axiome selon lequel les hypothèses fournies sont justes^{[réf. souhaitée]}).

Plus récemment, le raisonnement continu il a contribué à simplifier l'analyser des systèmes de large échelle^{[réf. souhaitée]}.

D'autres voies explorées sont le raisonnement par analogie, induction et abduction, le raisonnement non-monotone et le raisonnement sous les contraintes de l'incertitude (qui vise l'argumentation, sous des contraintes de minimalité et de cohérence, appliquée au sommet des déductions automatisées.

Les outils et techniques du raisonnement automatisé incluent les logiques et les calculs classiques de la preuve automatique de théorème, mais aussi la logique floue, l'inférence bayésienne, le raisonnement par le principe d'entropie maximale et un grand nombre de techniques ad-hoc moins formelles.

Cette discipline, autrefois théorique, a aujourd'hui des applications concrètes et parfois critiques, par exemple dans la vérification formelle de logiciels, la configuration industrielle et la planification de systèmes autonomes, allant de la programmation automatique à la planification robotique, en passant par la gestion de l’incertitude et l’optimisation.

Dans le premier quart du XXI^e siècle, la recherche en raisonnement automatisé, telle qu’elle apparaît dans les archives de l’AAAI, vise à doter les systèmes informatiques de capacités de déduction, de preuve et de planification comparables à celles mobilisées dans le raisonnement humain. Elle concerne notamment les domaines suivants :

• la démonstration automatique de théorèmes, qui explore des méthodes formelles pour établir la validité logique d’énoncés^[3] ;
• la planification, qui étudie la représentation d’actions, la gestion du temps et la construction de plans dans des environnements dynamiques^[3] ;
• le raisonnement fondé sur des règles ou des contraintes (mobilisant des systèmes de production, des réseaux de contraintes ou des approches probabilistes)^[3] ;
• la recherche heuristique, qui développe des stratégies d’exploration efficaces pour résoudre des problèmes combinatoires^[3] ;
• les systèmes de maintenance de la vérité (Truth Maintenance Systems), destinés à gérer la cohérence des connaissances dans des environnements évolutifs^[3].

Ces recherches sont structurées autour de méthodes logiques, algorithmiques et heuristiques visant à automatiser des formes complexes de raisonnement^[3].

Le système d'Oscar de John Pollock (en) est un exemple d'argumentation automatisée plus spécifique qu'un « simple » assistant de preuve de théorème. L'argumentation formelle est un sous-domaine de l'intelligence artificielle.

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Automated reasoning » (voir la liste des auteurs).

• Ateliers internationaux sur la mise en œuvre des Logiques
• Workshop on Empirically Successful Computerized Reasoning
• Journal of Automated Reasoning

• Ressource relative à la recherche :
  • Stanford Encyclopedia of Philosophy

• Portail de l’intelligence artificielle
• Portail de l'informatique théorique