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.
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.
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.
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.
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.
Posté par kantien .
En réponse au journal Le Rationalisme.
Évalué à 2 (+0/-0).
Dernière modification le 15 février 2025 à 15:30.
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. ;-)
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.
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.
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.
Déjà, comme dit dans un autre commentaire, ce que tu décris n'a absolument rien à voir avec le projet de Kant dans sa Critique de la raison pure. Si tu veux connaître son avis sur les probabilités, l'induction et le rasoir d'Ockham, ça se trouve dans son traité sur la Logique.
Nous avons observé plus haut, touchant la probabilité, qu’elle n’est qu’une simple approximation de la certitude. — Tel est aussi, et en particulier, le cas avec les hypothèses, au moyen desquelles nous ne pouvons jamais parvenir, dans notre connaissance, à une certitude apodictique, mais toujours seulement à un degré de probabilité tantôt plus grand, tantôt moindre.
Une hypothèse est une croyance du jugement touchant la vérité d’un principe, eu égard à la
suffisance des conséquences ; ou, plus brièvement, la croyance d’une supposition comme principe.
Toute croyance se fonde donc sur une hypothèse, en ce sens que la supposition, comme principe, est suffisante pour expliquer par là d’autres connaissances comme conséquences ; car on conclut ici de la vérité de la conséquence à la vérité du principe. Mais cette espèce de conclusion ne donne pas un critérium suffisant de la vérité, et ne peut conduire à une certitude apodictique qu’autant que toutes les conséquences possibles d’un principe admis sont vraies ; d’où il suit que, comme nous ne pouvons jamais déterminer toutes les conséquences possibles, les hypothèses restent toujours des hypothèses, c’est-à-dire des suppositions, à la pleine certitude desquelles nous ne pouvons jamais atteindre. — Cependant, la vraisemblance d’une hypothèse peut croître et s’élever, et la foi que nous lui accordons, devenir analogue à celle que nous donnons à la certitude, lorsque toutes les conséquences qui se sont présentées à nous jusqu’ici peuvent s’expliquer par le principe supposé ; car alors il n’y a pas de raison pour que nous ne devions pas admettre que toutes les conséquences possibles qui en dérivent peuvent également s’expliquer. Nous regardons alors l’hypothèse comme très certaine, quoiqu’elle ne le soit que par induction.
Quelque chose cependant doit être certain apodictiquement dans toute hypothèse, savoir :
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.
2° La conséquence.
Les conséquences doivent découler légitimement du principe admis, autrement l’hypothèse n’aurait enfanté qu’une chimère.
3° L’unité.
Une chose essentielle pour une hypothèse, c’est qu’elle soit une, et qu’elle n’ait pas be-
soin d’hypothèses auxiliaires pour la soutenir. Si une hypothèse ne pouvait subsister par elle-même, elle perdrait par ce fait beaucoup de sa probabilité; car, plus une hypothèse est féconde en conséquences, plus elle est probable, et réciproquement. C’est ainsi que l’hypothèse principale de Ticho-Brahé ne suffisait pas pour expliquer beaucoup de phénomènes, ce qui rendait nécessaires plusieurs autres hypothèses secondaires. On pouvait déjà présumer par là que l’hypothèse adoptée n’était pas un principe légitime. Au contraire, le système de Copernic est une hypothèse qui explique tout ce qu’elle doit expliquer, tous les grands phénomènes cosmiques qui se sont présentés à nous jusqu’ici ; nous n’avons pas besoin d’hypothèses subsidiaires.
Il est des sciences qui ne permettent aucune hypothèse, par exemple les mathématiques et la métaphysique. Mais en physique elles sont utiles et indispensables.
Kant, Logique.
Lorsqu'il dit que nous concluons de la vérité des conséquences (faits observés) à la vérité du principe, il dit que nous concluons par abduction ce qui n'est pas un principe logique valide, mais acceptable, voire nécessaire, dans la connaissance expérimentale et c'est sur cela que repose l'induction. Ce qui n'exclue pas la nécessité d'une certaine certitude, d'où les trois critères qui suivent : le premier visant à limiter les délires de l'imagination, le second exigeant que la majeur du raisonnement abductive soit certaine, et enfin le troisième n'étant que le rasoir d'Ockham (chez qui peut-il faire débat ?).
Texte où l'on voit encore une fois que ce dont tu parles n'a rien à voir avec la Critique de la raison pure, son objectif dans cet livre étant de mettre la métaphysique sur le chemin sûr de la science, et, comme il le rappelle, la métaphysique n'admet aucune hypothèse tout comme les mathématiques (autant vouloir fonder les mathématiques sur des conjectures).
Après, si, de ce que je comprends, l'ukémisme-rationnailsme vise à développer ce qui est ici synthétiquement exposé, vous réinventez la roue (carrée ?). Ensuite vouloir mettre des probabilités dans tous les problèmes rencontrés au cours d'une vie relève d'une maladie que j'appellerai la mesurite aigu. Le callul 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é.
Dernière remarque en passant. Ce que tu nommes la « technique interdite Kill the Buddha », j'appelle cela tout simplement le doute radicale cartésien. Dans ses Méditations métaphysiques, Descartes commence par mettre en doute la totalité de ce qu'il pense savoir: il se trouve alors dans un état où il n'est sûr de rien. Puis, pour sortir de cet état de doute radical, il cherche un point d'appui pour douter de son doute : comme il doute de tout, et donc également de sa propre existence, il réalise qu'il doit bien exister puisqu'il faut que ce qui doute existe : les pensées qui l'occupent doivent être les pensées de quelque chose qui existe. D'où son fameux cogito ergo sum, « je pense donc je suis ». À ce stade, il est assuré d'une seule chose : il existe; mais il se pourrait bien que ce qu'il appelait réalité, antérieurement à son Kill the Buddha, n'existe point et ne soit que le fruit de son imagination. Et là on a l'argument cartésien ultime qui lui permet de sortir de son solipsisme, argument qu'à mon avis ignorent beaucoup de ceux qui se disent cartésien et rationnaliste (je ne parle pas d'ukémisme, mais de son acception philosphique par opposition à l'empirisme) : pour pouvoir se convaincre de l'existence de la réalité, il passe par une preuve de l'existence de Dieu qui dans sa grande bonté ne peut être trompeur, d'où il déduira que la réalité existe. Si c'est pas beau tout ça ! On est encore loin, et bien en aval dans la chaîne des raisons, de se poser la question de savoir comment déterminer cette réalité via l'induction et le calcul des probabilités. Tu devrais Kill the Buddha sur l'ukémisme lui même. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Si l'on regarde la séquence, il se frappe deux fois le torse au niveau du cœur puis tend la main vers le ciel, ce qui ne peut que vouloir dire « de tout mon cœur, j'irais coloniser Mars ». Puis, comme il recommence les mêmes gestes, il ajoute « et plutôt deux fois qu'une ! ».
Mais bien sûr, comme d'habitude, quand le sage montre Mars le gauchiste regarde la main.
Nous ne voyons pas d'autre explication. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par kantien .
En réponse au journal Le Rationalisme.
Évalué à 5 (+3/-0).
Dernière modification le 03 février 2025 à 17:04.
[il] faut aller chercher pour trouver des observations qui nécessitent la théorie de la relativité générale pour être expliquées ?
Il me semble que pour le bon fonctionnement du système GPS il est nécessaire de prendre en compte l'influence du champ de gravitation sur la marche des horloges (le temps ne s'écoule pas de la même façon pour le satellite et le récepteur sur terre).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
J'en doute fortement. Après une lecture régulière et approfondie de l'ouvrage depuis plus de 25 ans, je pense pouvoir affirmer que je l'ai compris. Compréhension que ne semble pas posséder l'auteur du journal. Quiconque a lu le livre sait pertinemment que tout recours à la psychologie ou au probabilité, pour aborder les problèmes qu'il y traite, doit être considéré comme nul et non avenu d'un point de vue méthodologique. Kant ne pouvait être on ne peut plus explicite là-dessus dans sa préface à la première édition :
Pour ce qui est de la certitude, voici la loi que je me suis imposée à moi-même : dans cet ordre de considérations, l’opinion est absolument proscrite, et tout ce qui ressemble à une hypothèse est une marchandise prohibée qui ne doit être mise en vente à aucun prix, mais qu’on doit saisir dès qu’on la découvre. En effet, toute connaissance qui a un fondement à priori est marquée de ce caractère, qu’elle veut être tenue pour absolument nécessaire ; à plus forte raison en doit-il être ainsi d’une détermination de toutes les connaissances pures à priori qui doit servir elle-même de mesure et d’exemple à toute certitude apodictique (philosophique).
Kant, Critique de la Raison Pure
Autrement dit, toute proposition dont la mesure de probabilité n'est pas égale à l'unité (certitude apodictique) doit être proscrite dans toute entreprise de cette sorte.
J'avais pour projet, au départ, de faire une commentaire plus long après la lecture du journal pour réagir sur ce qu'il y dit sur Kant :
L’Ukemisme n’est pas un ensemble de conclusion philosophiques comme pourrait l’être, par exemple, le Kantisme.
Le kantisme est plus une méthode d'investigation philosophique qu'un ensemble de conclusions (bien qu'il y ait, dans l'ensemble de l'œuvre critique, des solutions que Kant considérait comme définitives à des problèmes métaphysiques légués par la tradition). Je verrai si je trouve le temps de développer le sujet, tout en le mettant en rapport avec le problème de l'arrêt, l'IA et l'analyse formelle de code informatique (preuves assistées par ordinateur, type checking, raisonnement automatique…) pour traiter de sujets plus familiés au lectorat du site.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Même au-delà de mon exemple, il y a un point fondamental en mathématique : toutes les valeurs sont immuables et vivent, pour ainsi dire, dans le monde Platonicien des idées. D'où ma référence à Haskell où tout est immuable et qui nécessite la monade IO pour faire des entrées sorties.
Mais de manière générale, la mutabilité est une source d'emmerdes sans nom dont on n'a rarement besoin, si ce n'est pour des raisons de performances en programmation bas niveau. Et dans ce cas, mieux vaut du Rust qui contrôle cela via le borrowing et le lifetime. Raisonner, sans erreur, avec des choses mutables sur une large échelle est une gageure.
Ensuite, mon expérience m'a appris que les programmeurs ne comprennent pas toujours réellement les structures qu'ils manipulent, en particulier avec la POO (qui se représente réellement un objet comme une paire constituée d'une algèbre et d'une valeur de son support ? ce qu'il est pourtant réellement).
Enfin, l'algorithmie est bien une branche des mathématiques. Pour l'anecdote, et en revenir à Platon (cf. le dialogue du Ménon), la première crise des mathématiques remonte à l'antiquité et concernait un problème de non terminaison d'un algorithme. Algorithme qui pour nous termine toujours, les pythagoriciens pensaient qu'il devait aussi en être ainsi mais ils ont trouvé un cas de non terminaison qui les laissa perplexe. Je veux parler de l'algorithme d'Euclide pour le calcul du plus petit diviseur commun. Il s'en servait pour trouver la commune mesure entre deux grandeurs géométriques, jusqu'à ce qu'il l'essaye sur un carré et sa diagonale. La non terminaison signifiant l'irrationalité de racine de 2. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui, cela doit dépendre des langages qu'on leur enseigne et comment l'on s'y prend. J'aimerai bien voir un esprit non matheux faire du Haskell ! Rien que pour faire des entrées-sorties, il faut déjà passer par la monade IO. Heu ? C'est quoi une monade ? C'est simple, c'est juste un monoïde dans la catégorie des enfodoncteurs ! :-D
Sinon, on fait comment pour traduire naturellement les concepts de bases de l'algèbre en OCaml ? C'est simple :
(* un concept mathématique est un type dans les cas des structures, ce sont des modules*)moduletypeGroupe=sigtypetvalzero:tvaladd:t->t->tvalneg:t->tendmoduletypeAnneau=sigincludeGroupevalone:tvalmul:t->t->tend(* maintenant on définit le polynôme `x² + x + 1` *)letpoly(typea)(moduleR:Anneauwithtypet=a)x=let(+),(*)=R.(add,mul)inx*x+x+R.one(* on l'utilise sur différents anneaux *)poly(moduleInt)5;;-:int=31poly(moduleFloat)5.4;;-:float=35.56(* la notion d'anneau produit *)moduleProd(R:Anneau)(S:Anneau):Anneauwithtypet=R.t*S.t=structtypet=R.t*S.tletzero=(R.zero,S.zero)letone=(R.one,S.one)letadd(x,y)(x',y')=(R.addxx',S.addyy')letmul(x,y)(x',y')=(R.mulxx',S.mulyy')letneg(x,y)(x',y')=(R.negxx',S.negyy')end(* utilisation *)poly(moduleProd(Int)(Float))(5,5.4);;-:int*float=(31,35.56)
Bon, la syntaxe est un peu lourde pour définir le polynôme, mais bientôt on pourra se contenter de:
letpoly(R:Anneau)x=...
En Haskell, on passerait par des types classes avec une syntaxe plus légère et il ne serait même pas nécessaire de passer explicitement l'anneau en paramètre lors de l'appel de fonction. En Rust, ce serait avec des Traits avec une syntaxe aussi lourde et sans instantiation explicite de l'anneau.
On peut ensuite continuer la hiérarchie des structures algébriques:
On fait comment dans les autres langages pour formaliser tout ça ? Le premier qui me propose un idiome de POO (comme en C++ ou Python), je l'envoie au piquet et lui demande de retourner étudier l'algèbre ! :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Tu n'es pas le seul à trouver qu'il y a une forme d'essentialisation des genres dans l'argumentaire de l'article (je rajouterai son allusion à la pratique du tricot, clin d'œil à Ysabeau, que j'ai moi même pratiqué sans me sentir attaquer dans ma masculinité et que l'on peut relier, mathématiquement, à la théories des nœuds qui est une branche de la topologie). Mais, si on laisse cela de côté, il y a des remarques intéressantes sur l'organisation et les sujets mis en valeur dans la communauté de recherche sur les langages des programmation. Pour y voir plus clair, voici des réactions de membres masculins de l'école mainstream (formalisme mathématique) de cette communauté sur le forum OCaml.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Pour le reste désolé mais je suis pas d'attaque pour ce genre de lecture ce soir
C'est pas un texte compliqué, il est même très simple à comprendre. Ce n'est pas comme si je te demandais de lire tout le traité des Harmonies Économiques dont il est extrait. Le texte permet de mieux comprendre le point de vue et le rapport entre celui qui produit un bien ou un service et celui qui le reçoit. ;-)
Une entreprise qui utilise un logiciel libre, potentiellement d'ailleurs pour packager le tout dans un logiciel proprio, n'est pas la définition d'un "consommateur". Pourtant c'est toujours dans l'objet du site.
C'est toujours une personne (physique ou morale) qui reçoit un produit de la part d'autrui. Qu'elle l'utilise seulement pour elle-même ou s'en sert comme moyen de production pour ses propres service ne changent rien à l'affaire. Qu'un maraîcher vende sa production à une personne qui cuisine pour elle ou à un restaurant ne change rien : ils sont les destinataires du service fourni par le maraîcher, qui est libre de les fournir à ses conditions, tout comme l'auteur d'un logiciel libre.
On peut arguer que l'aspect "partage des connaissances" qui fait partie du libre n'est pas une histoire de consommation au sens strict, d'ailleurs.
Certes, mais comme précisé au-dessus, le sens du mot consommateur était pris dans un sens beaucoup plus large que celui auquel tu veux le restreindre. D'ailleurs, dans son texte, Bastiat parle de l'écrivain comme personne dont la fonction est de vaincre l'obstacle appelé ignorance. ;-)
Le logiciel libre (version FSF) comporte certes, de mon point vue, une supériorité morale dans sa manière de promouvoir le partage de la connaissance; mais ce n'est pas à ce point de vue là, mais au plan juridique que je préfère me positionné pour le coup. Pour plus de complément sur la distinction, voir l'analyse critique, par Jules Barni, de la doctrine du droit de Kant (bon là, c'est beaucoup plus long et compliqué que le petit texte de Bastiat :-D).
On peut critiquer Starlink sur bien des points, mais certainement pas de la façon dont le fait le thread mastodon qui se permet de regretter que sur « l’île du Désespoir la terre ne soit pas plus ingrate, la source plus éloignée, le soleil moins longtemps sur l’horizon. Pour se nourrir, s’abreuver, s’éclairer, Robinson aurait plus de peine à prendre : il serait plus riche. » ;-)
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 (+0/-0).
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: Pour la complétude, j'ajoute le couple SPARK/Ada
Posté par kantien . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 3 (+1/-0).
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 :
est la version impérative du typage de la composition de fonction dans les langages fonctionnels (
('p -> 'q) -> ('q -> 'r) -> 'p -> 'rdans 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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2 (+0/-0).
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.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2 (+0/-0).
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2 (+0/-0).
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2 (+0/-0).
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2 (+0/-0).
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 :
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 :
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
Pet un théorèmeTet qui vérifie siPest bien une preuve deTet 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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 1 (+0/-1).
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 0 (+0/-2). Dernière modification le 03 mars 2025 à 15:19.
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 0 (+0/-2). Dernière modification le 03 mars 2025 à 14:42.
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.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 4 (+2/-0). Dernière modification le 02 mars 2025 à 21:42.
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.
[^] # Re: Pas si pas clair
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 2 (+0/-0). Dernière modification le 15 février 2025 à 15:30.
C'est bien ce que je disais tu n'écoutes pas et tu interprètes de travers.
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.
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.
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 * 1080avec 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
nle pixel aux coordonnéesxetyserap» (oùpest 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 :
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 :
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.
[^] # Re: Pas si pas clair
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 2 (+0/-0).
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é à
ncoté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 toujours180degré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 :
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.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 2 (+0/-0).
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.
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 :
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 :
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 :
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.
[^] # Re: Est-ce informatif?
Posté par kantien . En réponse au lien Quelle est réellement la fortune de Bernard Arnault ?. Évalué à 4 (+2/-0).
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.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 3 (+1/-0).
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 :
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.
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.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 5 (+3/-0).
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.
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 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.
Ce texte est ridicule, je n'ai pas pu aller jusqu'au bout. Je me suis arrêté ici :
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 :
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 :
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.
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.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 5 (+3/-0).
Cela me semble être de la philosophie douteuse.
Déjà, comme dit dans un autre commentaire, ce que tu décris n'a absolument rien à voir avec le projet de Kant dans sa Critique de la raison pure. Si tu veux connaître son avis sur les probabilités, l'induction et le rasoir d'Ockham, ça se trouve dans son traité sur la Logique.
Lorsqu'il dit que nous concluons de la vérité des conséquences (faits observés) à la vérité du principe, il dit que nous concluons par abduction ce qui n'est pas un principe logique valide, mais acceptable, voire nécessaire, dans la connaissance expérimentale et c'est sur cela que repose l'induction. Ce qui n'exclue pas la nécessité d'une certaine certitude, d'où les trois critères qui suivent : le premier visant à limiter les délires de l'imagination, le second exigeant que la majeur du raisonnement abductive soit certaine, et enfin le troisième n'étant que le rasoir d'Ockham (chez qui peut-il faire débat ?).
Texte où l'on voit encore une fois que ce dont tu parles n'a rien à voir avec la Critique de la raison pure, son objectif dans cet livre étant de mettre la métaphysique sur le chemin sûr de la science, et, comme il le rappelle, la métaphysique n'admet aucune hypothèse tout comme les mathématiques (autant vouloir fonder les mathématiques sur des conjectures).
Après, si, de ce que je comprends, l'ukémisme-rationnailsme vise à développer ce qui est ici synthétiquement exposé, vous réinventez la roue (carrée ?). Ensuite vouloir mettre des probabilités dans tous les problèmes rencontrés au cours d'une vie relève d'une maladie que j'appellerai la mesurite aigu. Le callul 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é.
Dernière remarque en passant. Ce que tu nommes la « technique interdite Kill the Buddha », j'appelle cela tout simplement le doute radicale cartésien. Dans ses Méditations métaphysiques, Descartes commence par mettre en doute la totalité de ce qu'il pense savoir: il se trouve alors dans un état où il n'est sûr de rien. Puis, pour sortir de cet état de doute radical, il cherche un point d'appui pour douter de son doute : comme il doute de tout, et donc également de sa propre existence, il réalise qu'il doit bien exister puisqu'il faut que ce qui doute existe : les pensées qui l'occupent doivent être les pensées de quelque chose qui existe. D'où son fameux cogito ergo sum, « je pense donc je suis ». À ce stade, il est assuré d'une seule chose : il existe; mais il se pourrait bien que ce qu'il appelait réalité, antérieurement à son Kill the Buddha, n'existe point et ne soit que le fruit de son imagination. Et là on a l'argument cartésien ultime qui lui permet de sortir de son solipsisme, argument qu'à mon avis ignorent beaucoup de ceux qui se disent cartésien et rationnaliste (je ne parle pas d'ukémisme, mais de son acception philosphique par opposition à l'empirisme) : pour pouvoir se convaincre de l'existence de la réalité, il passe par une preuve de l'existence de Dieu qui dans sa grande bonté ne peut être trompeur, d'où il déduira que la réalité existe. Si c'est pas beau tout ça ! On est encore loin, et bien en aval dans la chaîne des raisons, de se poser la question de savoir comment déterminer cette réalité via l'induction et le calcul des probabilités. Tu devrais Kill the Buddha sur l'ukémisme lui même. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Un point Godwin, et sa justification
Posté par kantien . En réponse au journal Facebook bloque les news sur Linux pour "menace pour la cybersécurité". Évalué à 2 (+2/-2).
Vous êtes de mauvaise foi.
Si l'on regarde la séquence, il se frappe deux fois le torse au niveau du cœur puis tend la main vers le ciel, ce qui ne peut que vouloir dire « de tout mon cœur, j'irais coloniser Mars ». Puis, comme il recommence les mêmes gestes, il ajoute « et plutôt deux fois qu'une ! ».
Mais bien sûr, comme d'habitude, quand le sage montre Mars le gauchiste regarde la main.
Nous ne voyons pas d'autre explication. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 5 (+3/-0). Dernière modification le 03 février 2025 à 17:04.
Il me semble que pour le bon fonctionnement du système GPS il est nécessaire de prendre en compte l'influence du champ de gravitation sur la marche des horloges (le temps ne s'écoule pas de la même façon pour le satellite et le récepteur sur terre).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Verbiage…
Posté par kantien . En réponse au journal Le Rationalisme. Évalué à 4 (+2/-0).
J'en doute fortement. Après une lecture régulière et approfondie de l'ouvrage depuis plus de 25 ans, je pense pouvoir affirmer que je l'ai compris. Compréhension que ne semble pas posséder l'auteur du journal. Quiconque a lu le livre sait pertinemment que tout recours à la psychologie ou au probabilité, pour aborder les problèmes qu'il y traite, doit être considéré comme nul et non avenu d'un point de vue méthodologique. Kant ne pouvait être on ne peut plus explicite là-dessus dans sa préface à la première édition :
Autrement dit, toute proposition dont la mesure de probabilité n'est pas égale à l'unité (certitude apodictique) doit être proscrite dans toute entreprise de cette sorte.
J'avais pour projet, au départ, de faire une commentaire plus long après la lecture du journal pour réagir sur ce qu'il y dit sur Kant :
Le kantisme est plus une méthode d'investigation philosophique qu'un ensemble de conclusions (bien qu'il y ait, dans l'ensemble de l'œuvre critique, des solutions que Kant considérait comme définitives à des problèmes métaphysiques légués par la tradition). Je verrai si je trouve le temps de développer le sujet, tout en le mettant en rapport avec le problème de l'arrêt, l'IA et l'analyse formelle de code informatique (preuves assistées par ordinateur, type checking, raisonnement automatique…) pour traiter de sujets plus familiés au lectorat du site.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Pas mieux
Posté par kantien . En réponse au lien Apprendre la programmation en Python n'est pas plus facile qu'en Java ou en C++. Évalué à 5.
Même au-delà de mon exemple, il y a un point fondamental en mathématique : toutes les valeurs sont immuables et vivent, pour ainsi dire, dans le monde Platonicien des idées. D'où ma référence à Haskell où tout est immuable et qui nécessite la monade IO pour faire des entrées sorties.
Mais de manière générale, la mutabilité est une source d'emmerdes sans nom dont on n'a rarement besoin, si ce n'est pour des raisons de performances en programmation bas niveau. Et dans ce cas, mieux vaut du Rust qui contrôle cela via le
borrowinget lelifetime. Raisonner, sans erreur, avec des choses mutables sur une large échelle est une gageure.Ensuite, mon expérience m'a appris que les programmeurs ne comprennent pas toujours réellement les structures qu'ils manipulent, en particulier avec la POO (qui se représente réellement un objet comme une paire constituée d'une algèbre et d'une valeur de son support ? ce qu'il est pourtant réellement).
Enfin, l'algorithmie est bien une branche des mathématiques. Pour l'anecdote, et en revenir à Platon (cf. le dialogue du Ménon), la première crise des mathématiques remonte à l'antiquité et concernait un problème de non terminaison d'un algorithme. Algorithme qui pour nous termine toujours, les pythagoriciens pensaient qu'il devait aussi en être ainsi mais ils ont trouvé un cas de non terminaison qui les laissa perplexe. Je veux parler de l'algorithme d'Euclide pour le calcul du plus petit diviseur commun. Il s'en servait pour trouver la commune mesure entre deux grandeurs géométriques, jusqu'à ce qu'il l'essaye sur un carré et sa diagonale. La non terminaison signifiant l'irrationalité de racine de 2. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Pas mieux
Posté par kantien . En réponse au lien Apprendre la programmation en Python n'est pas plus facile qu'en Java ou en C++. Évalué à 1. Dernière modification le 11 décembre 2024 à 09:40.
Oui, cela doit dépendre des langages qu'on leur enseigne et comment l'on s'y prend. J'aimerai bien voir un esprit non matheux faire du Haskell ! Rien que pour faire des entrées-sorties, il faut déjà passer par la monade IO. Heu ? C'est quoi une monade ? C'est simple, c'est juste un monoïde dans la catégorie des enfodoncteurs ! :-D
Sinon, on fait comment pour traduire naturellement les concepts de bases de l'algèbre en OCaml ? C'est simple :
Bon, la syntaxe est un peu lourde pour définir le polynôme, mais bientôt on pourra se contenter de:
En Haskell, on passerait par des types classes avec une syntaxe plus légère et il ne serait même pas nécessaire de passer explicitement l'anneau en paramètre lors de l'appel de fonction. En Rust, ce serait avec des Traits avec une syntaxe aussi lourde et sans instantiation explicite de l'anneau.
On peut ensuite continuer la hiérarchie des structures algébriques:
On fait comment dans les autres langages pour formaliser tout ça ? Le premier qui me propose un idiome de POO (comme en C++ ou Python), je l'envoie au piquet et lui demande de retourner étudier l'algèbre ! :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: serait il possible de m'expliquer
Posté par kantien . En réponse au lien Feminism in Programming Language Design. Évalué à 2.
Tu n'es pas le seul à trouver qu'il y a une forme d'essentialisation des genres dans l'argumentaire de l'article (je rajouterai son allusion à la pratique du tricot, clin d'œil à Ysabeau, que j'ai moi même pratiqué sans me sentir attaquer dans ma masculinité et que l'on peut relier, mathématiquement, à la théories des nœuds qui est une branche de la topologie). Mais, si on laisse cela de côté, il y a des remarques intéressantes sur l'organisation et les sujets mis en valeur dans la communauté de recherche sur les langages des programmation. Pour y voir plus clair, voici des réactions de membres masculins de l'école mainstream (formalisme mathématique) de cette communauté sur le forum OCaml.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: anti-tout
Posté par kantien . En réponse au lien petit écart vers le succès de Starlink dans certains territoires isolés, et son impact sur les commu. Évalué à 2. Dernière modification le 18 octobre 2024 à 18:18.
C'est pas un texte compliqué, il est même très simple à comprendre. Ce n'est pas comme si je te demandais de lire tout le traité des Harmonies Économiques dont il est extrait. Le texte permet de mieux comprendre le point de vue et le rapport entre celui qui produit un bien ou un service et celui qui le reçoit. ;-)
C'est toujours une personne (physique ou morale) qui reçoit un produit de la part d'autrui. Qu'elle l'utilise seulement pour elle-même ou s'en sert comme moyen de production pour ses propres service ne changent rien à l'affaire. Qu'un maraîcher vende sa production à une personne qui cuisine pour elle ou à un restaurant ne change rien : ils sont les destinataires du service fourni par le maraîcher, qui est libre de les fournir à ses conditions, tout comme l'auteur d'un logiciel libre.
Certes, mais comme précisé au-dessus, le sens du mot consommateur était pris dans un sens beaucoup plus large que celui auquel tu veux le restreindre. D'ailleurs, dans son texte, Bastiat parle de l'écrivain comme personne dont la fonction est de vaincre l'obstacle appelé ignorance. ;-)
Le logiciel libre (version FSF) comporte certes, de mon point vue, une supériorité morale dans sa manière de promouvoir le partage de la connaissance; mais ce n'est pas à ce point de vue là, mais au plan juridique que je préfère me positionné pour le coup. Pour plus de complément sur la distinction, voir l'analyse critique, par Jules Barni, de la doctrine du droit de Kant (bon là, c'est beaucoup plus long et compliqué que le petit texte de Bastiat :-D).
On peut critiquer Starlink sur bien des points, mais certainement pas de la façon dont le fait le thread mastodon qui se permet de regretter que sur « l’île du Désespoir la terre ne soit pas plus ingrate, la source plus éloignée, le soleil moins longtemps sur l’horizon. Pour se nourrir, s’abreuver, s’éclairer, Robinson aurait plus de peine à prendre : il serait plus riche. » ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.