AutoIP formalise la régularisation linéaire avec Lean

LLéna

Des chercheurs présentent AutoIP, une bibliothèque Lean dans laquelle des agents d’intelligence artificielle ont formalisé automatiquement la théorie classique de la régularisation linéaire et les éléments d’analyse fonctionnelle sur lesquels elle repose, selon arXiv. Le projet porte donc à la fois sur la formalisation d’une théorie mathématique et sur les outils d’analyse nécessaires à cette théorie, avec des énoncés et des preuves traduits dans le langage que Lean peut vérifier. Une preuve vérifiée par machine certifie uniquement l’énoncé formel qu’elle démontre : elle ne garantit pas, à elle seule, que cet énoncé exprime correctement l’intention mathématique des chercheurs. Il reste donc aux humains à contrôler cette correspondance, même lorsque la preuve elle-même a été vérifiée par le système, car la validité de la démonstration formelle et la fidélité de sa traduction sont deux questions distinctes. AutoIP est organisée pour aider à ce contrôle : un relecteur peut comparer les énoncés formels à leurs équivalents en langage naturel, sans devoir lire les preuves elles-mêmes, ce qui concentre la relecture sur le sens des énoncés. D’après l’expérience des auteurs, les risques les plus importants se situent davantage dans les énoncés que dans les preuves, et des tests automatisés simples peuvent contribuer à repérer des problèmes dans ces formulations. Le projet souligne ainsi une limite précise de l’automatisation : la machine peut contrôler qu’une preuve établit bien l’énoncé formel prévu, mais la vérification que cet énoncé correspond aux mathématiques voulues reste une tâche humaine, que la comparaison et les tests peuvent aider à mener.