[Stanford CS146S #9] TDD autonome & Vérification formelle : Solveurs SMT Z3, invariants basés sur les propriétés et preuves mathématiques pour le code IA
· 2 minutes de lecture
Bienvenue dans le neuvième volet de notre analyse technique du cours Stanford CS146S : The Modern Software Developer.
Dans ce Cours 9, le programme de Stanford aborde l'ultime frontière de l'ingénierie IA : Comment faire confiance à des modèles de langage stochastiques pour écrire du code ultra-critique sans aucun défaut dans la finance, l'aérospatiale ou la cryptographie ?
Comme le formulait le pionnier Edsger Dijkstra il y a 50 ans : « Les tests de programmes peuvent montrer la présence de bugs, mais jamais leur absence ! » Ce cours détaille la transition des tests d'exemples classiques vers le Property-Based Testing (PBT), l'exécution symbolique et la vérification formelle via le solveur SMT Z3.