kantien a écrit 1191 commentaires

Donc tu attribut de l’intelligence aux animaux, les animaux ne sont pas égaux aux humain en droit et tu ne veux pas attribuer de l’intelligence aux car ça demanderait à ce qu’ils aient le même droits que nous ?

Non, je n'attribue pas de raison mais un entendement (intelligence) aux animaux. Néanmoins, la raison étant un entendement qui se prend lui-même pour objet (et non seulement ce qui lui est autre, comme pour les animaux qui déterminent des moyens pour arriver à leur fin, mais qui ne semble pas disposer d'un langage argumentatif), il me paraît normal d'attribuer de la raison à une machine que l'on qualifierai d'intelligente : si l'intelligence émerge d'une fonction calculable (un lambda-terme), elle peut bien se prendre elle-même comme argument. Et partant, pourquoi ne pas lui attribuer les propriétés de la raison telle qu'elle nous apparaît à nous mêmes ?

Cela étant, ce n'est pas que je ne veux pas attribuer les mêmes droits aux machines, mais que ce sera une conséquence nécessaire si je leur reconnais de l'intelligence. Je n'ai pas proposé l'argumentaire suivant : je ne veux pas donner de droits aux machines, or si elle sont intelligentes alors elles auront les mêmes droits, donc elles ne sont pas intelligentes. Mais j'interrogeais les partisans des machines intelligentes, en leur posant cette question : puisque vous les considérer intelligentes, qu'en est-il de leurs droits ? Lorsque l'on pose dogmatiquement un principe (ce que fait le fonctionnalisme), il faut en assumer toutes les conséquences. ;-)

Pour ma part, je ne leur attribue pas d'intelligence pour les raisons évoquées précédemment, donc la question ne me concerne pas vraiment.

Donc oui ils manipulent de la sémantique.

Si tu veux, tout comme un type checker manipule la sémantique du code qu'il type. Mais il ne la comprend pas, cela n'a pas de signification pour lui, c'est là toute la conclusion de Searle avec sa chambre chinoise. Ce que dénote les signes qu'il manipule syntaxiquement, bien que représentant des rapports sémantiques, se trouve en dehors des signes et il ne peut s'en faire aucune représentation.

Mais là encore, c'est le langage que l'on utilise pour décrire le comportement de la machine qui prête à confusion. À strictement parler, la machine ne manipule aucun signe ni aucune sémantique, c'est nous, êtres humains, qui donnons cette interprétation aux états physiques de la machine. Mais la machine, elle même n'est consciente de rien, ni ne cherche à donner un sens à ce qu'elle fait, pas plus que la pascaline ne manipule des chiffres : ce sont des rouages mécaniques qui tournent, nous interprétons leurs positions comme dénotant un nombre et son mécanisme comme effectuant des calculs arithmétiques élémentaires. Pas plus que ton stylo ne manipule des signes et de la sémantique quand tu écris à la main.

Je réitères donc ma question : quel phénomène as-tu observé que tu ne peux expliquer qu'en attribuant de l'intelligence aux machines ? Une discussion avec un agent conversationnel ne relève pas de ce genre de phénomène pour moi. Il ne faut pas prendre une condition suffisante pour une condition nécessaire. Lorsqu'Ysabeau tricote, je n'ai aucun doute sur le fait qu'elle fasse usage de son intelligence. Ce n'est pas pour autant que j'irais attribuer de l'intelligence aux métiers Jacquard ou leur version moderne qui tricote du textile. À ma connaissance, personne ne les a jamais ainsi qualifiés. Alors pourquoi avec un agent conversationnel ? Qu'est-ce qui le différencie d'un métier Jacquard ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Par exemple je vois dans des comportements d'enfants qui ne parlent pas de l'intelligence, mais j'en vois aussi dans des animaux par exemple.

Tout comme moi. Pourquoi crois-tu que j'attribue de l'entendement (mais pas de raison) aux animaux ? Mais ma question était pourquoi veux-tu attribuer cette propriété à une machine construite par l'homme ?

Pas dans le monde dans le quel tu vis. Tu as le droit de l'imaginer, mais venir l'utiliser comme argument c'est ridicule tant que ce n'est pas le cas (bon ça ne le sera jamais donc c'est compliqué). Note que c'était encore moins le cas à l'époque que ton maître à penser.

Je crois que tu manques de culture philosophique et historique. A-t-on avis pourquoi le projet des Lumières a-t-il débouché sur la révolution française et sa Déclaration des droits de l'homme et du citoyen ? Son premier article affirme que Les hommes naissent et demeurent libres et égaux en droits. Pourquoi en-est il ainsi de tous les êtres humains ? Pourquoi seuls les humains sont des sujets de droit ? Pour être sujet de droit, il faut être soumis au principe du devoir (pas de droits sans devoirs). Mais pour concevoir la notion même de devoir être, il faut se penser comme non soumis exclusivement à la nécessité de la nature et son déterminisme, c'est-à-dire être libre. Comme tu as donné plus haut un lien vers une vidéo de Mr Phi, en voici une autre : libre ou determiné.

Les ordinateurs, quant à eux, ont toutes leurs successions d'états soumis au principe de causalité, ce qu'exprime parfaitement la loi de composition des instructions de la logique de Hoare :

{ P } S { Q } , { Q} T { R }
----------------------------
     { P } S ; T { R }

C'est une règle de déduction avec deux prémisses : la première stipule que l'instruction S fait passer la machine de l'état P à l'état Q, et la seconde que l'instruction T la fait passer de l'état Q à l'état R. Sous ces conditions, la règles affirme que l'on peut conclure que la série d'instruction S; T fait passer la machine de l'état P à l'état R.

Lorsque l'on formalise la notion de calcul dans le lambda-calcul typé (programmation fonctionnelle pure, sans effet de bords et donc sans changement d'état), l'analogue de cette règle est celle de la composition de fonction qui a pour type une double application de la règle de déduction logique dite du modus ponens : si P alors Q, or P donc Q. Résultat classique de la correspondance de Curry - Howard.

Et bien tu me croiras si tu veux, mais bien que ces deux logiques (Hoare et Curry-Howard) date de la fin des années 60, le principe qui préside à leur correspondance était déjà noir sur blanc dans la Critique de la raison pure. Comme je ne voudrais pas que tu me crois sur parole, ou que tu penses encore que je me mets à créer des concepts ex nihilo (ce qui n'a jamais était le cas), je te donne la référence tu n'auras qu'à le constater par toi même. Elle se trouve dans la correspondance entre la table logique des jugements et celle des catégories. Tu pourras alors voir que la notion de cause et effet (deuxième catégorie de la relation) de la seconde table a pour corrélat, dans la première, la forme logique des jugements hypothétiques (si A alors B), jugement dont la règle de déduction est le modus ponens susmentionné.

Pour aller plus loin, on pourrait même reprocher à la structure syntaxique de la règle de la logique de Hoare de ne pas mentionner le sujet (logique) de ses propositions, à savoir la machine ! Je propose donc de la reformuler ainsi :

{ M : P } S { M : Q } , { M : Q} T { M : R }
--------------------------------------------
       { M : P } S ; T { M : R }

où une expression de la forme M : P doit s'interpréter comme signifiant la machine M est dans l'état P. Je choisis cette notation à dessein, car c'est celle que l'on utilise dans le lambda-calcul typé pour signifier « la valeur M est de type P », ou dit autrement M est un P. Or, en logique formelle, un jugement de la forme « S est P » est appelé un jugement catégorique ou prédicatif; jugement qui met en relation un sujet S avec un prédicat P. Maintenant, si tu reprends les deux tables susmentionnées, tu pourras constater (ébahi ?) que la première catégorie de la relation (à savoir celle de substance et accident ou état) a pour corrélat la forme logique des jugements catégoriques.

Si Kant est mon maître à penser, comme tu aimes le qualifier, ce n'est pas sans raison. Il avait parfaitement compris ce qu'une partie de la communauté scientifique a mis près de deux cents ans à retrouver. ;-)

Le fonctionnalisme de l'état-machine tel que développé par Hilary Putnam repose fondamentalement sur les notions de changements d'états et de causalité. Contrairement à Kant, il ne prend même pas la peine de rechercher quelle pourrait être l'origine de ces notions (empirique ou a priori) ni quelles en sont les limites. Pourtant, tout comme pour la théorie de la calculabilité, le seul moyen qu'à l'être humain de déterminer les limites de notions, c'est d'emprunter le chemin des méthodes formelles (ce que fit Kant, que cela te plaise ou non). Et, comme dans le cas de la théorie de la calculabilité, les catégories aboutissent à un problème de l'arrêt connu sous le nom d'antinomies de la raison pure. La plus célèbre étant sans doute la troisième qui se voit affronter dans un débat qui n'a jamais de fin cette thèse et cette anti-thèse :

• Thèse : La causalité déterminée par les lois de la nature n’est pas la seule d’où puissent être dérivés tous les phénomènes du monde. Il est nécessaire d’admettre aussi, pour les expliquer, une causalité libre.
• Anti-thèse : Il n’y a pas de liberté, mais tout dans le monde arrive suivant des lois naturelles.

Antinomie qui fait le sujet de la vidéo donnée plus haut de Mr. Phi. Et la solution kantienne à cette antinomie apparente entre nature et liberté est justement la loi du devoir ou impératif catégorique qui prend son fondement dans la commune raison humaine. Puis sur cette notion de devoir, on peut édifier la doctrine philosophique du Droit. Conséquemment, tout être doué de raison est soumis au principe du devoir, et devient, par là-même, un sujet de droit. Si l'on considère que, des êtres connus pour l'instant de nous, seuls les êtres humains sont doués de raison, on aboutit au principe suivant : « Les hommes naissent et demeurent libres et égaux en droits ».

Si l'on ajoute à ce qui précède ce paragraphe de la page Wikipédia sur le computationnalisme :

Ainsi, la formalisation mathématique montre comment les propriétés sémantiques des symboles peuvent parfois être codés selon des règles syntaxiques, tandis que la machine de Turing montre comment la syntaxe peut être relié à un processus causal, qui permet de concevoir un mécanisme capable d'évaluer toute fonction formalisable. La formalisation relie la sémantique à la syntaxe, et la machine de Turing la syntaxe au mécanisme.

Sachant que tu niais au début que la machine ne faisait que de la manipulation syntaxique (alors que c'est même reconnu par les partisans du computationnalisme), que j'ai expliqué clairement pourquoi il en était ainsi en passant par le lambda-calcul et sa règle de beta-reduction, que j'ai viens d'expliquer en détails pourquoi un tel processus est mécanisable (correspondance entre le principe de la logique de Hoare et la règle de déduction logique du modus ponens au fondement du typage des fonctions dans la lambda-calcul), que j'ai, au demeurant, montré comment on pouvait retrouver tous ces principes dans la Critique de la raison pure, sachant tout cela, disais-je, j'ai comme un doute sur lequel de nous deux inventent des hypothèses et concepts ex nihilo, et sur lequel sait réellement ce qu'est la calculabilité, sait ce que l'on demande à la machine de faire pour nous, comment elle fonctionne et sait de quoi il parle. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne vois pas vraiment comment tu écartes à partir de tout ça l'idée qu'une machine puisse … avoir des perceptions.

Ce n'était pas la finalité du tableau de Magritte, mais d'illustrer et d'insister sur la distinction entre signifiant et signifié : le signifiant n'est pas le signifié. Que ce soit un mot, un tableau, un émoji ou que sais-je, une signifiant n'est pas un signifié.

Les états physiques d'une machine nous servent de signifiants (comme le sont les états de bien d'autres matières inertes), par les lois causales physiques connus de nous (à l'heure actuelle c'est de l'électronique) nous mécanisons et automatisons le traitement purement syntaxique des signes, mais les seuls êtres qui conférent une signification à ces signes sont les êtres humains. L'homme dans la chambre chinoise ne leur en attribue aucune, tout comme n'importe quel ordinateur. Pour ce qui est de leur attribuer une perception, on s'approche du fantasme. Autant dire que la pierre perçoit le soleil, parce qu'il a pour effet de la réchauffer.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Comment tu détermine que je suis doué de raison ?

Tu veux savoir comment je détermine qu'un autre être que moi est doué de raison ? Je le postule par analogie avec la manière dont je m'apparaît à moi même intérieurement. La maîtrise extérieure du langage est une condition nécessaire mais non suffisante. Si tu attends de moi un critère nécessaire et suffisant, sur le plan empirique, pour déterminer chez un être, autre qu'humain, l'existence de la raison, je crains fort de ne pouvoir en donner un. Mais je défie quiconque du pouvoir en fournir un qui fasse consensus. Pour le dénier à une machine, rien de plus simple : on sait parfaitement comment elle fonctionne (elles sont notre création) et il n'est nullement nécessaire d'invoquer l'existence de la raison pour expliquer n'importe lequel de leur résultat (rasoir d'Ockham : rien ne sert de multiplier les êtres sans nécessité). Autant vouloir conférer de la raison à la lune pour expliquer l'impact de son champ de gravitation sur les marées terrestre (le principe de causalité d'une matière inerte explique aussi bien l'action de la lune que celui d'un programme exécuté par une machine).

Un sujet de droit ? Tu parles d'un point de vue légal ?

Bien entendu. Je parle du droit que l'on trouve dans les différents codes (pénal, civil…) et déterminé par nos représentants à l'Assemblée et au Sénat.

D'une part c'est toi qui fait ce glissement et d'autre part si elles deviennent des entités légales elles peuvent aussi commettre des plagiats. Mais le fait d'être doué de raison ne donne pas les même droits qu'un humain.

Je fais ce glissement parce qu'il est une conséquence nécessaire de l'attribution de l'intelligence et de la compréhension aux machines. Et si, être doué de raison confère les même droits, du moins pour un kantien : le principe du droit est fondé sur la raison. Si les autres animaux dispose d'un entendement, jusqu'à preuve du contraire, rien ne permet de conclure à l'existence de la raison chez eux : un entendement qui se prend lui même pour objet et qui se manifeste par un usage argumentatif du langage (comme nous le faisons depuis le début du débat). Raison pour laquelle je ne me considère que dans un rapport éthique et non juridique avec eux. En revanche, je n'entretiens aucun de ses rapports avec une simple machine.

Mais à mon tour de poser une question. Qu'est-ce qui te pousse à considérer que les machines sont intelligentes et comprennent ce qu'elles font ? C'est parce que maintenant l'entrée et la sortie de l'interaction avec le programme se fait en langue naturelle ? Quand tu joues dans la REPL python, le programme ne montre pas le moindre signe d'intelligence, mais quand c'est la REPL d'un agent conversationnel, c'est intelligent ? Et une ligne automatique du métro, elle comprend ce que c'est que conduire un métro (au moins, pour la sécurité des passagers, la rigueur formelle de sa conception fait qu'elle n'hallucine pas) ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La vrai pipe n'existe pas, pour paraphraser le petit enfant bouddhiste du premier Matrix. :-P C'est la distinction kantienne entre le phénomène et la chose en soi (ta « vraie pipe »). Si, au fondement des phénomènes que nous percevons dans l'espace-temps (une pipe), on peut bien poser une chose en soi (la « vraie pipe »), il s'avére que la chose en soi est inconnaissable et non spatio-temporellement déterminée. Si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous-mêmes (ils sont les formes a priori de notre sensibilité). Parler d'objets spatio-temporellement déterminés sans référence à un observateur qui les perçoit (comme la « vraie pipe ») est une proposition vide de sens.

C'est la non prise en compte de cette distinction (phénomène et chose en soi) qui entraîne notre raison dans des illusions dialectiques dont elle a du mal à se départir. C'est ce qui a amené Descartes à considérer un esprit sans corps ayant conscience de lui même, illusion objet du premier chapitre de la dialéctique transcendantal et qui réfute au passage le matérialisme. Même Gödel fût victime de cette illusion en tentant de ressusciter la preuve ontologique de l'existence de Dieu, preuve formellement inattaquable : elle a été certifié en Isabelle/HOL. Cette illusion est l'objet du dernier chapitre de la dialectique, celui sur L'Idéal de la Raison Pure . Elle trouve son fondement dans la catégorie de la communauté et celle de la nécessité, c'est-à-dire la forme logique du raisonnement disjonctif et la modalité apodictique (voir la correspondance entre la table des jugements et celles des Catégories, un correspondance de Curry-Howard bien avent l'heure ;-). Rien d'étonnant que Gödel ait eu recours à la logique modale, mais c'est une illusion de la raison… L'homme s'y trouve dupe de son propre langage, comme ceux qui voient de l'intelligence ou de la compréhension dans une machine exécutant un programme.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu préfère élargir la notion de syntaxe. C’est rigolo.

Je n'élargi pas la notion de syntaxe, mais l'utilise dans la même acception que John Searle lorsqu'il distingue syntaxe et sémantique. La syntaxe relève de toutes les règles qui régissent l'usage des termes du langages entre eux, la sémantique consiste en un rapport entre le langage et quelque chose qui lui est extérieur : le rapport signifiant (les mots) à signifié (les choses); voir sémantique Tarskienne.

Tu ne trouveras personnes qui ne considère pas la réduction d'un lambda-terme (c'est-à-dire l'exécution d'un programme) comme de la simple manipulation syntaxique des termes du langage.

Exécuter un programme c'est comme calculer le polynôme 1 + x + x² pour la valeur 4. Cela consiste à remplacer toutes les occurences de x par 4 (c'est cela la beta-réduction), pour obtenir 1 + 4 + 4², puis réduire l'expression obtenue. Tout ceci n'est que de la manipulation syntaxique. Le lambda-calcul et sa règle de beta-reduction n'est qu'une extension de ce procédé, ce qui donne un formalisme de la notion de calculabilité équivalent aux machines de Turing.

La thèse de Church affirme que tout ce qu'un être humain peut calculer est exprimable dans chacun de ces formalismes (je la partage, et à dire vrai elle fait peu débat). Le computationalisme est la thèse converse : tout ce qu'une homme pense est réductible au calcul et donc exprimable dans l'un de ces formalismes. Cette thèse je la récuse.

Mais du coup le te répète sous une forme un peu différente une question que j’ai posé plus haut : qu’est ce qui me distingue d’un zombie qui ne fait que du traitement syntaxique ? ou puisque nous communiquons par écrit uniquement qu’est ce qui te permet de dire que je suis un humain ou une IA ?

Rien. Mais, mes interactions avec les êtres humains ne se limitent pas à des échanges écrits. Le but de la chambre chinoise n'est pas de dire qu'une machine ne peut pas passer le test de Turing (ce que ne font pas encore les chat bots les plus actuels), mais de dire que ce test est insuffisant pour conclure que la machine comprend ce qu'elle fait. Il n'est nullement nécessaire d'invoquer la notion de compréhension pour expliquer l'expérience de pensée.

S’il n’est pas possible de le déterminer à quoi sert cette distinction ? Uniquement pour créer artificiellement si nécessaire des différences (un peu comme quand on disait que les animaux ne ressentaient pas la douleur) ou il y a une démarche autre dans la quelle c’est utile ?

Savoir si l'être avec lequel j'intéragis est doué de raison et donc s'il est un sujet de droit. La distinction n'a pas d'intérêt en philosophie théorique (connaissance de ce qui est) mais un intérêt en philosophie pratique (connaissance de ce qui doit être : éthique et droit). J'ai des devoirs de vertus (éthique) envers tout être vivant (les animaux dans leur ensemble), mais ceux doués de raison sont aussi, tout comme moi, soumis au principe du devoir et dans nos devoirs réciproques nous sommes soumis au principe du droit.

Remarques, considérer que la machine peut être douée de raison cela ôterait une épine du pied des entreprises d'IA. Dans les débats actuels sur le droit d'auteur et les IA, les auteurs qui s'estiment léser ne devraient pas ester les entreprises mais la machine elle-même. :-D

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

D’une par d’un point de vu technique ces IA peuvent te dessiner cette reine, ils peuvent la repérer dans une image.

Il faut vraiment arrêter de croire que ces IA raisonnent au niveau syntaxique car c’est faux.

À moins que ces IA ne soient pas un programme informatique, c'est la seule chose qu'elles peuvent faire. En tant que programme, je peux choisir n'importe quelle représentation équivalente : choisissons le lambda-calcul. Toute exécution d'un programme, vu sous sa représentation comme lambda-terme, n'est rien d'autre qu'un processus syntaxique de réécriture connu sous le nom de béta-réduction.

Même dans un logiciel comme Coq, la machine ne raisonne pas. C'est nous, être humains, qui interprétons ce jeu de réécriture, ou les états successifs de la machine, comme le déroulement d'un raisonnement. Mais, au sens propre du terme, la machine ne raisonne pas. Pas plus qu'un distributeur automatique de boissons comprend et raisonne sur ce qu'il fait.

Il en est de même dans la chambre chinoise, seule la personne à l'extérieur de la chambre donne une signification au texte en chinois et comprend ce qu'il s'y dit. Pour la personne à l'intérieur (ou même les système opérateur + chambre + tables), tout cela est vide de sens : ce n'est que de la manipulation syntaxique, de la réécriture de signe. Seuls les rapports de signe à signe sont considérés, et non les rapport de signifiant à signifié (ce en quoi consiste la sémantique nécessaire à la compréhension).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Si ce n’est pas le cas est-ce que c’est que pour toi par construction les machines ne peuvent pas comprendre ?

Pour moi c'est bien cela, une machine pensante est inconcevable. Je ne suis pas fonctionnaliste et encore moins computationaliste. J'ai du mal à concevoir ces doctrines comme non assises sur le matérialisme (la pensée étant conçue comme une propriété émergente du cerveau), même si Hilary Putnam pensait que le fonctionnalisme était conciliable avec le dualisme corps-esprit, et je considère le matérialisme comme réfuté par la dialectique transcendantale de la Critique de la Raison Pure.

Sans être un grand partisan de l'argumentaire de la chambre chinoise, je souscris à sa conclusion car reconnaît le principe selon lequel « la syntaxe n'est ni constitutive, ni suffisante à la sémantique ». Pour reprendre un aphorisme de Wittgenstein : ce que le langage signifie, cela se montre, cela ne se dit pas (je le formule de mémoire, mais l'idée est là). Manipuler les signifiants ne donnera jamais accès au signifié. Ton exemple du roi, de la femme et de la reine, n'est que de la manipulation syntaxique; il n'y a aucun rapport à quelque chose qui est au-delà du langage : un signifié. En logique mathématique, on retombe sur la même problématique en combinant deux résultats de Gödel : le théorème de complétude et le théorème d'incomplétude.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

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.

Le langage fonctionnant par effet de bords, il faut effectivement utiliser la logique de Hoare pour vérifier la correction des programmes écrits avec.

Cela étant, il me semble que Thomas voulait dire que l'exemple était monomorphe (les deux variables d'entrées sont de types Int) et non polymorphes (il n'y a pas de variable de types); d'où sa remarque sur le manque de généralité.

Quoi qu'il en soit, la logique de Hoare est une proche parente de la théorie des types en partageant le même fondement : la structure logico-déductive de l'ésprit humain. Par exemple, la règle de composition :

{P} S {Q} , {Q} T {R}
---------------------
    {P} S; T {R}

est la version impérative du typage de la composition de fonction dans les langages fonctionnels (('p -> 'q) -> ('q -> 'r) -> 'p -> 'r dans le langage des types de OCaml), règle qui a pour fondement une double application du modus ponens (si A alors B, or A, donc B).

Les programmeurs impératifs composent les instructions, comme les programmeurs fonctionnels composent les fonctions.

P.S : Joli dépêche qui résume bien le domaine et l'état des lieux. J'étais passé à côté et je compte bien t'écrire un commentaire plus long et détaillé (qui me demandera plus de temps que cette simple remarque sur la logique de Haore). En plus, ça me permettra de parler de mes marottes (la logique formelle, la théorie de la démonstration, la correspondance de Curry-Howard et la philosophie des mathématiques) sans que thoasm m'en fasse le reproche. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Qu'il me soit permis d'ajouter une remarque sur la démarche qui consiste à comparer le jeu mathématique et celui des échecs, des dames, du Go ou de Othello.

Leibniz vantait fort une caractéristique dont il était l’inventeur ; tous les savants ont regretté qu’elle fût ensevelie avec ce grand homme. Ce regret m’est une occasion de dire mon sentiment sur l’art combinatoire. J’avoue que dans ces paroles du grand philosophe, je crois apercevoir le testament du père de famille dont parle Esope : étant sur le point d’expirer, il déclara en secret à ses enfants qu’il avait un trésor caché quelque part dans son champ, mais, surpris par la mort, il ne put leur indiquer l’endroit où il l’avait enfoui ; ce fut pour les enfants l’occasion de fouiller leur champ avec la plus grande ardeur, de le creuser et de le retourner en tous sens ; tant et si bien que, quoique trompés dans leurs espérances, ils finirent par se trouver plus riches de la plus grande fécondité de leur champ. Nul doute que ce ne soit là le seul fruit à retirer de la recherche de ce mécanisme inventé par Leibniz, si l’on doit s’en occuper encore.

Kant, Explication nouvelle des premiers principes de la connaissance métaphysique

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ça veut dire quoi "partir en sucette" ?

C'est la machine qui part en sucette (elle boucle sans fin, le programme ne s'arrête jamais), pas les êtres humains. Si je cherche un exemple d'énoncé indécidable, le postulat d'Euclide est le premier qui me vient à l'ésprit. Et pourtant il a alimenté une grosse partie de la géométrie du XIXème siècle, et quand un physicien s'y intéresse il donne une réponse plus que satisfaisante au périhélie de Mercure. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Non, le jeu est infini évidemment

Que le jeu soit infini je m'en fous, c'est pas là le problème. Ce que je veux savoir c'est si la méta-machine part en sucette. Et donc est-ce que jouer aux maths c'est la même chose que jouer aux échecs, au Go ou Othello ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu parles bien de ce que je dis dans mon commentaire "oui et non" finalement, la recherche de preuve.

J'ai l'impression de parler d'autre chose, mais c'est peut être moi qui m'explique mal.

La méta-machine nourrit par tous les coups jouables du jeu est capable de partir en couille (boucler sans fin sur certaines de ses entrées). Alpahe go et compagnie ne sont rien d'autres que des optimisations de ces machines (elles ne font pas du brut force). Néanmoins jouer au jeu mathématique est-t-il semblable à jouer aux échecs, au go ou othello ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui il y un lien avec le programme de Hilbert (et c'était bien à cela que voulait répondre entre autre Turing), mais ce que je voulais dire est plus simple.

Ton commentaire auquel j'ai répondu en premier contenait ce paragraphe :

Exemple limite : un raisonnement mathématique. Prend un ensemble de démonstration mathématiques, à classer comme "correctes" ou "incorrecte", entraine le donc à discriminer le mathématiquement correct du mathématiquement incorrect. Les lois de la logiques ont des règles du jeu. Un réseau de neurone "séquentiel" peut en principe apprendre les différentes règles pertinentes, et classer leur application correcte ou pas, voire pointer directement les applications incorrectes.

Dans son article originaire, Turing, où il développe sa notion de machine à calculer, traite justement de cette question mais sans recourir à un apprentissage automatique. Relativement à cette question, on se retrouve dans le cas que Liorel, dans sa dépêche, décrit en ces termes :

En définitive, on peut voir le réseau de neurones comme un outil qui résout approximativement un problème mal posé. S’il existe une solution formelle, et qu’on sait la coder en un temps acceptable, il faut le faire. Sinon, le réseau de neurones fera un taf acceptable.

Et justement, Turing, dans son article, donne une telle solution formelle. Il a montré qu'il existe une machine à calculer qui prend en entrée un argumentaire P et un théorème T et qui vérifie si P est bien une preuve de T et cela en un temps fini. Cette machine prend n'importe quelle preuves et n'importe quel théorème et s'arrête toujours pour répondre à la question. Une telle machine, ou un tel programme, est ce que l'on appelle un type checker.

Mais continuant son raisonnement, pour répondre au problème de Hilbert, il construit idéalement un autre machine. Celle ci ne va pas seulement vérifier qu'une preuve est correcte mais elle va en chercher une. En entrée, elle ne prend plus une preuve et un théorème mais seulement un théorème et elle cherche à savoir si on peut le prouver ou le réfuter. Pour la décrire, il se sert de la machine précédente (le type checker), puis constate que tous les argumentaires possibles sont récursivement énumérables : il a une seconde machine qui va alimenter la première avec toutes les preuves possibles. En gros il fait de la composition de fonctions pour faire du brut forcing. Puis, il montre, finalement, que pour certaines entrées sa technique de brut force mouline sans fin : c'est le problème de l'arrêt ou l'existence d'énoncés indécidables.

Chercher un preuve pour un théorème donné, c'est cela que font des logiciels LLM comme copilot. Mais il ne peuvent pas simuler bien mieux qu'un programmeur junior. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

personne n'en doutai je pense, mais c'était juste pour faire mon point.

Personne n'en doute, ça c'est ce que tu dis maintenant. Mais, à la base, Turing s'est posé la même question que toi (classifier les preuves mathématiques) et sa réponse me semble plus sensée et sérieuse que la tienne. On n'a peut être pas la même lecture et interprétation de Turing ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Et ben … ça se discute.

En fait ça ne se discute même pas. Tu n'as juste pas compris la question. Si la question est « énonce loi un théorème, j'en chercherais la preuve », alors oui il n'y a pas d'algorithme pour y répondre, c'est bien le résultat des travaux de Gödel et Turing. Mais, pour arriver à leur conclucsion, ils ont bien comenncé par prouver que la question de la classification des preuves mathématiques était décidables. Le faire en 80 lignes de codes n'est rien d'autre qu'une sytnhèse de leur argumentaire. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tout dépend de ton projet. Si ton but est de dire que les réseaux de neurones peuvent aller au delà du calcul des probabilités, le plus simple est invoquer le fait qu'il soient Turing complet.

Néanmoins, relativement à la question que tu as mis sur la table, il est inepte de passer par un LLM pour la résoudre. How to implement dependent types in 80 lines of code. Bien que ce code ait des défaut et soit perfectible, un tel algorithme de classification ne doit pas dépasser la centaine de lignes de code. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Exemple limite : un raisonnement mathématique

Loin d'être limite, cet exemple est celui qui a donné l'ordinateur à l'humanité. Quoi qu'il en soit, pour ce type de problème on tombe sous le coup suivant : le problème est formellement circonscrits, on a des algorithmes qui le résolvent à 100% sans aucun risque d'erreurs. Pourquoi donc passer par un LLM pour résoudre cette question ? Déjà qu'une machine de Turing est con comme une huître, mais si en plus en plus son programmeur s'y met, on n'est pas sorti de l'aurberge. :-D

Et tout programmeur cotoit quotidiennement un tel algorithme, vérifier qu'une preuve est logiquement valide cela s'appelle faire du type cheking. Après il y a des systèmes de types plus sérieux que d'autres, d'où le débat sur Rust dans le code du noyau Linux. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est bien ce que je disais tu n'écoutes pas et tu interprètes de travers.

Je suis prêt à écouter et discuter, je n’attend même que ça !

Toi peut être, mais moi non. J'ai des choses bien plus importantes et sérieuses à faire, comme lire de le dernier livre d'Alain Aspect, Si Einstein avait su, où il revient sur sa résolution expérimentale du conflit entre Bohr et Einstein au sujet du paradoxe EPR. Il contient de la philosophie des sciences et de l'épistémologie bien plus intéressante.

Quel est le cadre plus général de l’induction de Solomonoff ?

Le cadre le plus général, je te l'ai déjà dit mais tu fais la sourde oreille : c'est le principe de l'inférence abductive, dont la loi de Bayes n'est qu'un cas particulier.

Parce que pour l’instant, la meilleure objection que j’aie eu, c’est "et si le processus stochastique en question générant la séquence d’observations n’est pas calculable ?". Qui n’est effectivement pas abordée noir sur blanc dans le texte original.

Et ce n'est pas ce que j'ai dit. Tu as appris à lire où ? Je reproche, entre autre, à Yudkoswki (via son personnage Blaine) de sauter du coq à l'âne en passant d'un énoncé du type « Le canada envahit les États-Unis », à l'enregistrement de la totalité de ce qu'à observé Ashley depuis sa naissance, pour finir sur la simple étude d'un écran de taille 1920 * 1080 avec des pixels encodés sur 32 bits et un taux de rafraîchissement de 60 Hz. Alors là oui, on arrive sur un automate fini : la taille de son espace d'états est même calculé par Ashley. C'est cela qui est fini : le nombre d'états possibles du système étudié. Alors là, certes, vous pouvez appliquer votre théorème. Mais j'appelle cela du foutage de gueule !

Je ne sais pas si tu as une vague connaissance des fondements de la théorie de la probabilité et de la théorie de la mesure de Borel-Lebesgue, mais le seul type d'énoncés sur lesquels portera votre distribution de probabilité sont construits sur les énoncés élémentaires de la forme : « sur la frame n le pixel aux coordonnées x et y sera p » (où p est un nombre codé sur 32 bits). Et à partir des ces énoncés atomiques, on considère le langage construit via les connecteurs logiques de la conjonction (et), de la disjonction (ou) et de l'implication (si A alors B). De fait, la loi de Bayes dans ce cas très particulier est la forme que prend l'inférence abductive, la distribution de probabilité déterminant une logique modale sur cette famille d'énoncés.. Mais j'ai beau retourné dans tous les sens la totalité (dénombrable) de ces énoncés, je n'y vois à aucun moment apparaître celui-ci : « le Canada envahit les États-Unis ».

Mais dans le fond ce qu'il y a de plus ridicule dans ce que j'ai lu, et tout simplement ce que Yudkowski-BLaine entend par good epistemology :

Fairness requires that I congratulate you on having come further in formalizing 'do good epistemology' as a sequence prediction problem than I previously thought you might.

L'épistémologie telle que pratiquée depuis Kant (Russel, qui est à l'origine de l'introduction du mot en langue française, le considérait comme le père de l'épistémologie) n'a jamais consisté en l'étude de la prédiction de séquences. La seule science dont un des résultats pourrait être de fournir de telles prédictions est la physique-mathématique. Mais je doute que les physiciens acceptent que tu réduises leur science à cette simple finalité. Les philosophes, quant à eux, lorsqu'ils font de l'épistémologie étudies les méthodes mises en œuvre par les scientifiques dans la constitution de leur savoir. Et ce que décrit Yudkowski n'a rien à voir avec la pratique des physiciens. Pour citer la Critique de la Raison Pure, voilà comment ces derniers procèdent :

La physique arriva beaucoup plus lentement à trouver la grande route de la science ; car il n’y a guère plus d’un siècle et demi qu’un grand esprit, Bacon de Verulam, a en partie provoqué, et en partie, car on était déjà sur la trace, stimulé cette découverte, qui ne peut s’expliquer que par une révolution subite de la pensée. Je ne veux ici considérer la physique qu’autant qu’elle est fondée sur des principes empiriques.

Lorsque Galilée fit rouler sur un plan incliné des boules dont il avait lui-même déterminée la pesanteur, ou que Toricelli fit porter à l’air un poids qu’il savait être égal à celui d’une colonne d’eau à lui connue, ou que, plus tard, Stahl transforma des métaux en chaux et celle-ci à son tour en métal, en y retranchant ou en y ajoutant certains éléments, alors une nouvelle lumière vint éclairer tous les physiciens. Ils comprirent que la raison n’aperçoit que ce qu’elle produit elle-même d’après ses propres plans, qu’elle doit prendre les devants avec les principes qui déterminent ses jugements suivant des lois constantes, et forcer la nature à répondre à ses questions, au lieu de se laisser conduire par elle comme à la lisière ; car autrement des observations accidentelles et faites sans aucun plan tracé d’avance ne sauraient se rattacher à une loi nécessaire, ce que cherche pourtant et ce qu’exige la raison. Celle-ci doit se présenter à la nature tenant d’une main ses principes, qui seuls peuvent donner à des phénomènes concordants l’autorité de lois, et de l’autre les expériences qu’elle a instituées d’après ces mêmes principes. Elle lui demande de l’instruire, non pas comme un écolier qui se laisse dire tout ce qui plaît au maître, mais comme un juge qui a le droit de contraindre les témoins à répondre aux questions qu’il leur adresse. La physique est donc redevable de l’heureuse révolution qui s’est opérée dans sa méthode à cette simple idée, qu’elle doit, je ne dis pas imaginer, mais chercher dans la nature, conformément aux idées que la raison même y transporte, ce qu’elle veut en apprendre, mais ce dont elle ne pourrait rien savoir par elle-même. C’est ainsi qu’elle est entrée dans le véritable chemin de la science, après n’avoir fait pendant tant de siècles que marcher à tâtons.

Kant, préface à la deuxième édition de la Critique de la Raison Pure.

Comme exemple de ce mode de procédure, on pourrait ajouter, pour citer des expériences postérieurs à la mort de Kant, Foucault faisant osciller son pendule pour illustrer la rotation de la terre, l'éclipse solaire de 1919 pour trancher entre gravitation newtonienne et relativité générale, les expériences d'Alain Aspect au laboratoire d'optique d'Orsay, et j'en passe.

Ce que décrit le dialogue Ashley-Blaine, ce n'est pas la méthodologie d'être doté d'intelligence, mais celle parfaite pour un être qui en est totalement dénué, une IA : un Idiot Artificiel qui, pour reprendre les mots de Kant, se laisse conduire par la nature comme à la lisière. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Encore une fois, quand on me dit "j’ai pas lu mais c’est ridicule", je m’énerve.

Je n'ai pas dit que je ne l'avais pas lu, mais que je me suis arrêté de le lire quand j'en ai eu marre de lire des inepties. Ce n'est pas la même chose. Pour être extrêmement clair, je n'ai aucun problème avec le théorème de Solomonoff (ni celui de Von Neumann, d'ailleurs), mais seulement avec l'interprétation douteuse que vous cherchez à lui donner.

Ce théorème ne révolutionne en rien la question de l'induction ou celui du rasoir d'Ockham. Pour prendre une comparaison simple à comprendre : je t'énonce que la somme des angles d'un polygone convexe étoilé à n cotés est (n - 2) * 180. Et au fond, tu me réponds : on peut faire mieux, si on se limite au cas du triangle, la forme est plus simple cela donne toujours 180 degrés. C'est ce que vous faites avec le théorème de Solomonoff : en restreignant (arbitrairement) la classe des objets sur laquelle porte votre champ d'investigation, vous arrivez à une formulation que vous considérez plus simple. Mais elle n'est que la mise en forme d'un principe général dans un de ses cas particuliers.

Dans un autre commentaire plus bas, tu écris :

le problème de l’amateur qui n’a pas un professeur pour lui dire quand il est à côté de la plaque

Et quand on t'explique ce qui cloche, tu n'écoutes pas. Ça ne va pas t'aider à comprendre. ;-)

Pour information, je ne suis pas philosophe de formation mais mathématicien et logicien. Si je porte un grand intérêt à la philosophie, c'est pour la simple raison que donna Jean Dieudonné comme réponse à Bernard Pivot lors de cette interview dans Apostrophes.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Quel argumentaire puissant. Je ne peux plus que m’avouer vaincu, je suppose.

Alors s'il faut argumenter… Il faut surtout être sérieux deux minutes. Je te demande de me définir une distribution de probabilité sur des événements du type « Le Canada envahit les États-Unis » (le personnage de Blaine affirme que la magie du théorème de Solomonoff permettra de la déterminer) et vous me répondez en substance : considérant que l'univers est un automate à états finis alors on peut déterminer une telle distribution de probabilité, et en plus ça tombe bien on se retrouve dans le cas d'application du théorème. Vous pensez sérieusement que l'univers est un automate à état fini et que, par exemple, le travail des physiciens consistent à déterminer les lois qui régissent ses transitions ? Si c'est le cas, alors oui, il faut consulter. ;-)

Mon problème avec ce texte n'était pas « tl;dr » mais que cette réponse je l'avais vu venir gros comme une maison, et que je n'ai pas de temps à perdre à lire de telles inepties. Votre « good epistemology » c'est quoi ? L'étude des automates à états finis ? Et on peut l'étendre à toutes les formes de savoir humain ?

Comme tu aimes les probabilités : les séquences de bits (0 et 1) calculables par un tel algorithme sont récursivement énumérables. On peut identifier une telle suite à un réel dans le segment [0; 1]. Si on considére la distribution de probabilité uniforme sur cette intervalle, quel est est la probabilité de tomber au hasard sur un nombre calculé par l'algorithme ? Pour de simple raison de cardinalité, cette probabilité est nulle. Certes l'ensemble est dense dans l'intervalle pour sa topologie usuelle, mais il pèse peanuts.

Par pitié, rassurez-moi. Dites moi que je vous ai terriblement mal interprété.

Assurément, tu m'as mal interprété. Pour Von Neumann, j'ai lu trop vite, j'ai cru qu'il appliquait une axiomatique à la réalité empirique sans plus de justification que cela, ce qui, je l'avoue, aurait me faire dire : « attends un peu, tu as du louper un truc ». Et c'est bien le cas :

Many economists will feel that we are assuming far too much … Have we not shown too much? … As far as we can see, our postulates [are] plausible … We have practically defined numerical utility as being that thing for which the calculus of mathematical expectations is legitimate.

L'adjectif plausible ajoute bien une marque problématique sur le plan de la modalité (sans pour autant renvoyer à une quelconque distribution de probabilité). Il me faudrait lire plus en détails la source elle même pour me faire une idée son point de vue, mais je n'y ai pas intérêt.

Néanmoins, je justifiais ce que je considère être de la cuistrerie que d'appliquer une axiomatique à la réalité sans justification d'aucune sortes (ce que je perçois chez Yudkowsky). Sur le sujet, voir par exemple l'excellente introduction d'Einstein sur le sujet dans son livre de vulgarisation sur les théories de la relativité.

Enfin, rassure toi pour moi, lorsque l'on discute, même en 2025, des possibilités et limites du calcul on est en très bonne compagnie avec Kant. Je ne vais pas faire un exposé détaillé de l'histoire des idées, mais sache que, pour rependre l'exemple de Yudkowsky, il a occupé une place non négligeable dans l'intervalle qui sépare Poe de Shannon. La clarification de la notion de calculabilité tient, en partie, son origine dans la volonté de Gottlob Frege de réfuter un point de la philosophie kantienne. Finalement, on va aborder la Critique de la raison pure. ;-)

Dans cette ouvrage, où il expose clairement le problème qu'il cherche à traiter, on y trouve au chapitre VI (problème général de la raison pure) de l'introduction ce passage :

C’est avoir déjà beaucoup gagné que de pouvoir ramener une foule de recherches sous la formule d’un unique problème. Par là, en effet, non-seulement nous facilitons notre propre travail, en le déterminant avec précision, mais il devient aisé à quiconque veut le contrôler, de juger si nous avons ou non rempli notre dessein. Or le véritable problème de la raison pure est renfermé dans cette question : Comment des jugements synthétiques à priori sont-ils possibles ?

Pour comprendre la signification de cette question, il faut lire les chapitres précédents où il détermine avec précision ce qu'il entend par jugement synthétique et jugement a priori.

Cette question générale se subdivise en une question particulière : Comment les mathématiques pure sont-elles possibles ?. En effet, dans le chapitre qui précède (chapitre V), on trouve ce texte :

Les jugements mathématiques sont tous synthétiques. Cette proposition semble avoir échappé jusqu’ici à l’observation de tous ceux qui ont analysé la raison humaine, et elle paraît même en opposition avec toutes leurs suppositions ; elle est pourtant incontestablement certaine, et elle a une grande importance par ses résultats. En effet, comme on trouvait que les raisonnements des mathématiques procédaient tous suivant le principe de contradiction (ainsi que l’exige la nature de toute certitude apodictique), on se persuadait que leurs principes devaient être connus aussi à l’aide du principe de contradiction, en quoi l’on se trompait ; car si le principe de contradiction peut nous faire admettre une proposition synthétique, ce ne peut être qu’autant qu’on présuppose une autre proposition synthétique, d’où elle puisse être tirée, mais en elle-même elle n’en saurait dériver.

Et voilà ce que Frege voulait réfuter : il voulait montrer que loin d'être synthétiques, les jugements mathématiques sont tous analytiques. Il mit au point la théorie des ensembles dites de Cantor-Frege, mais elle s'avéra contradictoire. Ce qui créa une crise au sein des mathématiques au tournant des dix-neuvième et vingtième siècles (voir, par exemple, cette article de Poincaré où il prend, à bon droit, la défense de Kant), puis le programme de Hilbert, soldé par l'incomplétude gödelienne et le problème de l'arrêt de Turing. Bilan des courses : Kant avait raison !

L'histoire est racontée, par exemple, dans le livre Les métamorphoses du calcul de Gilles Dowek. M. Dowek a reçu, en 2024, la Médaille Histoire des Sciences et Épistémologie de l'Académie des sciences en 2024. Je te laisse décider si l'Académie des sciences est en mesure de distribuer des gages de « good epistemology ».

Tu pourras lire avec intérêt l'article Analytic and synthetic judgment in type theory de Per Martin-Löf (un théoricien des types). La théorie des types modernes est basé sur le résultat logico-mathématique de la correspondance de Curry-Howard qui est complétement kantienne dans l'esprit. À ce sujet, voir le chapitre de la Critique de la raison pure consacré à la logique transcendentale et la correspondance entre ces deux tables tables des jugements et table des catégories. Un autre théoricien des types, Jean-Yves Girard (auteur, en autre, des sytème F et systèmes F-omega à la base de langage de programmation comme Haskell ou OCaml) s'étonnait d'ailleurs dans l'introduction de son dernier livre, le fantôme de la transparence de l'étonnante actualité de la philosophie kantienne. Tu trouveras sur le site du Collège de France, une présentation de la correspondance de Curry-Howard lors de première année de cours de Xavier Leroy : Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui. Reste à savoir si le Collège de France fait de la bonne science et de la bonne épistémologie.

Personnellement, j'aime aussi ce texte À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court) de Jean-Louis Krivine. M. Krivine fut un de mes professeurs lorsque j'étais encore un jeune étudiant, et c'est lui qui m'initia à la correspondance de Curry-Howard. Fort heureusement pour moi, j'étais, à l'époque, déjà un lecteur de la Critique de la raison pure. Je me suis alors dit : « Ô c'est comme Kant, mais en plus simple », et j'ai eu 20 au module en question. ;-)

Pour conclure, et revenir sur de la bonne epistémologie, je te propose cette conférence vidéo de Gilles Dowek sur le thème La dificile explication des résultats de calculs : des preuves automatiques à l'apprentissage automatique.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

y a réellement un truc derrière ou c'est juste que tu as mal choisi ton exemple ?

Oui, mais c'est parce que tu n'as pas son capital que tu ne le vois pas. ;-)

Au lieu d'acheter comptant, en investissant les 200M€ à un rendement supérieur au taux de remboursement de sa dette, il accroît son capital. À la fin, lorsqu'il aura rembourser son emprunt, son capital sera plus important que s'il avait acheter son Yacht cash.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je vais faire un petit effort et te citer le passage exact, même si vu le ton de ta réponse, je pense que c’est peine perdue.

C'est effectivement peine perdue. ;-) Vous considérez sérieusement cela comme une définition d'une distribution de probabilité sur une famille d'événements du type « le Canada envahit les États-Unis » ? À ce stade, il faut songer à consulter ! Les bras m'en tombent /o\

C'est du même acabit que l'approche « économiste » que tu décris dans ton autre commentaire :

Les économistes ont rencontré ce problème : si les préférences sont de la forme (je préfère A à B), quelle est la validité de les représenter par des nombres réels (fonction d’utilité) ?

La réponse est: si on se limite aux agents rationnels (entre autre: dont les préférences forment un ordre total), les deux sont équivalents.

Ce genre d'énoncé contient bien plus d'informations sur celui qui l'énonce que sur la réalité qu'il cherche à modéliser. Je suis étonné que Von Neumann se soit fourvoyé dans ce genre de chose.

Ensuite le résultat n'est pas si surprenant : si je présuppose des probabilités à l'entrée (voir la liste des axiomes) alors j'ai des probabilités à la sortie. On n'est pas loin de la tautologie. Le problème étant de quel droit puis-je poser l'axiome 3 ? Sur le plan mathématique, on peut poser les axiomes que l'on veut tant que l'on évite la contradiction. Mais lorsque l'on prétend l'appliquer à la réalité, je pose la question typiquement kantienne : Quid juris ? De quel droit ? Où se trouve la déduction transcendentale qui m'autorise à appliquer cette connaissance pure et a priori à la réalité expérimentale ? Et là on quitte le champ des mathématiques, pour celui de la philosophie.

Que tu sois d’accord ou non sur la conclusion finale, le sujet abordé me semble extrêmement intéressant pour le genre de personne qui s’intéresse à ces questions. Dont j’ai l’impression que tu fais partie. J’ai écrit en grande partie de journal pour atteindre ce genre de personne, en mode "hey : il y a des choses intéressantes et nouvelles à regarder là bas".

Oui j'en fait partie, ce sont des interrogations typiquement philosophique. Seulement, sur l'usage des probabilités, il n'y a rien de neuf sous le soleil si ce n'est une extension de l'usage qui est à la limite de me glacer le sang et qui me semble anti-philosophique au plus haut point.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne veux pas me lancer dans l’exégèse de Kant ; je connais très mal le sujet, ma seule intention dans l’invocation du nom est de donner un exemple de théorie épistémologique, pas de me prétendre expert sur le sujet (ou d’en invoquer un).

Alors pourquoi en parles-tu ? D'où t'es venu l'idée de mentionner Kant comme projet similaire à ce que tu cherches à présenter ? Et non ! la Critique de la raison pure n'est pas une théorie épistémologique. D'où sors-tu cette idée ? Si la question de la possibilité de la connaissance expérimentale est aborder de façon secondaire dans l'œuvre, c'est loin d'être sa préoccupation fondamentale.

C’est une très bonne illustration de comment la théorie des probabilités est utilisée dans le projet ukemiste

Je le sais bien, c'est à peu près la seule chose que j'avais réussi à comprendre dans ton texte qui manque franchement de clarté (mais d'autres t'ont déjà expliqué le pourquoi du comment sur le sujet).

Mais tu as loupé le point important dans ce que j'avais écrit, je le remet en graissant ce qui compte :

Le calcul des probabilités permet de développer une logique modale dans laquelle le possible est quantifié par un nombre réel. Mais il n'est pas nécessaire de mesurer le degré de possibilité pour raisonner modalement, et c'est même bien souvent impossible. Ce qui réduit grandement le champ d'extension d'une telle méthodologie pour atteindre la vérité.

Le raisonnement abductif est valide en logique modale si l'on considére comme apodictique la majeure, assertorique la mineure et problématique la conclusion.

Ce que je dis c'est que étant donné une distribution de problabilité, elle détermine une logique modale sur un ensemble d'énoncés (ceux sur qui porte la distribution). Néanmoins, la réciproque est fausse. Toute logique modale ne dérive pas nécessairement d'une distribution de probabilité.

Conséquemment, présenter le calcul de probabilités et la loi de Bayes comme l'alpha et l'oméga d'une épistémologie révolutionnaire, comme si on avait trouvé là une panacée au problème de la vérité et la pierre philosopohale, ça me fait mourir de rire. C'est une thèse d'un ridicule profond.

si tu veux une approche ukemiste de cette question : https://www.lesswrong.com/posts/EL4HNa92Z95FKL9R2/a-semitechnical-introductory-dialogue-on-solomonoff-1 ; qui est également je pense un bon représentant de ce qu’est le projet ukemiste, à la relecture

Ce texte est ridicule, je n'ai pas pu aller jusqu'au bout. Je me suis arrêté ici :

Fairness requires that I congratulate you on having come further in formalizing 'do good epistemology' as a sequence prediction problem than I previously thought you might.

L'honnêteté m'oblige à dire que c'est de l'épistémologie bonne à jeter à la poubelle. La page wikipédia sur l'inférence inductive de Solomonoff précise pourtant :

For this equation to make sense, the quantities P [ D | T ] and P [D|A] must be well-defined for all theories T and A. In other words, any theory must define a probability distribution over observable data D. Solomonoff's induction essentially boils down to demanding that all such probability distributions be computable.

Peux-tu en toute bonne foi me définir une distribution de probabilité sur des événements comme « le Canada envahit les Étas-Unis » (qui devrait plutôt être mis à jour son sa forme converse « les États-Unis envahissent le Canada »), et qui plus est une distribution qui soit calculable sur machine ?

Je rappelle la première règle de bon usage des hyptohèses :

1 ° La possibilité de la supposition même.

Si, par exemple, pour expliquer les tremblements de terre et les volcans, on admet un feu souterrain, cette sorte de feu doit être possible, ne brûlât-il pas comme un corps enflammé. Mais, lorsqu’à l’aide de certains autres phénomènes, on veut faire de la terre un animal dans lequel la circulation d’un liquide intérieur produit la chaleur, c’est une pure fiction, et non une hypothèse ; car les réalités s’imaginent bien, mais non les possibilités : elles doivent être certaines.

règle qui a pour but de contenir les délires de l'imagination.

De plus, présenter la théorie de Solomonoff sous la forme d'une dialogue Platonicien où Socrate est joué par le personnage Blaine, je ne sais pas si je dois rire ou pleurer. Quand on réfléchit au problème que Blaine prétant pouvoir résoudre via cette théorie et au contenu de l'alégorie de la caverne, ça me donne plutôt envie de rire.

C’est l’observation très bête que quand tu es investi émotionnellement dans une hypothèse, c’est là que les biais importants se manifesteront le plus fortement, et qu’il va falloir être particulièrement impitoyable sur les justifications.

Drôle de technique interdite. Je préfère l'approche philosophique kantienne : dans le doute je m'abstiens de juger définitivement, si j'affirme c'est que j'ai été impitoyable sur les justifications. Autrement dit : ne jamais asserter sans examen approfondi des raisons qui mènent à la conclusion, pour tout le reste rester au stade problématique sur le plan de la modalité (sans recourir aux calcul des probabilités là où il n'est pas applicable ;-). Et loin d'être interdite, cette technique est le degré zéro de ce que l'on peut appeler rigueur intellectuelle.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.