@MonniauxD @antoinechambertloir @arthurperret Pour compléter ce que dit David, et faire le lien avec le régime de vérité qui est abordé dans d'autres billets, pour les maths l'horizon actuellement est de coupler les IA génératives à des assistants de preuve (type Lean), ce qui permettrait d'avoir un vérificateur de ces essais-erreurs. Le potentiel d'exploration est énorme. Pour l'instant la pratique des matheux comme mon doctorant est de générer des "preuves papiers en LaTeX" puis de faire nous-même le tri entre l'ivraie des "passages abscons, faux ou inutiles" et le bon grain qui nous permet d'avancer dans les preuves techniques (qui emploient des patterns communs à d'autres preuves figurant dans son corpus de données). François Chollet donne souvent l'image des LLM comme d'un outil nous permettant parfois de pointer dans la bonne direction, sans toutefois tomber dans le mille du premier coup, le tandem avec l'expert rectifiant le tir pour s'approcher progressivement de la cible. Les assistants de preuve pourraient automatiser davantage ce processus en identifiant les étapes qui sont fausses. De même techniquement rien n'interdit que l'on puisse conserver une trace fidèle aux sources, mais il est vrai que pour le moment il nous faut vérifier si les références pointent vers un article existant, ce qui n'est pas un problème pour l'expert. Celui-ci se sert de l'outil comme d'un GPS dans un océan d'articles, parfois il fait fausse route, et parfois il nous fait découvrir des pépites qui étaient passées en dehors de nos radars et qu'une recherche par mot clef dans Google Scholar n'aurait pas décelé.
Donc c'est très utile, le problème est le coût écologique catastrophique.