Ce pourquoi c'est d'après moi juste ridicule d'utiliser un LLM pour commencer, puisque ce sera souvent faux, ou pire: ce sera faux mais aura l'air d'être vrai si on n'est pas extrêmement attentif (bien plus attentif qu'on ne devrait l'être si on devait tout écrire soi-même); et dans tous les cas, on perdra énormément de temps à arriver à l'une ou l'autre des conclusions possibles.
Dans le cas très particulier des démonstrations mathématique, les réponses de chatGPT ne sont pas souvent fausses. Par contre, c'est vrai que quand elle est fausse, c'est presque toujours subtil, et l'erreur ruine généralement l'ensemble de la preuve.
C'est pourquoi je préfère toujours trouver une démonstration dans un cours publié par un humain.
MAIS MAIS MAIS MAIS MAIS ...
Aussi incroyable que cela puisse paraître, il y a des trucs en math qu'on ne trouve pas sur internet. Un des plus gros pavé généré par LLM dans le Frido est toute la partie pour démontrer le théorème de Cauchy-Lipsitz analytique. À ma connaissance, le seul endroit sur internet où on donne la définition d'une application analytique entre espaces de Banach est ce document.
Et ce n'est pas faute d'avoir demandé à des humains:
(zéro réponses, mais les commentaires m'ont convaincu de passer par l'holomorphie, et y'avait encore pas mal de boulot)
tu as déjà fait le premier pas vers la facilité, et c'est vraiment dommage étant donné ton niveau d'implication,
Demander à un LLM n'est pas la facilité. Les démonstrations données dans les cours publiés par les profs sont toujours plus faciles à exploiter que celles données par les LLM—il y a plusieurs raisons à cela, et le fait qu'il y ait moins d'erreurs n'en est pas la principale.
Si les mathématiciens passaient un peu moins de temps à écrire le millième livre "Introduction à l'algèbre linéaire" publié chez un éditeur privateur (qui imprimera 500 exemplaires avant de le remplacer par le livre suivant exactement identique), et un peu plus de temps à publier des notes de cours bien faites, je ne serais pas réduit à demander à des LLM.
En attendant je reprécise mon flux :
j'ai une preuve sur mon écran (pdf, blog, mathoverflow et LLM)
je rédige une preuve complète sur ma feuille de brouillon (à la main, au crayon)
je retranscrit la preuve en LaTeX.
Prétendre que ce flux génère plus d'erreurs en partant d'un LLM que d'ailleurs est une hypothèse possible, mais elle doit être vérifiée empiriquement.
Pour l'instant l'erratum ne contient pas de fautes générées par l'IA.
Si quelqu'un veut aider à prouver le point de la médiocrité des LLM, il suffit de chercher les preuves dont les références contiennent un de ces trois :
BIBooMistral
BIBChatGPT
BIBChatGPTDifficile
Et puis il faudra montrer que la densité de fautes parmi ces résultats est plus importante que parmi les autres.
Mode d'emploi: ag BIBChatGPT retourne des lignes comme:
[^] # Re: J'ai eu un problème similaire avec le Frido (livre de math)
Posté par LaurentClaessens (site web personnel) . En réponse au journal Recrudescence de contributions générées par IA. Évalué à 10.
Dans le cas très particulier des démonstrations mathématique, les réponses de chatGPT ne sont pas souvent fausses. Par contre, c'est vrai que quand elle est fausse, c'est presque toujours subtil, et l'erreur ruine généralement l'ensemble de la preuve.
C'est pourquoi je préfère toujours trouver une démonstration dans un cours publié par un humain.
MAIS MAIS MAIS MAIS MAIS ...
Aussi incroyable que cela puisse paraître, il y a des trucs en math qu'on ne trouve pas sur internet. Un des plus gros pavé généré par LLM dans le Frido est toute la partie pour démontrer le théorème de Cauchy-Lipsitz analytique. À ma connaissance, le seul endroit sur internet où on donne la définition d'une application analytique entre espaces de Banach est ce document.
Et ce n'est pas faute d'avoir demandé à des humains:
https://math.stackexchange.com/questions/5113042/analytic-picard-lindel%c3%b6f-theorem
https://math.stackexchange.com/questions/5101596/analytic-picard-lindel%c3%b6f-theorem
(zéro réponses, mais les commentaires m'ont convaincu de passer par l'holomorphie, et y'avait encore pas mal de boulot)
Demander à un LLM n'est pas la facilité. Les démonstrations données dans les cours publiés par les profs sont toujours plus faciles à exploiter que celles données par les LLM—il y a plusieurs raisons à cela, et le fait qu'il y ait moins d'erreurs n'en est pas la principale.
Si les mathématiciens passaient un peu moins de temps à écrire le millième livre "Introduction à l'algèbre linéaire" publié chez un éditeur privateur (qui imprimera 500 exemplaires avant de le remplacer par le livre suivant exactement identique), et un peu plus de temps à publier des notes de cours bien faites, je ne serais pas réduit à demander à des LLM.
En attendant je reprécise mon flux :
Prétendre que ce flux génère plus d'erreurs en partant d'un LLM que d'ailleurs est une hypothèse possible, mais elle doit être vérifiée empiriquement.
Pour l'instant l'erratum ne contient pas de fautes générées par l'IA.
Si quelqu'un veut aider à prouver le point de la médiocrité des LLM, il suffit de chercher les preuves dont les références contiennent un de ces trois :
Et puis il faudra montrer que la densité de fautes parmi ces résultats est plus importante que parmi les autres.
Mode d'emploi:
ag BIBChatGPTretourne des lignes comme:Ensuite il suffit de faire une recherche du label (
PROPooYTMYooEYxuQc) dans le pdf pour trouver le résultat à vérifier.