Pour pallier le manque de garanties vérifiables concernant la sortie des modèles de langage à grande échelle (LLM), cet article propose une couche de contrat qui exploite les principes de la conception par contrat (DbC) et de la théorie des types. Cette couche de contrat gère toutes les invocations de LLM, spécifie les exigences sémantiques et typologiques des entrées et des sorties, et fournit des corrections probabilistes pour garantir la conformité. Nous présentons le LLM comme un analyseur sémantique à double point de vue et un composant probabiliste de type boîte noire, où la satisfaction du contrat est probabiliste et la vérification sémantique est définie opérationnellement par des conditions spécifiées par le programmeur sur des structures de données bien définies. Plus généralement, nous soutenons que deux agents qui satisfont au même contrat sont fonctionnellement équivalents par rapport à ce contrat.
