J'aime bien le grand écart entre ces tendances plus ou moins antagonistes
Ces tendances ne sont pas antagonistes et peuvent parfaitement coopérer. Ce qui m'a gêné dernièrement, c'est plus ceux qui s'emballent sur les succès récents de la technologie des LLM. Mais combiner des LLM avec des méthodes formelles comme la vérification ou la recherche automatique de preuves, cela se fait : Imandra, par exemple.
Sur l'emballement au sujet des LLM et des machines soit disant intelligentes, cela me rappelle une anecdote. Il y a 20 ans, ma compagne de l'époque était journaliste et utilisait du speech-to-text (algorithmique que l'on retrouve dans l'apprentissage automatique) pour l'aider à retranscrire ses interviews enregistrés sur dictaphone.. Un jour j'essaye de lui expliquer que l'on peut programmer un ordinateur pour qu'il est 20 au bac S en maths (on sait faire ça depuis longtemps via les approches formelles) : elle n'a jamais voulu me croire ! Une machine ne pouvait pas être aussi « intelligente » pour elle (le fait qu'elle utilise du speech-to-text me faisait rire intérieurement ;-). Je me demande bien ce qu'elle pense aujourd'hui d'un logiciel comme ChatGPT.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reproductibilité, vérifiabilité et musiciens de Brême
Posté par kantien . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2.
Ces tendances ne sont pas antagonistes et peuvent parfaitement coopérer. Ce qui m'a gêné dernièrement, c'est plus ceux qui s'emballent sur les succès récents de la technologie des LLM. Mais combiner des LLM avec des méthodes formelles comme la vérification ou la recherche automatique de preuves, cela se fait : Imandra, par exemple.
Sur l'emballement au sujet des LLM et des machines soit disant intelligentes, cela me rappelle une anecdote. Il y a 20 ans, ma compagne de l'époque était journaliste et utilisait du speech-to-text (algorithmique que l'on retrouve dans l'apprentissage automatique) pour l'aider à retranscrire ses interviews enregistrés sur dictaphone.. Un jour j'essaye de lui expliquer que l'on peut programmer un ordinateur pour qu'il est 20 au bac S en maths (on sait faire ça depuis longtemps via les approches formelles) : elle n'a jamais voulu me croire ! Une machine ne pouvait pas être aussi « intelligente » pour elle (le fait qu'elle utilise du speech-to-text me faisait rire intérieurement ;-). Je me demande bien ce qu'elle pense aujourd'hui d'un logiciel comme ChatGPT.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.