Qu'est-ce que le raisonnement automatisé ?
Le raisonnement automatisé est le domaine de l'informatique qui tente de fournir des garanties sur ce qu'un système ou un programme fera ou ne fera jamais. Cette assurance est basée sur des preuves mathématiques. Les gens résolvent de nombreux problèmes logiques en mathématiques, en sciences et en calcul en utilisant des stratégies logiques telles que des théorèmes et des déductions. Le raisonnement automatisé utilise des ordinateurs qui utilisent les mêmes outils pour résoudre des problèmes complexes. Les outils de raisonnement automatisé tentent de répondre à des questions concernant un programme (ou une formule logique) en utilisant des techniques mathématiques connues. Les outils vous aident à confirmer la véracité d'une déclaration ou d'une expression.
Quels problèmes le raisonnement automatisé peut-il résoudre ?
Les scientifiques et les développeurs de logiciels utilisent le raisonnement automatisé pour prouver deux choses. Tout d'abord, ils prouvent que la conception ou la mise en œuvre d'un système respecte ses spécifications. Ensuite, ils prouvent qu'il fonctionne comme prévu.
Pour ce faire, le raisonnement automatisé produit des preuves en logique formelle étayées par des théorèmes mathématiques ou des vérités connues. Le raisonnement automatisé utilise des méthodes de vérification algorithmique basées sur des mathématiques et la logique pour produire des preuves de sécurité ou d'exactitude pour tous les comportements possibles.
Le raisonnement automatisé peut également être utilisé pour prouver que les systèmes utilisés pour configurer les réseaux, autoriser l'accès au réseau ou accorder des autorisations, ou pour préserver la confidentialité et la sécurité des données fonctionnent comme prévu.
Lorsque vous utilisez le raisonnement automatisé, vous présentez d'abord au système un énoncé du problème. Ensuite, le système de raisonnement automatisé calcule et valide les hypothèses à l'aide de l'énoncé du problème. Le logiciel le fait jusqu'à ce qu'il ait épuisé toutes les options.
Exemple de problème pour le raisonnement automatisé
Pour mieux comprendre le raisonnement automatisé, considérez l'énoncé du problème Les chats vivent-ils sur terre ? et les assertions suivantes :
- Les chats sont des mammifères
- Les mammifères vivent sur terre
Le système de raisonnement automatisé évalue si l'énoncé du problème est vrai. Plus précisément, il utilise la déduction logique. Dans ce cas, les chats sont des mammifères et les mammifères vivent sur terre. Cela permettrait donc de vérifier que les chats vivent sur terre.
Limites du raisonnement automatisé
Le raisonnement automatisé ne permet pas de faire des prédictions ou des généralisations. Par exemple, nous pouvons utiliser un raisonnement automatisé pour présenter un argument comme celui-ci :
- Les chats ont des poils
- Fluffy est un chat
- Donc Fluffy a des poils
Nous ne pouvons pas utiliser le raisonnement automatisé pour présenter des arguments comme celui-ci :
- Les chats sont des mammifères
- Les chats vivent sur terre
- Donc, tous les mammifères vivent sur terre
De telles applications sont courantes dans un démonstrateur de théorèmes, qui nécessite des conseils humains lors de l'exécution de tâches de raisonnement déductif.
Quels sont les cas d'utilisation du raisonnement automatisé ?
La capacité du raisonnement automatisé à faire des inférences logiques étape par étape est utile dans plusieurs domaines. En utilisant le raisonnement automatisé, vous pouvez prouver les propriétés de sécurité, de conformité, de disponibilité, de durabilité et de sûreté des architectures à grande échelle.
Voici d'autres cas d'utilisation du raisonnement automatisé.
Modèle mathématique
Les scientifiques, les ingénieurs et les mathématiciens résolvent des problèmes et vérifient des preuves mathématiques en appliquant des formules algébriques à des applications scientifiques. Dans de telles pratiques, ils utilisent des modèles mathématiques qui s'appuient sur plusieurs variables pour déduire des solutions probables à un problème.
Vérification du matériel
Le raisonnement automatisé aide les ingénieurs matériels à créer des produits fiables. Cela leur permet de découvrir des failles potentielles négligées par les méthodes de test classiques.
Par exemple, les ingénieurs de conception électronique utilisent des analyses de raisonnement mathématique automatisées rigoureuses pour obtenir des preuves qu'une conception matérielle particulière répond à ses spécifications, telles que les comportements ou les exécutions du système.
La vérification montre que tous les comportements possibles du système satisfont aux propriétés temporelles qui constituent la spécification. Cela pourrait également montrer que chaque comportement possible de l'implémentation du système est cohérent avec certains comportements de ses spécifications de haut niveau.
Validation logicielle
Les développeurs de logiciels utilisent le raisonnement automatisé pour s'assurer que les applications sont robustes face aux problèmes de sécurité indésirables et que les logiciels fonctionnent comme prévu ou conçu. À l'instar de la vérification matérielle, le raisonnement automatisé permet aux développeurs de valider les mesures de sécurité des logiciels par rapport à différentes politiques.
Par exemple, les ingénieurs d'Amazon Web Services (AWS) prouvent que le code de démarrage est sécurisé pour chaque configuration de démarrage grâce à un raisonnement automatisé. Un autre exemple est qu'ils prouvent que les données stockées et traitées sur Amazon Simple Storage Service (Amazon S3) sont protégées. Dans cet exemple, ils s'appuient sur un raisonnement automatisé pour la réplication, la cohérence, l'autoscaling, l'équilibrage de charge et d'autres tâches de coordination.
Modélisation du raisonnement humain
Les informaticiens utilisent des technologies de raisonnement automatisé pour configurer l'accès. Pour ce faire, ils rédigent des politiques qui décrivent quand autoriser et refuser les demandes d'accès à une ressource par les utilisateurs. Cela permet de vérifier que seuls les utilisateurs concernés ont accès à la ressource, ce qui est important pour la sécurité et la confidentialité de la ressource.
Par exemple, les informaticiens utilisent des formules de la théorie des modulos de satisfaction (SMT) et des solveurs SMT pour prouver les propriétés de sécurité.
Quels sont les outils et techniques de raisonnement automatisés ?
Ensuite, nous partageons plusieurs méthodes de déduction automatisées qui permettent aux systèmes informatiques d'effectuer une déduction humaine.
Logique classique
La logique classique est une philosophie mathématique qui fournit des modèles de raisonnement de base pour les programmes de raisonnement logique automatisés. Cette logique repose sur le principe selon lequel chaque proposition a une valeur de vérité qui est vraie ou fausse, mais pas les deux.
Elle se concentre principalement sur la logique de premier ordre, qui permet aux mathématiciens de représenter des variables inconnues comme x avec des quantificateurs comme il existe dans une phrase. Par exemple, des scientifiques appliquent la logique classique à la programmation logique pour trouver x dans cette phrase : Il existe x tel que x vit sur terre, et x est un mammifère.
Logique propositionnelle
La logique propositionnelle est un système logique dans lequel certaines propositions peuvent être vraies ou fausses et la construction de relations entre elles, appelées arguments.
L'énoncé classique d'un argument en logique propositionnelle est Si P, alors Q. Par exemple, si c'est samedi, c'est le week-end.
Le raisonnement automatisé utilise une technique appelée résolution SAT. Il utilise des outils appelés solveurs SAT pour rechercher des assignations satisfaisantes aux arguments dans la logique propositionnelle. Cela signifie des variables qui rendent l'argument vrai.
Quelle est la différence entre le raisonnement automatisé et l'intelligence artificielle ?
Le raisonnement automatisé est une discipline spécifique de l'intelligence artificielle (IA) qui applique la déduction logique aux systèmes informatiques.
L'IA est une science qui apprend aux ordinateurs à penser comme des humains lorsqu'ils résolvent des problèmes. Les récents développements de l'IA ont conduit à l'avancement de diverses sous-disciplines, notamment le deep learning, l'analyse de données et le machine learning.
Le raisonnement automatisé diffère des autres technologies d'IA, telles que le traitement du langage naturel (NLP), qui vise à entraîner les ordinateurs à comprendre des discours écrits ou verbaux. Le raisonnement automatisé utilise plutôt des modèles logiques et des preuves pour raisonner sur les comportements possibles d'un système ou d'un programme, y compris les états qu'il peut ou n'atteindra jamais.
Quelle est la différence entre le raisonnement automatisé et le deep learning ?
Le raisonnement automatisé prouve les propriétés d'un programme ou d'un système. Il utilise le programme ou le système lui-même, ainsi qu'un modèle ou une spécification du système en logique formelle.
Le deep learning permet d'établir des prévisions en appliquant des modèles statistiques à de grands jeux de données.
Le deep learning est une technologie avancée de machine learning qui simule le fonctionnement du cerveau humain. Il utilise différents modèles de réseaux neuronaux composés de plusieurs couches de neurones qui extraient, comparent et analysent les informations pertinentes. Les scientifiques des données utilisent le deep learning pour des applications complexes, telles que le traitement des données des caméras et des capteurs dans les voitures autonomes.
Le raisonnement automatisé est-il du machine learning ?
Le raisonnement automatisé et le machine learning sont deux choses différentes. En bref, le machine learning réalise des prédictions et des inférences. Le raisonnement automatisé fournit des preuves.
Le machine learning est un sous-ensemble de l'IA qui entraîne les ordinateurs à prendre des décisions avec de grands échantillons de données. Par exemple, les scientifiques des données utilisent le machine learning pour former les logiciels bancaires à identifier les activités frauduleuses. Ils utilisent de grands échantillons de données financières pour s'assurer que le logiciel identifie facilement les modèles anormaux sur la base des résultats obtenus précédemment.
Au lieu d'entraîner le modèle à l'aide de données, le raisonnement automatisé permet au modèle de déduire un résultat basé sur la vérité et la preuve mathématiques.
Comment AWS utilise-t-il le raisonnement automatisé pour améliorer ses offres de services ?
AWS utilise le raisonnement automatisé pour améliorer plusieurs offres de services. Nous en donnons quelques exemples ci-dessous :
- Amazon CodeGuru Reviewer utilise le raisonnement automatisé et le machine learning pour aider les développeurs à identifier les vulnérabilités des logiciels.
- Amazon Inspector Classic dispose d'une fonctionnalité d'accessibilité réseau qui analyse automatiquement vos instances EC2 pour détecter d'éventuelles failles de sécurité et erreurs de configuration.
- L’analyseur d’accès AWS Identity and Access Management (IAM) gère les autorisations des comptes à l’aide d’un raisonnement automatisé.
- L'analyseur d'accessibilité Amazon Virtual Private Cloud (Amazon VPC) applique un raisonnement automatisé pour vous aider à comprendre et à visualiser votre réseau AWS.
Consultez Provable Security pour en savoir plus sur le raisonnement automatisé dans les services AWS. Nous utilisons un raisonnement mathématique pour fournir de solides garanties de sécurité pour vos charges de travail de sécurité.
Apprenez-en plus sur la sécurité sur AWS en créant un compte dès aujourd'hui.
Étapes suivantes sur AWS
