Agrégateur de nouvelles

L'association Root66 vous propose une permanence Logiciels Libres

A cette permanence, tu pourras bénéficier d'une aide et d'un accompagnement pour t'aider à installer, configurer des logiciels libres aussi bien sur PC que sur Smartphones.
Un vieux pc qui rame? Besoin de faire une sauvegarde de tes données? Envie de tester des applications opensource sur ton téléphone ou sur ton pc mais tu as peur de tout casser et de ne pas y arriver seul.e. Pas de souci, l'équipe de root66 est là pour t'accompagner, à ton propre rythme!

Un des objectifs est de t'aider à reprendre le contrôle de tes données et d'apprendre pas à pas les bonnes pratiques à adopter pour sécuriser et améliorer ta vie privée numérique.

N'hésite pas à passer! L'équipe de root66 sera ravie de t'accueillir! 

« Arrêtez de donner à Wokepedia jusqu'à ce qu'ils rétablissent l'équilibre dans leur autorité éditoriale », avait déclaré il y a quelques semaines Elon Musk sur son réseau social X. Entre le milliardaire et Wikipédia, il n'y a pas à dire, la guerre est déclarée. Si ce n'est pas la première fois qu'il s'en prend à l'encyclopédie en ligne, il n'est surtout pas le seul…
Delphine Sabattier : Attaques en règle d'Elon Musk, chambardement avec l'intelligence artificielle et les colères de (…)

- Transcriptions / Serge Abiteboul, Delphine Sabattier, Rémy Gerbet, Communs numériques, Wikipédia, Institutions, Conférence, Vidéo

Louise Tourret : Bonjour et bienvenue dans Être et savoir, le magazine de l'éducation de France Culture. Peire Legras à la réalisation de cette émission, Dalia en assure la prise de son et Avril Ventura collabore à sa préparation. L'intelligence artificielle générative à l'école : faut-il s'en méfier et/ou s'en saisir ?
Les 10 et 11 février 2025 se tiendra à Paris un grand Sommet pour l'action sur l'intelligence artificielle. Il réunira des chefs d'État et des chefs de gouvernement, des (…)

- Transcriptions / Orianne Ledroit, Axel Jean, Mickaël Bertrand, Louise Tourret, Intelligence artificielle, Éducation, Entreprises, Conférence, Audio

Atel'libre | Jerripartie

Samedi 01 mars 2025 de 10h00 à 14h00
EPF Montpellier - 21, boulevard Berthelot, 34000 Montpellier
JPO EPF | Jerripartie, montez vous-même votre ordinateur et repartez avec
En partenariat avec MAIF, API : Action of Public Interest, Docteur PC, Ayiyikoh, Blolab, Emmabuntüs, JMSI, Lilo, Montpel’libre, Ovillage, Senfablab, Ubunteam, YovoTogo, Youthlead.
Inscriptions nécessaires, places limitées | Photos | GPS

Montpel’libre vous montrera comment construire un ordinateur soi-même à partir de matériels reconditionnés.

Après une brève présentation réalisée par API : Action d'Intérêt Collectif, sur les enjeux en terme de développement durable des jerriparties, et les innovations réalisées grâce à elles en Afrique, l’atelier de Montpel’libre commence.

Il consiste à ouvrir un jerrican, et y recomposer une tour en prenant des composants qui fonctionnent d’ordinateurs mis au rebus. On s’affranchit ainsi des brevets posés sur les châssis.

Une fois le jerri terminé, on lui branche un écran, un clavier, une souris et on lui intègre Emmabuntüs, un système d’exploitation pour ordinateur de bureau, facile d’accès et prêt à l’emploi, libre éthique, durable et responsable.

On a alors un ordinateur transportable avec lequel repart la personne qui l’a réalisé. Il lui revient de le décorer, d’en prendre une photo, de nous l’envoyer et de lui donner un nom. Tous les mois, le plus beau jerri est élu.

 

Le matériel (ordinateur, clavier, souris, écran) et logiciel pour monter 3 ordinateurs sont fournis par l’association Montpel’libre et offerts à 3 participants, idéalement des familles.

Une Jerryparty, c’est du Do It Together: un véritable acte d’intelligence collective, qui tire son énergie d’un savoir collaboratif: chacun apporte ses compétences, son savoir-faire, son temps au projet. Cette activité s’inscrit pleinement dans l’écoresponsabilité, car elle réutilise des objets, jerricans, ordinateurs…

Elle permet de sensibiliser le public, de façon ludique, à l'importance de l'éducation numérique, de la maîtrise des outils informatiques, d’éviter l’obsolescence programmée matérielle et logicielle, de reconditionner le matériel informatique, d’utiliser des logiciels libres…

C’est pourquoi, en 2023, Montpel’libre a reçu le Prix du Fonds MAIF pour l’Éducation dont l’objectif est de faire connaître et récompenser des initiatives d'associations permettant l’accès à l’éducation, de récompenser des actions innovantes et originales favorisant le partage de la connaissance. Ces actions, d’intérêt général à vocation éducative, concernent prioritairement un public défavorisé du fait, par exemple, d’un handicap ou d’une situation sociale difficile.

Places limitées, inscription nécessaire | GPS 43.60023/3.87136

Ces derniers temps, on a beaucoup parlé d’intelligence artificielle sur LinuxFr.org. D’IA propriétaires, et d’IA libres. Mais peut-on vraiment faire une IA libre ? La notion n’est pas sans poser quelques difficultés. Une (pas si) courte discussion du problème.

Sommaire

• On appellera IA un réseau de neurones artificiels
• Pour comprendre le réseau de neurones, il est nécessaire de disposer de bases statistiques
  • Les statistiques reposent sur la modélisation
    • Un exemple : la régression linéaire
• Le réseau de neurones
  • Le neurone naturel
  • Le neurone formel
  • La mise en réseau
  • Le réseau de neurones est Turing-complet
  • Le réseau de neurones présente un effet boîte noire important
  • Le réseau de neurones est un modèle statistique
    • Tous les modèles sont faux, certains sont utiles, et c’est vrai aussi pour le réseau de neurones
• Le but du logiciel libre est de rendre le pouvoir à l’utilisateur
  • La première des libertés est celle de savoir ce que je fais
  • Si je sais ce que je fais, je dois pouvoir modifier ce que je fais
• Le réseau de neurones est difficilement compatible avec le libre
  • Personne ne sait vraiment ce que fait un réseau de neurones
  • Disposer de la description complète d’un réseau de neurones ne permet pas de l’améliorer
  • La définition du code source d’un réseau de neurones est ambiguë
  • Cette ambiguïté fait courir un risque juridique sous certaines licences libres
    • Comment les boîtes qui font de l’IA non libre résolvent-elles ce dilemme ? Elles ne le résolvent pas
  • La définition d’une IA open source ressemble furieusement à un constat d’échec
• Conclusion : qu’attendre d’une IA libre ?

On appellera IA un réseau de neurones artificiels

Commençons par définir notre objet d’étude : qu’est-ce qu’une IA ? Par « intelligence artificielle », on pourrait entendre tout dispositif capable de faire réaliser par un ordinateur une opération réputée requérir une tâche cognitive. Dans cette acception, un système expert qui prend des décisions médicales en implémentant les recommandations d’une société savante est une IA. Le pilote automatique d’un avion de ligne est une IA.

Cependant, ce n’est pas la définition la plus couramment employée ces derniers temps. Une IA a battu Lee Sedol au go, mais ça fait des années que des ordinateurs battent les humains aux échecs et personne ne prétend que c’est une IA. Des IA sont employées pour reconnaître des images alors que reconnaître un chien nous semble absolument élémentaire, mais l’algorithme de Youtube qui te suggère des vidéos pouvant te plaire parmi les milliards hébergées fait preuve d’une certaine intelligence et personne ne l’appelle IA. Il semble donc que le terme « IA » s’applique donc à une technique pour effectuer une tâche plus qu’à la tâche en elle-même, ou plutôt à un ensemble de techniques partageant un point commun : le réseau de neurones artificiels.

Dans la suite de cette dépêche, j’utiliserai donc indifféremment les termes d’IA et de réseau de neurones1.

Pour comprendre le réseau de neurones, il est nécessaire de disposer de bases statistiques

Les statistiques (ou la statistique, on peut dire les deux, comme en Alexandrie), c’est la branche des mathématiques qui s’intéresse aux moyens, à partir de données observées et fondamentalement probabilistes, d’en tirer des conclusions généralisables (et idéalement, de prédire l’avenir à partir du passé).

La data science, c’est la branche de l’informatique qui s’intéresse aux moyens, à partir de données emmagasinées sur lesquelles on ne fait pas d’hypothèse de mode de génération, d’en tirer des conclusions généralisables (et idéalement, de prédire les données futures).

Ça vous semble similaire ? Ça l’est. Les deux champs vont avoir des divergences de vocabulaire, de langages (les stateux préfèreront R, les data scientists Python), de formation (les stateux sont plutôt des universitaires, les data scientists plutôt des informaticiens au niveau licence, mais ils ont les mêmes masters et doctorats), mais fondamentalement, et surtout mathématiquement, c’est la même chose. Les connaissances en inférence statistique (notamment bayésienne, pour ceux à qui ça parle) se généralisent très bien à la data science.

Pour faire court, un statisticien est un data scientist qui se la pète, alors qu’un data scientist est un informaticien qui, n’étant pas assez bon pour survivre à la rude concurrence universitaire, a multiplié son salaire par 10 ou 20 en allant vendre ses compétences statistiques à Facebook.

Les statistiques reposent sur la modélisation

En statistique, la manière la plus courante de répondre à une question est de construire un modèle. Prenons une question simple : je dispose d’un jeu de données où j’ai enregistré, pour 1000 personnes, leur IMC et leur taux de cholestérol. Je souhaite savoir s’il y a un lien entre les deux. On souhaiterait, dans ce cas simple, rechercher une relation monotone, sans faire d’hypothèse sur le type de relation.

Un exemple : la régression linéaire

Une manière de répondre à ma question est d’écrire et de trouver les meilleurs A et B pour que la droite « colle » le mieux possible au nuage de points. On démontre que la meilleure droite est celle qui minimise un certain critère, la somme des carrés des erreurs. Une fois qu’on a la meilleure droite possible, on peut faire plein de choses avec :

• On peut rétro-prédire le taux de cholestérol des personnes déjà observées et voir de combien la prédiction s’écarte du réel, ce qui fournit une erreur moyenne de prédiction ;
• On peut faire de même en prédisant juste le taux de cholestérol moyen pour tous les individus et comparer les erreurs moyennes de prédiction, ce qui permet de voir de combien le modèle améliore la prédiction (et donc de quantifier la quantité d’info apportée par la donnée IMC sur la variable cholestérol) ;
• On peut étudier le signe de A : si A est négatif, prendre du poids fait baisser le cholestérol : si A est positif, prendre du poids augmente le cholestérol : si A est nul, le poids n’apporte pas d’info sur le cholestérol.
• Par contre, on ne peut rien dire de la causalité. Tout ce qu’on a observé, ce sont des personnes qui, au même moment, avaient un IMC et un taux de cholestérol donnés. Impossible de dire s’ils ont ce cholestérol parce qu’ils ont cet IMC, s’ils ont cet IMC parce qu’ils ont ce cholestérol, ou s’ils ont ce cholestérol et cet IMC parce qu’ils ont une troisième exposition.
• On peut enfin faire effectuer de la prédiction à notre modèle : en lui passant une personne dont on ne connaît que l’IMC, on peut estimer son taux de cholestérol et assortir cette prédiction d’un niveau de certitude (ça demande un peu plus de maths, mais c’est l’idée).

On peut vouloir ajouter une troisième variable, mettons le tabagisme. On écrira alors :

Avec la variable tabac codée à 0 (non fumeur) ou 1 (fumeur). Noter que notre modèle est alors passé en dimension 3 : on ne cherche plus à faire passer la meilleure droite par rapport au nuage de points en 2D, mais à faire passer le meilleur plan par rapport au nuage de points en 3D. Noter aussi qu’on peut facilement inclure des variables qualitatives : il suffit de les coder 0 ou 1. On peut d’ailleurs inclure des variables à n modalités : il suffit de les recoder en n-1 sous-variables en 0-1 (la modalité de référence étant celle pour laquelle toutes les sous-variables sont à 0).

Les sont appelés des paramètres : c’est en les faisant varier qu’on ajuste le modèle aux données.

On peut ainsi ajouter un nombre quelconque de variables… Ou peut-être pas. En effet, on va finir par atteindre un seuil où le meilleur hyperplan est tout simplement celui qui passe par tous les points ! Si j’ai 50 individus et 50 paramètres, il est facile de choisir un plan qui passe par tous les individus. C’est ce qu’on appelle le surapprentissage : le modèle a tout simplement appris le jeu de données par cœur ! Le surapprentissage est un écueil des modèles trop complexes et un réseau de neurones est tout à fait capable de surapprendre.

Le réseau de neurones Le neurone naturel

Les neurones sont les cellules du système nerveux. Elles sont spécialisées dans la transmission d’information.

Comme tu peux le voir sur cette image issue de Wikimedia (source), un neurone comprend un nombre quelconque de dendrites, un corps cellulaire, et un axone. Point crucial : l’axone est unique. Il peut lui-même transmettre de l’information à différents neurones en aval, mais il transmet la même information. Or l’information, dans un neurone, peut entrer par les dendrites et par le corps cellulaire, mais elle ne peut ressortir que par l’axone (on peut faire abstraction de la gaine de myéline et des nœuds de Ranvier, qui ont un rôle central dans la vitesse de conduction de l’information mais qui ne changent rien aux calculs effectués). Autrement dit, un neurone transmet la même information à tous les neurones d’aval, et si ceux-ci en font un usage différent, c’est uniquement lié à leurs propres calculs en interne.

Le neurone formel

On peut modéliser un neurone, par analogie avec le neurone naturel. Notre neurone formel pourra donc prendre un nombre quelconque d’entrées, mais comme un neurone naturel, il ne produira qu’une seule sortie. Notre neurone est donc une fonction de ses entrées :

En pratique (mais ça n’a rien d’obligatoire), on prend souvent une fonction d’une combinaison linéaire des entrées :

Avec une contrainte : la fonction (qu’on appelle fonction d’activation) doit être monotone (idéalement strictement monotone), dérivable presque partout (c’est nécessaire à l’optimisation du réseau, qu’on verra plus tard), définie sur un intervalle suffisamment large pour qu’on soit toujours dedans, et non linéaire (sinon mettre les neurones en réseau n’a aucun intérêt, autant faire directement une unique régression linéaire).

En pratique, on prend donc quelques fonctions classiques :

• La fonction binaire : si , sinon
• La fonction logistique, une amélioration de la fonction binaire : . Avantage : elle est strictement monotone, dérivable partout, et elle prend quand même ses valeurs entre 0 et 1.
• La fonction Rectified Linear Unit (ReLU, qu’on peut prononcer « relou ») : si , sinon. Avantage : elle est très facile (donc rapide) à calculer et à dériver. On peut la rendre strictement monotone en la modifiant à la marge : si , sinon, avec .

La mise en réseau

Tout l’intérêt du neurone formel réside dans sa mise en réseau. Un unique neurone ne fait pas mieux qu’une régression linéaire. On construit donc un réseau de neurones. Pour ce faire, on va donc générer plusieurs neurones, chacun prenant en entrée la sortie de plusieurs neurones et produisant une sortie unique, qui sera à son tour utilisée en entrée par d’autres neurones. On ajoute un ensemble de neurones qu’on pourrait qualifier de « sensitifs », au sens où ils prennent en entrée non pas la sortie d’un neurone antérieur, mais directement l’input de l’utilisateur, ou plutôt une partie de l’input : un pixel, un mot… Enfin, une sortie est ajoutée : elle produit le résultat final.

Étant donné que les neurones sont virtuels et n’ont pas d’emplacement géographique, il est assez logique de les représenter en couches : la couche 0 est constituée des neurones sensitifs, la couche 1 prend en entrée les résultats de la couche 0, et ainsi de suite. Classiquement, tous les neurones de la couche n+1 prennent en entrée les sorties de tous les neurones de la couche n.

Se pose alors la question : combien de neurones par couche, et combien de couches au total ?
On peut considérer deux types de topologies : soit il y a plus de neurones par couche que de couches : le réseau est plus large que long, on parlera de réseau large. Soit il y a plus de couches que de neurones par couche, auquel cas le réseau est plus long que large, mais on ne va pas parler de réseau long parce que ça pourrait se comprendre « réseau lent ». On parlera de réseau profond. C’est de là que viennent les Deep et les Large qu’on voit un peu partout dans le marketing des IA. Un Large Language Model, c’est un modèle, au sens statistique, de langage large, autrement dit un réseau de neurones avec plus de neurones par couche que de couches, entraîné à traiter du langage naturel. On constate empiriquement que certaines topologies de réseau sont plus efficaces pour certaines tâches. Par exemple, à nombre de neurones constant, un modèle large fera mieux pour du langage. À l’inverse, un modèle profond fera mieux pour de la reconnaissance d’images.

Le réseau de neurones est Turing-complet

Un résultat théorique important est que les réseaux de neurones sont Turing-complets. C’est-à-dire que, pour tout programme que l’on peut coder et qui sorte une réponse algorithmique, il existe un réseau de neurones qui donne le même résultat. La réciproque est vraie aussi : ce qui est faisable avec un réseau de neurones est faisable en C ou dans un autre langage, au pire en recodant le réseau dans ce langage.

Le réseau de neurones présente un effet boîte noire important

Prenons maintenant un élément d’information et essayons de suivre son trajet dans le modèle jusqu’à la sortie. Dans une régression linéaire, c’est assez facile : le poids de l’IMC va peser pour dans le résultat final. Dans une forêt aléatoire, on peut toujours isoler les arbres où apparaît une donnée et essayer de regarder combien elle pèse. C’est fastidieux mais ça reste faisable. Dans un réseau de neurones, c’est impossible. Chaque neurone de la couche 1 va passer un résultat agrégé à la couche 2, où chaque donnée de la couche 0 ne compte plus que comme partie d’un tout. De même, chaque neurone de la couche 2 va agréger tous les résultats de la couche 1. Il devient impossible d’individualiser l’effet d’une donnée ou même celui d’un neurone.

Ainsi, même si je connais l’intégralité du contenu du modèle, il m’est impossible de donner du sens à une partie du modèle, prise isolément. Le modèle se comporte comme un bloc monolithique, et la seule manière d’étudier un nouvel exemple est de lui appliquer tout le modèle et de voir ce qui sort. C’est ce qu’on nomme l’effet boîte noire.

Attention : l’effet boîte noire n’est pas lié au nombre de paramètres du modèle. Si je fais de la génétique, et que j’étudie 2000 mutations génétiques individuelles (des SNP, pour single nucleotide polymorphism), je peux assez facilement ajuster un modèle de régression logistique (qui est une variante de la régression linéaire où on fait prédire non pas une variable quantitative, mais une probabilité) à 2000 paramètres (un pour chaque SNP). Chaque paramètre sera parfaitement compréhensible et il n’y aura pas d’effet boîte noire.

Il n’est pas non plus lié à ta méconnaissance des mathématiques, cher lectorat. Des statisticiens chevronnés se cassent les dents sur l’effet boîte noire. Il est intégralement lié à la structure du modèle. Certains types de modèles en ont, d’autres n’en ont pas. Les réseaux de neurones en ont.

Cet effet a une conséquence perturbante : même si on sait ce que fait un réseau de neurones, il est impossible de savoir comment il le fait ! On pourrait argumenter que ce n’est pas forcément différent de ce que nous faisons : si on montre à un enfant de 3 ans une photo de chien, il saura dire que c’est un chien, mais il ne saura pas dire pourquoi c’est un chien. Cependant, on demande rarement à un programme d’être réflexif, mais on demande toujours à son auteur de savoir comment il tourne. C’est un peu la base de la programmation.

Le réseau de neurones est un modèle statistique

Reprenons : on a un paradigme (le réseau de neurones) capable d’effectuer n’importe quelle tâche pour laquelle il existe une solution algorithmique, à condition de le programmer correctement… Mais on ne sait pas le programmer ! Heureusement, il existe un contournement : on ne va pas le programmer, on va l’ajuster, comme un modèle statistique. Ou l’entraîner, si on préfère le terme de « machine learning ».

Tu t’en souviens, cher lecteur, un réseau de neurones est un ensemble de fonctions dont chacune prend en entrée différentes données avec des coefficients (les fameux ). On va commencer par initialiser l’apprentissage en donnant des valeurs aléatoires à ces coefficients. Ensuite, on va soumettre à notre réseau de neurones des tas et des tas de données correctes, et qu’on va comparer ce qu’il prédit à ce qu’on attend. La différence s’appelle l’erreur. Et à chaque itération, on va identifier les neurones les plus générateurs d’erreur et les pénaliser (réduire leur poids, ou plutôt réduire leur poids dans les neurones où c’est nécessaire), tout en favorisant les meilleurs neurones. Les détails de la technique (qui s’appelle la rétropropagation de l’erreur) dépassent largement le cadre de cette courte introduction, mais l’essentiel est qu’à la fin, on obtient un réseau capable de donner des réponses proches de ce qui existait dans l’ensemble des données correctes qu’on lui a passé et de généraliser quand la demande est différente d’une donnée de l’ensemble d’apprentissage. Avantage : en pratique, un réseau de neurones est capable de prendre en entrée n’importe quel type de structure de données : image, texte, son… Tant que les neurones d’entrée sont adaptés et qu’il existe un ensemble d’apprentissage suffisamment grand, c’est bon.

Tous les modèles sont faux, certains sont utiles, et c’est vrai aussi pour le réseau de neurones

Bien sûr, il y a des limites. La première est la complexité algorithmique. Un réseau de neurones nécessite de réaliser un nombre astronomique d’opérations simples : pour chaque couche, il faut, pour chaque neurone, calculer la somme des produits des coefficients avec toutes les sorties de la couche antérieure, soit multiplications, où n est le nombre de neurones par couche et c le nombre de couches. Par exemple, pour un petit réseau de 10 couches de 20 neurones, plus une couche d’entrée, on réaliserait à chaque itération multiplications en virgule flottante, et encore, c’est ici un tout petit réseau : un réseau comme ChatGPT a des neurones qui se comptent par millions, voire dizaines de millions !

Une autre limite est la précision des réponses. Le réseau de neurones étant un modèle statistique, il n’est capable que d’interpoler, c’est-à-dire trouver une réponse à partir de cas similaires. Cette interpolation est rarement aussi précise que celle que donnerait une réponse formelle si elle existait : si Newton avait eu accès à des réseaux de neurones, nous aurions une prédiction du mouvement des planètes qui ne baserait sur aucune théorie, qui serait à peu près exacte mais insuffisamment précise pour envoyer des sondes sur Mars. Quant à s’interroger sur la précession du périhélie de Mercure, on oublie.

De manière générale, on peut s’interroger sur ce qui amène un réseau de neurones à se planter. On peut diviser les erreurs en plusieurs catégories :

• La question posée n’a aucun rapport avec les données passées en entrée. Par exemple : « Sachant que la dernière personne que j’ai croisée dans la rue avait 42 ans, indique-moi son genre ». Le modèle n’a pas assez d’information pour répondre.
• La question posée n’a aucun rapport avec l’ensemble d’apprentissage. Par exemple, demander à un modèle entraîné à reconnaître des photos de chien de reconnaître une voiture. En général, ce problème est résolu en contraignant le format des questions ; dans cet exemple, il suffirait de ne pas permettre à l’utilisateur de poser une question, juste de poster une photo et de recevoir une réponse. D’ailleurs, on ne voit pas très bien pourquoi entraîner un tel modèle à traiter du langage.
• L’ensemble d’apprentissage est trop restreint/biaisé. L’exemple typique est le modèle qui prétendait reconnaître les délinquants à une simple photo et identifiait en fait tous les noirs : ben oui, ils étaient majoritaires dans les délinquants de l’ensemble d’apprentissage. Noter qu’il existe des problèmes où l’ensemble d’apprentissage sera toujours trop restreint pour un certain niveau de précision exigé. Si on demande à un réseau de dire si un point donné est à l’intérieur ou à l’extérieur d’un flocon de Koch, il va falloir lui passer une infinité de données d’apprentissage pour qu’il apprenne les cas limites juste par interpolation (alors qu’avec un modèle formel, ça serait assez facile).
• Le modèle est parasité par une donnée annexe : c’est une problématique assez spécifique du réseau de neurones. L’exemple le plus classique est celui des images de mains : après tout, le voisin le plus probable d’un doigt, c’est un autre doigt. L’amusant, c’est que ce problème serait résolu assez facilement en demandant au modèle de compter 4 doigts et un pouce. Mais comme on ne peut pas programmer directement un réseau de neurones…
• Enfin, si les motifs précédents ont été écartés, je dois me demander si mon modèle n’est pas inadapté : soit qu’il n’a pas assez de neurones, soit que la topologie n’est pas bonne. Plus de neurones permettent de traiter des données plus complexes et leur disposition permet d’augmenter leur efficacité.

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.

Le but du logiciel libre est de rendre le pouvoir à l’utilisateur

On a beaucoup glosé, et on continuera de le faire longtemps, sur la philosophie du Libre. Free Software Foundation d’un côté, Open Source Initiative de l’autre, les sujets de discorde ne manquent pas. Mais il faut au moins créditer l’OSI sur un point : avoir clarifié le fait que le Libre est avant tout un mouvement politique, au sens noble du terme : il vise à peser sur la vie de la cité, alors que l’Open Source vise avant tout à disposer de logiciels de qualité.

La première des libertés est celle de savoir ce que je fais

Ça paraît évident dans la vie de tous les jours : je sais ce que je fais. Si je décide de prendre une pelle et de planter un arbre dans mon jardin, je sais que je suis en train de prendre une pelle et de planter un arbre dans mon jardin. Si je décide de prendre un couteau et de le planter dans le thorax de mon voisin, je sais ce que je fais. C’est une liberté fondamentale, au sens où elle fonde toutes les autres. Si je ne sais pas ce que je fais, je ne peux signer un contrat, par exemple (c’est d’ailleurs le principe qui sous-tend le régime de la tutelle en droit). D’ailleurs, comme toute liberté, elle fonde une responsabilité. Si je ne savais pas ce que je faisais (et que je peux le prouver), je peux plaider l’abolition du discernement et échapper à ma responsabilité pénale, quelle que soit l’infraction commise, même les plus graves2

Dans la vie de tous les jours, donc, il est évident que je sais ce que je fais. Mais avec un ordinateur, c’est beaucoup moins évident. Quand j’exécute Windows, je ne sais pas ce que je fais. Pas seulement parce que je ne connais pas la séquence de boot, mais de façon beaucoup plus fondamentale : parce que n’ayant pas accès au code source, je ne sais pas ce que fait le programme que j’exécute. Ce qui pose un problème majeur de confiance dans le logiciel exécuté :

• Confiance dans le fait que le programme fait bien ce que son programmeur a voulu qu’il fasse (absence de bugs)
• Confiance dans le fait que le programmeur avait bien mon intérêt en tête et pas seulement le sien (sincérité du programmeur, fréquemment prise en défaut dans le logiciel non libre)

Dans le système des 4 libertés du logiciel libre, cette liberté est la liberté 1. Elle passe après la liberté 0 (liberté d’exécuter le programme) et avant la liberté 2 (liberté de redistribuer le programme). On pourrait légitimement discuter de sa priorité par rapport à la liberté 0 (est-il raisonnable d’exécuter un programme dont on ne sait pas ce qu’il fait ?) mais ça dépasserait l’objet de cette dépêche.

Si je sais ce que je fais, je dois pouvoir modifier ce que je fais

Conséquence logique de la liberté précédente : si je n’aime pas ce que fait un programme, je dois pouvoir l’améliorer. Si je ne sais pas le faire moi-même, je dois pouvoir payer quelqu’un pour l’améliorer. Là encore, ça suppose l’accès au code source, ne serait-ce que pour savoir ce que fait le programme. Il s’agit de la liberté 3 du logiciel libre.

Le réseau de neurones est difficilement compatible avec le libre Personne ne sait vraiment ce que fait un réseau de neurones

On l’a vu, les réseaux de neurones présentent un effet boîte noire important. Déjà, la plupart des IA commerciales ne sont accessibles qu’au travers d’une interface ou une API. Elles n’exposent que rarement les neurones. Mais même pour une personne disposant de tous les neurones, autrement dit de la description complète du réseau, l’effet boîte noire est tel que le fonctionnement du réseau de neurones est inintelligible. D’ailleurs, s’il était intelligible, il serait très vite simplifié !

En effet, on peut recoder tout réseau de neurones dans un langage plus rapide, dès lors qu’on comprend ce qu’il fait (puisqu’il est Turing-complet). Vu la consommation astronomique d’énergie des réseaux de neurones, s’il existait un moyen de comprendre ce que fait un réseau de neurones et de le traduire dans un autre langage, on le ferait très vite. Ce qui fournirait d’ailleurs des réponses à des questions théoriques ouvertes comme : qu’est-ce que comprendre une phrase ? Comment reconnaît-on un chien, un visage, un avion ?

Disposer de la description complète d’un réseau de neurones ne permet pas de l’améliorer

On l’a vu : si je dispose de la totalité des neurones, je dispose de la totalité de la description du réseau de neurones. Mais comme je suis incapable de savoir ce qu’il fait, je ne suis pas plus avancé pour l’améliorer, qu’il s’agisse de retirer un défaut ou d’ajouter une fonctionnalité. Noter d’ailleurs que ceci n’est pas forcément impactant de la même manière pour tous les aspects du réseau de neurones : si je n’ai aucun moyen d’être sûr de l’absence de bugs (c’est même le contraire ! Il y a forcément des bugs, c’est juste que je ne les ai pas trouvés ou qu’ils ne sont pas corrigeables), j’ai en revanche peu d’inquiétude à avoir concernant la sincérité du programmeur : comme lui non plus ne maîtrise pas sa bestiole, pas de risque qu’il soit insincère3.

La définition du code source d’un réseau de neurones est ambiguë

Posons-nous un instant la question : qu’est-ce que le code source d’un réseau de neurones ? Est-ce la liste des neurones ? Comme on l’a vu, ils ne permettent ni de comprendre ce que fait le réseau, ni de le modifier. Ce sont donc de mauvais candidats. La GPL fournit une définition : le code source est la forme de l’œuvre privilégiée pour effectuer des modifications. Dans cette acception, le code source d’un réseau de neurones serait l’algorithme d’entraînement, le réseau de neurones de départ et le corpus sur lequel le réseau a été entraîné.

Cette ambiguïté fait courir un risque juridique sous certaines licences libres

Tu devines alors, cher lecteur, là où je veux en venir… Si le corpus comprend des œuvres non libres, tu n’as tout simplement pas le droit de le diffuser sous une licence libre ! Et si tu t’es limité à des œuvres libres pour entraîner ton modèle, tu risques fort d’avoir un ensemble d’apprentissage trop restreint, donc un réseau de neurones sans intérêt.

Alors il y a quatre moyens de tricher.
Le premier, c’est de t’asseoir sur la GPL et de considérer qu’en distribuant les neurones, tu as fait le taf. La ficelle est grossière. Je viens de passer une dépêche à te démontrer que c’est faux, tu pourrais au moins me montrer un peu plus de respect.

Le deuxième, c’est de distribuer sous une licence non copyleft, genre BSD ou WTFPL. Une licence qui ne nécessite pas de distribuer le code source. Certes, mais en fait tu ne fais pas du Libre.

Le troisième, c’est de considérer le réseau de neurones comme une donnée, pas un exécutable. Donc pas de code source. La partie sous GPL serait alors l’interface graphique, et le réseau, une donnée. C’est assez limite. Une donnée exécutable, ça s’approche dangereusement d’un blob binaire.

Le quatrième, c’est de repenser complètement le paradigme du logiciel libre et de considérer qu’il vise avant tout à rééquilibrer les rapports de pouvoir entre programmeur et utilisateur, et qu’en redistribuant les neurones, tu as fait le job. Sur les rapports de pouvoir, tu n’as pas tort ! Mais d’une part, ça ne tiendra pas la route devant un tribunal. D’autre part, il persiste une asymétrie de pouvoir : tu as accès au corpus, pas l’utilisateur.

Quand bien même on admettrait que le code source est l’ensemble corpus + algorithme d’optimisation + réseau de neurones de départ, l’optimisation d’un réseau de neurones consomme autrement plus de ressources que la compilation d’un programme plus classique, des ressources qui sont loin d’être à la portée du quidam classique. À quoi servirait un code source impossible à compiler ?

Enfin, même cette définition du code source pose problème : elle n’est en fait pas beaucoup plus lisible que le réseau lui-même. Ce n’est pas parce que j’ai accès aux centaines (de milliers) de textes sur lesquels un réseau a été entraîné que je peux prédire comment il va se comporter face à une nouvelle question.

Comment les boîtes qui font de l’IA non libre résolvent-elles ce dilemme ? Elles ne le résolvent pas

C’est presque enfoncer une porte ouverte que dire que l’IA pose de nombreuses questions de droit d’auteur, y compris dans le petit microcosme du non-libre. Cependant, les IA non-libres ont un avantage sur ce point : si le réseau de neurones ne permet pas de remonter au corpus initial (donc en l’absence de surapprentissage), alors elles peuvent tranquillement nier avoir plagié une œuvre donnée. Tu ne me verras pas défendre les pauvres auteurs spoliés, car j’ai toujours considéré que la nature même de l’information est de circuler sans barrières (Information wants to be free, tout ça) et que le droit d’auteur en est une, et particulièrement perverse.

La définition d’une IA open source ressemble furieusement à un constat d’échec

L’OSI a publié une définition d’IA open source. Cette définition mérite qu’on s’y attarde.

Premier point intéressant : après des années à tenter de se démarquer du Libre, notamment via la définition de l’Open Source qui tente de reformuler les 4 libertés sans recopier les 4 libertérs, l’OSI baisse les bras : est open source une IA qui respecte les 4 libertés.

Deuxième point intéressant : est open source une IA qui publie la liste des neurones, le corpus d’entraînement et la méthode d’entraînement. En fait, ça revient à ne pas choisir entre les neurones et leur méthode d’entraînement. Soit, mais ça ne résout pas le problème de l’effet boîte noire. Au mieux, ça revient à admettre qu’il est le même pour le programmeur et l’utilisateur.

Conclusion : qu’attendre d’une IA libre ?

Il ne fait aucun doute que développer des IA libres exigera de nouvelles licences. La GPL, on l’a vu, expose à un risque juridique du fait de l’ambiguïté de la définition du code source.

Il est à noter, d’ailleurs, qu’une IA repose rarement exclusivement sur son réseau de neurones : il y a systématiquement au moins un logiciel classique pour recueillir les inputs de l’utilisateur et les passer au réseau de neurones, et un second en sortie pour présenter les outputs. Ces briques logicielles, elles, peuvent tout à fait suivre le paradigme classique du logiciel libre.

En définitive, cher lecteur qui ne développes pas d’IA, je t’invite surtout à te demander : qu’attends-tu d’une IA ? Qu’entends-tu quand on te parle d’IA libre ? Plus fondamentalement, l’IA serait-elle un des rares domaines où il existe une distinction pratique entre libre et Open Source ?

Il n’y a pas de façon simple de faire une IA libre, il n’y a peut-être pas de façon du tout. Mais le principe du libre, c’est que c’est à l’utilisateur in fine de prendre ses décisions, et les responsabilités qui vont avec. Je n’espère pas t’avoir fait changer d’avis : j’espère modestement t’avoir fourni quelques clés pour enrichir ta réflexion sur le sens à donner au vocable IA open source qu’on voit fleurir ici et là.

1. Et je mettrai « artificiel » à la poubelle parce que Implicit is better than explicit, rien que pour embêter Guido). ↩

2. Bon, certaines infractions complexes à exécuter, comme le trafic de drogue ou le génocide, requièrent une certaine implication intellectuelle et sont donc peu compatibles avec l’altération du discernement, mais c’est lié au fait que l’infraction elle-même requiert un certain discernement. ↩

3. Du moins au niveau du réseau de neurones lui-même. Les entrées et les sorties peuvent tout à fait passer par une moulinette insincère et codée dans un langage tout à fait classique. ↩

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

Toutes les informations sont sur https://premier-samedi.org
Plan des salles : https://premier-samedi.org/IMG/png/plancarrnum.png

Venez aider ou vous faire aider à installer et paramétrer des logiciels libres et toute distribution GNU/Linux ou Android avec les associations d'utilisateurs de Fedora, Mageia, Ubuntu, Debian pour GNU/Linux ; et Replicant, LineageOS, f-droid pour Android, sur netbook, portable, tour, PC/Mac, ou smartphone, éventuellement à côté de votre système actuel. Idem si vous avez des difficultés avec GNU/Linux, un périphérique, un logiciel libre, ou avec des logiciels libres sous Android.

• Déjeuner à partir de 12h30-12h45 à la pizzeria Le Verona, 25 avenue Corentin Cariou
• Salle Classe Numérique 14h-18h : install party GNU/Linux toutes distributions + atelier auto-hébergement et Brique Internet avec Franciliens.net
• Salle Agora : si pas de conférence prévue, possibilité d'organiser à partir de 16h30 une présentation-discussion autour d'un thème particulier (pour se renseigner, choisir le thème ou s'inscrire, s'adresser à l'accueil de l'Install Partie à partir de 14h)
• Salle LivingLab : wikipermanence Wikimedia France
• Salle Atelier : atelier Blender 3D du BUG Blender User Group Paris
• Apéro/dîner dans un lieu à déterminer sur place

SQL Noir est un jeu libre (licence MIT) par Hristo « Cool as a cucumber » Bogoev, où vous incarnerez le rôle d’une personne enquêtant sur un crime, mais à grand renfort de requêtes SQL. Le SQL pour Structured Query Language ou « langage de requêtes structurées » est un langage informatique normalisé servant à exploiter des bases de données relationnelles (Wikipédia).

Bref vous avez une interface web qui vous permet de faire des requêtes dans les bases de données de témoins, suspects, enregistrements audio ou vidéo, etc., et vous devez trouver qui est la personne ayant commis le crime. Sur le principe vous allez identifier des éléments dans les données, traquer les infos correspondantes ou manquantes, faire le lien entre les éléments, repérer des liens entre personnes ou des transactions, et tout cela avec des requêtes SQL.

Il y a actuellement 4 enquêtes disponibles (et probablement plus à venir). C'est rapide, ludique, joli et ergonomique. L'outil aide en suggérant les mots clés SQL ou les noms de tables par exemple. L'outil dispose d'une zone pour prendre des notes, ce qui est à la fois pratique pour garder trace des requêtes SQL, mais surtout des résultats, et vous en aurez besoin pour les cas compliqués.

Le premier commit du projet date du début du mois, et le projet est donc assez jeune, tout en étant à la fois prometteur, et déjà très sympa.

Note: full disclosure, LinuxFr.org utilise du SQL. Cette information est-elle pertinente ici ? Absolument pas, mais des fois il y a des infos inutiles dans les enquêtes. Et merci à @siltaer d'avoir partagé ce message qui m'a fait découvrir ce jeu.

• lien nᵒ 1 : SQLNoir Solve mysteries through SQL
• lien nᵒ 2 : GitHub SQLNoir
• lien nᵒ 3 : MiXiT 2022 Lætitia Avrot "Meet NULL the UNKNOWN"
• lien nᵒ 4 : DELETEs are difficult

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

Jean-Pierre Archambault est décédé le 23 février 2025. Ancien enseignant et professeur agrégé de mathématiques, il présidait notamment l'association Enseignement Public et Informatique (EPI). Il a été un acteur essentiel des ressources libres et des logiciels pour l'Éducation nationale en France et dans la francophonie.

L'étiquette jean-pierre_archambault vient nous remémorer combien il était actif autour du logiciel libre et de l'éducation depuis longtemps, que nous le croisions régulièrement lors de conférences et d'événements, et combien il était une personne appréciée, active, humaine et de convictions.

LinuxFr.org présente ses plus sincères condoléances à sa famille et à ses proches.

(photo tirée d'une citation pour l'April)

• lien nᵒ 1 : Annonce du décès
• lien nᵒ 2 : Une biographie par l'EPI
• lien nᵒ 3 : Réaction de l'April
• lien nᵒ 4 : Interview pour L'étudiant en 2012
• lien nᵒ 5 : Article Les clés de demain/Le Monde « Il est indispensable que chacun ait une culture informatique »

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

Cette revue de presse sur Internet fait partie du travail de veille mené par l’April dans le cadre de son action de défense et de promotion du logiciel libre. Les positions exposées dans les articles sont celles de leurs auteurs et ne rejoignent pas forcément celles de l’April.

• [clubic.com] DeepSeek continue de bousculer l'IA en partageant plus largement ses modèles
• [leParisien.fr] Polémique Wikipédia: cinq minutes pour comprendre les critiques qui visent l'encyclopédie en France - Le Parisien
• [Next] Donald Trump supprime l'indépendance des agences de régulation FTC, FCC et SEC
• [Next] GNOME 47.4 et 48 Beta disponibles: quelles nouveautés?

• lien nᵒ 1 : April
• lien nᵒ 2 : Revue de presse de l'April
• lien nᵒ 3 : Revue de presse de la semaine précédente
• lien nᵒ 4 :

Illico Editor est un (petit) couteau suisse de la qualification de données développé à l’origine pour permettre aux experts métiers de transformer les données sans recourir à la programmation… le tout dans une simple page HTML (pas de serveur Web) donc une utilisation à travers le navigateur.

Aujourd’hui, plus de 150 transformations de données sont disponibles prêtes à l'emploi.

Particularité : chaque transformation exécutée ainsi que son résultat sont inscrits dans un journal de bord créant ainsi une sorte de procédure-type sans effort.

Publié sous licence GPL, le code d’Illico est globalement très basique : standards HTML5/CSS3/JS, et zéro dépendance, bibliothèque ou appel à un code tiers. Les données restent dans le (cache du) navigateur.
Les algorithmes sont très simples. La complexité est plutôt liée à la manière d’imaginer de nouvelles transformations de données, à la fois génériques (paramétrables) tout en restant simples pour l’utilisateur (nombre réduit de paramètres).

• lien nᵒ 1 : Site principal (changement de domaine)
• lien nᵒ 2 : Précédente dépêche (2021)

Sommaire

• Quelques limites à connaître
•  Objet de la dépêche
  • Avant de commencer
• Nouveaux tutoriels
  • Transposer une matrice
  • Comparer (rapidement) des groupes de colonnes
  • Comparer des lignes dans un fichier cumul
  • Créer un fichier cumul à partir de deux sources aux formats proches
  • Reconstituer des calendriers
  • Fidélisation (suivre une cohorte)
• Nouvelles fonctionnalités
  • Valeurs en liste : compacter, inverser l’ordre, filtrer
  • Valeurs en liste : lister les permutations, mélanger la liste
  • enlever les accents et les cédilles de l’en-tête
  • Permuter les colonnes
  • Numéroter chaque série
  • Obtenir les méta-données des colonnes sélectionnées
  • Décaler les dates
  • Jours de la semaine
  • Transformation des périodes « temps : intervalles »
  • Calculs
  • Convertir d’un système de numération à un autre
  • Matrice : transposée, inverser, trier

Quelques limites à connaître

Dans mon usage, des crashs du navigateur ont été constatés sur des grands jeux de données avec les fonctionnalités qui sollicitent le plus grand nombre de comparaisons (précisément le calcul de la distance d’édition / lignes).

Pour un grand volume de données, mon conseil serait d’opter pour Opera/Vivaldi qui proposent à l’utilisateur d’augmenter la mémoire allouée à la page (plutôt que de faire crasher l’onglet/navigateur) ; de réduire le jeu de données aux colonnes/lignes à traiter (ce qui réduirait la taille), avant de se lancer dans les transformations ; ou d’opter pour des outils plus adaptés à cette volumétrie.

Un test sur des données factices m’avait permis d’identifier des tailles limites de jeu de données : https://illico.ti-nuage.fr/doc/build/html/fct/principes.html#jeu-de-donnees-volumineux

 Objet de la dépêche

Cette dépêche fait écho à la précédente de janvier 2021.

Au-delà des corrections de bug et des améliorations (gestion des nombres décimaux et négatifs pour les intervalles, options supplémentaires pour décider l’interprétation de “valeurs” vides), je voulais présenter ici la trentaine de nouvelles fonctionnalités/traitements et les nouveaux tutoriels.

Avant de commencer

Dans Illico, l’expression valeurs en liste désigne

• des données présentées sous la forme a, b, c (le séparateur peut être un caractère ou une chaîne)
• des listes de couples de valeurs xxx:1 / yyy:2 / zzz:3 (un séparateur de liste / + un délimiteur {clé => valeur} ici :

Nouveaux tutoriels

La section tutoriels décrit des cas concrets pour lesquels il n’existe pas de résolution « en 1 étape ».
Dans certains cas, une fonctionnalité a été développée pour couvrir tout ou partie de la résolution.

Ces tutoriels sont détaillés pas à pas dans la section “tutoriels” afin d’être utilisés comme support de formation.

Je résume ici leur logique.

Transposer une matrice

Au sens “mathématique” du terme, bascule les lignes en colonnes et vice-versa :

nombre d’étapes/actions du tutoriel : 6

une nouvelle fonctionnalité a été développée par la suite pour transposer les données en 1 clic/étape/action

Comparer (rapidement) des groupes de colonnes

Comparer des groupes de colonnes prises deux à deux était déjà possible. Cependant, avec un grand nombre de colonne, l’opération pouvait s’avérer fastidieuse et source d’erreurs.
Le tutoriel présente une manière plus générique de comparer un grand nombre de colonne de deux fichiers sources avec le même en-tête, par exemple la description d’une même population sur deux années différentes.

nombre d’étapes/actions du tutoriel : (2 par fichier source) + 4

l’intérêt de ce tutoriel réside surtout dans le fait de rendre la complexité du traitement indépendante du nombre (de paires) de colonnes à comparer

Comparer des lignes dans un fichier cumul

On souhaite identifier des différences mais cette fois au sein d’un même fichier de données décrivant un cumul.
Il peut s’agir par exemple de deux jeux de données mis bout-à-bout décrivant une même population sur deux années différentes.

nombre d’étapes/actions du tutoriel : 3

Créer un fichier cumul à partir de deux sources aux formats proches

Le cas a été rencontré lors d’une analyse de journaux comptables où les jeux de données présentaient des rubriques/codes comptables en colonne.
D’un mois sur l’autre, le nombre et l’ordre de ces colonnes/rubriques différaient. Le tutoriel permet de s’affranchir de ces variations de la structure des données.

nombre d’étapes/actions du tutoriel : (4 par fichier source) + 3

Reconstituer des calendriers

Autre cas de figure rencontré, les données décrivent des personnes présentes sur des périodes avec en colonne la date de début, la date de fin, puis les autres données.
À partir de ces données, on recherche les dates/jours exactes qui ont rassemblé le plus de personne.

La résolution consiste à générer l’ensemble des jours (entre la date de début et la date de fin), c’est-à-dire une description des faits à une échelle unitaire/atomique (chaque ligne décrivant alors une date et non une période).

Trois approches sont proposées dans le tutoriel : entre 3 et 6 étapes/actions

Fidélisation (suivre une cohorte)

La problématique soulevée était de comprendre les parcours, trajectoires pour une population donnée.

Exemple simplifié : 4 lignes de données décrivent (dans l’ordre chronologique) les états/statuts successifs d’un individu, à raison d’un par ligne : a -> b -> c -> d.

dans la pratique, le jeu de données décrivait une population d’individu avec des trajectoire de 4 à 50 états, parfois circulaires a -> b -> a -> d -> c

On souhaite identifier :

1. le parcours par rapport à l’état initial pour l’individu pris en exemple, le résultat sera la relation suivante : a => {b -> c -> d}
2. les changements d’état (de proche en proche) pour le même exemple, le résultat sera une liste de couple de valeurs : (a => b), (b => c), (c => d)
3. les relations entre l’état initial et n’importe quel autre état du parcours même exemple, le résultat sera trois couples de valeurs : (a => b), (a => c), (a => d)
4. les relations entre n’importe quel état du parcours et n’importe quel autre état rencontré par la suite même exemple, le résultat sera six couples :
   • (a => b), (a => c), (a => d)
   • (b => c), (b => d)
   • (c => d)

La fonctionnalité utilisée possède une option “scénario” avec les 4 choix.
Ainsi, on définit « ce que représente les données » en précisant le ou les séparateurs, et la transformation est appliquée selon la demande.

Les 4 scénarios sont proposés dans le tutoriel : 3 étapes/actions (une 4ème étape est nécessaire si on souhaite étudier à part le 1er état et l’état terminal de la trajectoire)

Nouvelles fonctionnalités

La majorité des nouvelles fonctionnalités concerne

• des traitements de dates (décalage, conversion)
• des traitements d’intervalles numériques
• des traitements de périodes (intervalles de dates)

Elles sont présentées ci-dessous dans leur rubrique respective (dans l’ordre d’apparition des rubriques dans Illico et dans la documentation).

(dans l’application, chaque écran permettant d’exécuter une transformation possède un lien vers la section/page concernée dans la documentation)

Valeurs en liste : compacter, inverser l’ordre, filtrer

compacter les listes

rubrique « valeurs en liste : agrégats"

Pour une liste qui présente des répétitions—a,a,b,c,a,d,b—les deux options de cette transformation permettent d’obtenir :

• a,b,c,a,d,b : réduire à une occurrence, pour chaque série
• a,b,c,d : conserver globalement les premières occurrences
• c,a,d,b : conserver globalement les dernières occurrences

inverser l’ordre des éléments des listes

rubrique « valeurs en liste : structure"

Pour une colonne décrivant des listes d’éléments—a:1, b:2—,

• inverse l’ordre des valeurs des listes (b:2, a:1)
• inverse l’ordre des valeurs des listes imbriquées seulement (1:a, 2:b)
• inverse l’ordre des listes imbriquées et des valeurs dans ces listes (2:b, 1:a)

filtrer ou exclure les valeurs d’une liste

rubrique « valeurs en liste : filtres"

compare les listes de valeurs d’une colonne par rapport à une autre colonne de référence

• égal
• différent de
• supérieur/inférieur ou égal à
• strictement supérieur/inférieur à

réduire la liste à certaines clés

conserver/exclure certains couples {clé:valeur} lorsque la clé existe dans une autre colonne (qui contient pour chaque ligne la liste de clés à conserver ou à exclure)

Par exemple—et sans devoir utiliser des regex/expressions rationnelles—la liste 2021=3,2022=1,2024=4 pourra être réduite à 2022=1,2024=4 si la clé 2021 existe dans la colonne de contrôle.

Valeurs en liste : lister les permutations, mélanger la liste

rubrique valeurs en liste : enrichissement

lister les permutations des valeurs d’une liste

produit la liste de toutes les permutations des valeurs des listes de la colonne sélectionnée.

mélanger les valeurs de la liste

applique le mélange de Fisher-Yates sur les valeurs de la liste

enlever les accents et les cédilles de l’en-tête

rubrique « en-tête"

surtout utile lorsque l’on part d’un tableur et que l’on cherche à injecter les données dans une base de données ne tolérant pas ces caractères dans les en-têtes

Permuter les colonnes

rubrique « colonnes : ordre"

Dans le cas d’un export de données depuis un logiciel métier, ou suite à certaines transformations, certaines colonnes peuvent être générées dans un ordre qui ne s’avère pas très intuitif.

Cette nouvelle fonctionnalité inverse en 1 clic l’ordre des colonnes sélectionnées en permutant (au choix)

• 1ʳᵉ et 2ᵉ, 3ᵉ et 4ᵉ, etc.
• 1ʳᵉ et dernière, 2ᵉ et avant-dernière, etc.

Numéroter chaque série

rubrique “lignes”

Dans Illico, le terme série désigne une suite de lignes contiguës qui possèdent la même valeur dans la colonne sélectionnée (un identifiant par exemple).
Si l’identifiant réapparaît plus loin dans les données, il s’agira d’une nouvelle série.

(une autre transformation permet déjà de numéroter chaque ligne de la série)

Obtenir les méta-données des colonnes sélectionnées

rubrique “agrégats”

Pour les colonnes sélectionnées, indique

• si la colonne ne contient que des valeurs uniques (les valeurs vides sont comptées à part)
• le nombre de lignes sans valeur (valeur vide)
• le nombre de valeurs renseignées (valeur non-vide)
• la cardinalité : nombre de valeurs différentes rencontrées dans la colonne

Décaler les dates

rubrique “temps”

décaler les dates avec 1 constante (saisie par l’utilisateur)

permet de décaler les dates d’une colonne à partir d’une constante (on précise l’unité : nombre de jours, de semaines, de mois ou d’années)

décaler des dates selon 1 autre colonne

idem précédemment mais en se basant sur les valeurs d’une autre colonne plutôt qu’une constante

Jours de la semaine

rubrique “temps”

donner le nom des jours de la semaine

la date est alors recodée : lundi, mardi…

compter chacun des jours de la semaine

nombre de lundis, de mardis, etc. dans l’intervalle décrit par des colonnes début et fin de la période

obtenir le numéro du jour dans l’année

1 pour le 1ᵉʳ janvier, 32 pour le 1ᵉʳ février…

Transformation des périodes « temps : intervalles »

compléter un intervalle de date (2 colonnes : début et fin de la période)

crée une liste de jour/date dans l’intervalle décrit

rechercher une date dans un intervalle de date

compare 1 colonne (date recherchée) par rapport à 2 autres colonnes décrivant une période (début et fin de la période)

combiner deux périodes (4 colonnes)

option (au choix) : obtenir

• une fusion : période englobant les deux [min, max]
• une union : période englobant les deux seulement si intersection
• une intersection : plus petite période commune

comparer les dates et une liste de seuils (saisie par l’utilisateur)

détecter des collisions de périodes

portée de la détection

• rechercher pour l’ensemble des données
• rechercher dans les lignes qui partagent un même identifiant (les lignes comparées ne sont pas forcément contiguës)
• rechercher dans les lignes qui décrivent une série (lignes contiguës avec un même identifiant)

Calculs

rubrique “calculs”

calculer une opération sur 1 colonne : options

options :

• opérations : minimum, maximum, moyenne, somme
• valeurs vides : ignorées ou traduites par zéro
• calcul : total ou cumulé
  • option si cumulé : en partant de la première ou dernière ligne
• résultat : global ou local
  • option si local : pour chaque série ou pour chaque identifiant

calculer une opération avec 1 constante (saisie par l’utilisateur)

calculer une somme ou une moyenne sur x colonnes

Convertir d’un système de numération à un autre

rubrique “enrichissement”

conversion depuis et vers une base binaire, octale, décimale, hexadécimale

Matrice : transposée, inverser, trier

rubrique “matrice”

calculer la transposée

Transpose le jeu de données : les lignes deviennent les colonnes et inversement ; la ligne d’en-tête devient la première colonne ; la première colonne devient la ligne d’en-tête.

inverser l’ordre des lignes

Inverse l’ordre des lignes du jeu de données : la première ligne devient la dernière, la dernière devient la première, etc.

trier par ordre alphabétique

options

• ordre des lettres : A…Z…a…z…É…é ou A…É…Z…a…é…z
• placer les valeurs vides : au début ou à la fin

trier par ordre numérique

option : les valeurs vides sont

• les plus petites (seront placées au début du tableau)
• les plus grandes (seront placées à la fin du tableau)
• égales à zéro

trier par ordre chronologique

option : les valeurs vides sont

• dans le passé lointain
• dans un futur lointain
• égales à la date du jour
• égales à une date précise (à saisir)

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.

• lien nᵒ 1 : Why formalize mathematics? par Patrick Massot

Sommaire

• Vérifier des programmes
• Vérifier des démonstrations mathématiques
• Brouwer-Heyting-Kolmogorov
• Curry-Howard
• Quantificateurs et types dépendants
• Logique intuitionniste
• Quelques exemples
• Quelques succès de la formalisation
• La recherche en théorie des types
• Conclusion

Vérifier des programmes

Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : nous passons énormément de temps à découvrir des bugs, et pour les personnes du développement logiciel, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.

Dans une formation universitaire de base en informatique, on rencontre des algorithmes, mais aussi des méthodes pour prouver que ces algorithmes terminent et répondent bien au problème posé. Les premières introduites sont typiquement les variants de boucle (montrer qu’une certaine valeur décroît à chaque itération, ce qui assure que le programme termine si elle ne peut pas décroître à l’infini), et les invariants de boucle (montrer qu’une certaine propriété vraie au début d’une boucle est préservée entre deux itérations, ce qui assure qu’elle reste encore vraie à la fin de la boucle).

On a donc, d’une part, un algorithme, implémentable sur machine, d’autre part une preuve, sur papier, que l’algorithme est correct. Mais si l’implémentation a une erreur par rapport à l’algorithme sur papier ? Et puisque nous n’arrêtons pas de nous tromper dans nos programmes, il est fort possible que nous nous trompions dans notre preuve (qui n’a jamais oublié qu’il fallait faire quelque chose de spécial dans le cas  ?).

En tant que programmeurs, on peut imaginer une approche où non seulement l’algorithme est implémenté, mais sa preuve de terminaison et de correction est aussi « implémentée », c’est-à-dire encodée dans un langage qui ressemble à un langage de programmation, pour être ensuite non pas interprétée ou compilée mais vérifiée.

La vérification est un très vaste domaine de l’informatique, dont je ne suis pas spécialiste du tout, et dans lequel il existe énormément d’approches : la logique de Hoare (voir par exemple l’outil why3), qui est essentiellement un raffinement des variants et invariants de boucle, la logique de séparation spécialement conçue pour raisonner sur la mémoire mutable (voir Iris), le model checking qui se concentre sur des programmes d’une forme particulièrement simple (typiquement des systèmes de transition finis) pour en vérifier des propriétés de façon complètement automatisée, etc.

Dans cette dépêche, je vais parler d’une approche avec quelques caractéristiques particulières :

• On vérifie des programmes purement fonctionnels (pas d’effets de bord, même si on peut les simuler).

• Le même langage mélange à la fois les programmes et leurs preuves.

• Plus précisément, le langage ne fait pas (ou peu) de distinction entre les programmes et les preuves.

Vérifier des démonstrations mathématiques

Pour se convaincre de l’ampleur que les démonstrations ont prise dans les mathématiques contemporaines, il suffit d’aller jeter un œil, par exemple, au projet Stacks : un livre de référence sur la géométrie algébrique, écrit collaborativement sur les 20 dernières années, dont l’intégrale totalise plus de 7500 pages très techniques. Ou bien la démonstration du théorème de classification des groupes finis simples : la combinaison de résultats répartis dans les dizaines de milliers de pages de centaines d’articles, et une preuve « simplifiée » toujours en train d’être écrite et qui devrait faire plus de 5000 pages. Ou bien le théorème de Robertson-Seymour, monument de la théorie des graphes aux nombreuses applications algorithmiques : 20 articles publiés sur 20 ans, 400 pages en tout. Ou bien, tout simplement, le nombre de références dans la bibliographie de la moindre thèse ou d’articles publiés récemment sur arXiv.

Inévitablement, beaucoup de ces démonstrations contiennent des erreurs. Parfois découvertes, parfois beaucoup plus tard. Un exemple assez célèbre est celui d’un théorème, qui aurait été très important s’il avait été vrai, publié en 1989 par Vladimir Voedvodsky, un célèbre mathématicien dont je vais être amené à reparler plus bas, avec Mikhail Kapranov. Comme raconté par Voedvodsky lui-même, un contre-exemple a été proposé par Carlos Simpson en 1998, mais jusqu’en 2013, Voedvodsky lui-même n’était pas sûr duquel était faux entre sa preuve et le contre-exemple !

Il y a aussi, souvent, des « trous », qui ne mettent pas tant en danger la démonstration mais restent gênants : par exemple, « il est clair que la méthode classique de compactification des espaces Lindelöf s’applique aussi aux espaces quasi-Lindelöf », quand l’auteur pense évident qu’un argument existant s’adapte au cas dont il a besoin mais que ce serait trop de travail de le rédiger entièrement. Donc, assez naturellement, un but possible de la formalisation des maths est de produire des démonstrations qui soient certifiées sans erreur (et sans trou).

Mais c’est loin d’être le seul argument. On peut espérer d’autres avantages, qui pour l’instant restent de la science-fiction, mais après tout ce n’est que le début : par exemple, on peut imaginer que des collaborations à grande échelle entre beaucoup de mathématiciens deviennent possibles, grâce au fait qu’il est beaucoup plus facile de réutiliser le travail partiel de quelqu’un d’autre s’il est formalisé que s’il est donné sous formes d’ébauches informelles pas complètement rédigées.

Brouwer-Heyting-Kolmogorov

Parmi les assistants de preuve existants, la plupart (mais pas tous) se fondent sur une famille de systèmes logiques rangés dans la famille des « théories des types ». L’une des raisons pour lesquelles ces systèmes sont assez naturels pour être utilisés en pratique est qu’en théorie des types, les preuves et les programmes deviennent entièrement confondus ou presque, ce qui rend facile le mélange entre les deux.

Mais comment est-ce qu’un programme devient une preuve, au juste ? L’idée de base est appelée interprétation de Brouwer-Heyting-Kolomogorov et veut que les preuves mathématiques se comprennent de la façon suivante :

• Le moyen de base pour prouver une proposition de la forme «  et  » est de fournir d’une part une preuve de et une preuve de . En d’autres mots, une preuve de «  et  » rassemble en un même objet une preuve de et une preuve de . Mais en termes informatiques, ceci signifie qu’une preuve de «  et  » est une paire d’une preuve de et d’une preuve de .

• De même, pour prouver «  ou  », on peut prouver , ou on peut prouver . Informatiquement, une preuve de «  ou  » va être une union disjointe : une preuve de ou une preuve de , avec un bit pour savoir dans quel cas on est.

• Pour prouver « Vrai », il suffit de dire « c’est vrai » : on a une unique preuve de « Vrai ».

• On ne doit pas pouvoir prouver « Faux », donc une preuve de « Faux » n’existe pas.

• Et le plus intéressant : pour prouver « si alors  », on suppose temporairement et on en déduit . Informatiquement, ceci doit devenir une fonction qui prend une preuve de et renvoie une preuve de .

Curry-Howard

L’interprétation de Brouwer-Heyting-Kolmogorov est informelle, et il existe plusieurs manières de la rendre formelle. Par exemple, on peut interpréter tout ceci par des programmes dans un langage complètement non-typé, ce qui s’appelle la réalisabilité.

Mais en théorie des types, on prend plutôt un langage statiquement typé pour suivre l’idée suivante : si une preuve de et est une paire d’une preuve de et d’une preuve de , alors le type des paires de et peut se comprendre comme le type des preuves de «  et  ». On peut faire de même avec les autres types de preuves, et ceci s’appelle la correspondance de Curry-Howard. Autrement dit, là où Brouwer-Heyting-Kolmogorov est une correspondance entre les preuves et les programmes, Curry-Howard est un raffinement qui met aussi en correspondance les propositions logiques avec les types du langage, et la vérification des preuves se confond entièrement avec le type checking.

Sur les cas que j’ai donnés, la correspondance de Curry-Howard donne :

• La proposition «  et  » est le type des paires d’un élément de et d’un élément de ,

• La proposition «  ou  » est le type somme de et (comme Either en Haskell et OCaml, les tagged unions en C, et std::variant en C++ : l’un ou l’autre, avec un booléen pour savoir lequel),

• La proposition « Vrai » est le type trivial à une seule valeur (comme () en Haskell et Rust, unit en OCaml),

• La proposition « Faux » est le type vide qui n’a aucune valeur (comme ! en Rust),

• La proposition « si alors  » est le type des fonctions qui prennent un argument de type et renvoient une valeur de type .

Quantificateurs et types dépendants

La version de Curry-Howard que j’ai esquissée donne une logique dite « propositionnelle » : il n’y a que des propositions, avec des connecteurs entre elles. Mais en maths, on ne parle évidemment pas que des propositions. On parle de nombres, de structures algébriques, d’espaces topologiques, …, bref, d’objets mathématiques, et des propriétés de ces objets. Les deux types principaux de propositions qui manquent sont ce qu’on appelle les quantificateurs : « Pour tout , … » et « Il existe tel que… ». Ici, ce qui est une évidence en logique devient moins évident, mais très intéressant, du côté des programmes.

Prenons pour l’exemple le théorème des deux carrés de Fermat, qui énonce (dans l’une de ses variantes) qu’un nombre premier impair est de la forme si et seulement s’il peut s’écrire comme somme de deux carrés parfaits. À quoi doit ressembler le type associé à cette proposition ? Par analogie avec les implications, on a envie de dire que cela devrait être une fonction, qui prend un nombre premier impair , et renvoie une preuve de l’équivalence. Problème : ce qui est à droite de l’équivalence est une proposition paramétrée par . Autrement dit, en notant le type des nombres premiers impairs, on ne veut plus un simple type fonction , mais un type fonction où le type de retour peut dépendre de la valeur passée à la fonction, noté par exemple . Ces types qui dépendent de valeurs sont appelés types dépendants.

Dans les langages de programmation populaires, il est rare de trouver des types dépendants. Mais on en retrouve une forme faible en C avec les tableaux de longueur variable (VLA pour « variable-length arrays ») : on peut écrire

… f(int n) { int array[n]; … }

qui déclare un tableau dont la taille n est une expression. Néanmoins, en C, même si on dispose de ce type tableau qui est en quelque sorte dépendant, on ne peut pas écrire une fonction « int[n] f(int n) » qui renvoie un tableau dont la longueur est passée en paramètre. Plus récemment, en Rust, il existe les const generics, où des valeurs se retrouvent dans les types et où on peut écrire fn f<const n: usize>() -> [u8; n], ce qui est un vrai type dépendant, mais cette fois avec la restriction assez sévère que toutes ces valeurs peuvent être calculées entièrement à la compilation, ce qui à cause de la façon dont fonctionne ce type de calcul en Rust empêche par exemple les allocations mémoire. (Donc l’implémentation est assez différente, elle efface ces valeurs en « monomorphisant » tous les endroits où elles apparaissent.)

En théorie des types, le langage est (normalement) purement fonctionnel, donc les problèmes d’effets de bord dans les valeurs à l’intérieur des types dépendants ne se pose pas. Le type checking peut déclencher des calculs arbitrairement complexes pour calculer les valeurs qui se trouvent dans les types.

Et le « il existe », au fait, à quoi correspond-il ? Cette fois, ce n’est plus une fonction dépendante mais une paire dépendante : une preuve de « Il existe tel que  » est une paire d’une valeur et d’une preuve de . La différence avec une paire normale est que le type du deuxième élément peut dépendre de la valeur du premier élément.

Comme on peut commencer à s’en douter, le fait d’avoir des types dépendants est utile pour prouver des affirmations mathématiques, mais aussi, bien qu’il puisse sembler inhabituel, pour prouver des programmes, et plus précisément pour encoder des propriétés des valeurs dans les types. Là où on aurait dans un langage moins expressif une fonction qui renvoie deux listes, avec une remarque dans la documentation qu’elles sont toujours de même taille, dans un langage avec des types dépendants, on peut renvoyer un triplet d’un entier , d’une liste dont le type indique qu’elle est de taille , et une deuxième liste elle aussi de taille . Et là où on aurait un deuxieme_liste[indice_venant_de_la_premiere] avec un commentaire que cela ne peut pas produire d’erreur, car les deux listes sont de même taille, on a un programme qui utilise la garantie que les deux listes sont de même taille, et le typage garantit statiquement que cette opération t[i] ne produira pas d’erreur.

Logique intuitionniste

Reprenons l’exemple du théorème des deux carrés de Fermat. Nous pouvons maintenant traduire cette proposition en un type : celui des fonctions qui prennent un nombre premier impair et renvoient une paire de :

• Une fonction qui prend tel que et renvoie deux entiers accompagnés d’une preuve que ,

• Réciproquement, une fonction qui prend et une preuve de , et renvoie tel que .

Prouver le théorème des deux carrés de Fermat en théorie des types, c’est donner un élément (on dit plutôt « habitant ») de ce type, soit un programme dont le langage peut vérifier qu’il a ce type. Mais que fait au juste ce programme quand on l’exécute ? On voit qu’il permet notamment de calculer une décomposition d’un nombre premier impair congru à 1 modulo 4 comme somme de deux carrés.

Là, c’est le côté « programmes » qui apporte un élément moins habituel du côté « preuves » : l’exécution d’un programme va correspondre à un processus de simplification des preuves. Notamment, si on a une preuve de « si alors  » et une preuve de , on peut prendre la preuve de et remplacer chaque utilisation de l’hypothèse dans la preuve de « si alors  », pour obtenir une preuve de qui peut contenir de multiples copies d’une même preuve de . Cette opération de simplification du côté logique correspond naturellement au fait que la manière en théorie des types de prouver à partir d’une preuve de et d’une preuve de est tout simplement d’écrire , et que calculer , informatiquement, se fait bien en remplaçant le paramètre de à tous les endroits où il apparaît par la valeur et à simplifier le résultat. On dit que la logique de Curry-Howard est constructive, parce qu’elle se prête à une interprétation algorithmique.

Mais ceci peut sembler gênant. Par exemple, il est trivial en maths « normales » de prouver que tout programme termine ou ne termine pas. Mais par Curry-Howard, une preuve que tout programme termine ou ne termine pas doit être une fonction qui prend un programme, et qui renvoie soit une preuve qu’il termine, soit une preuve qu’il ne termine pas. Autrement dit, si cette proposition censément triviale était prouvable dans Curry-Howard, on aurait un algorithme pour résoudre le problème de l’arrêt, ce qui est bien connu pour être impossible.

L’explication à cette différence tient au fait que la preuve « triviale » de cette proposition utilise une règle de déduction qui a un statut un peu à part en logique, dite règle du tiers exclu : pour n’importe quelle proposition , sans aucune hypothèse, on peut déduire «  ou (non ) » (autrement dit, que est vraie ou fausse). Or cette règle n’admet pas d’interprétation évidente par Curry-Howard : le tiers exclu devrait prendre une proposition et renvoyer soit une preuve de , soit une preuve que est fausse (ce qui s’encode par « si alors Faux »), autrement dit, le tiers exclu devrait être un oracle omniscient capable de vous dire si une proposition arbitraire est vraie ou fausse, et ceci est bien évidemment impossible.

(Cela dit, si vous voulez vous faire mal à la tête, apprenez que c’est l’opérateur call/cc et pourquoi l’ajouter permet de prouver le tiers exclu. Exercice : call/cc existe dans de vrais langages, comme Scheme, pourtant on vient de voir que le tiers exclu semble nécessiter un oracle omniscient, comment expliquer cela ?)

Pour être précis, la logique sans le tiers exclu est dite intuitionniste (le terme constructive étant un peu flou, alors que celui-ci est précis). On peut faire des maths en restant entièrement en logique intuitionniste, et même si ce n’est pas le cas de l’écrasante majorité des maths, il existe tout de même un certain nombre de chercheurs qui le font, et ceci peut avoir divers intérêts. Il y a notamment l’interprétation algorithmique des théorèmes, mais aussi, de manière beaucoup plus avancée, le fait que certaines structures mathématiques (topos, ∞-topos et consorts) peuvent s’interpréter comme des sortes d’univers mathématiques alternatifs régis par les règles de la logique intuitionniste (techniquement, des « modèles » de cette logique), et que parfois il est plus simple de prouver un théorème en le traduisant à l’intérieur de l’univers et en prouvant cette version traduite de manière intuitionniste.

Pour pouvoir malgré tout raisonner en théorie des types de manière classique (par opposition à intuitionniste), il suffit de postuler le tiers exclu comme axiome. Du point de vue des programmes, cela revient à rajouter une constante qui est supposée avoir un certain type mais qui n’a pas de définition (cela peut donc rendre les programmes impossibles à exécuter, ce qui est normal pour le tiers exclu).

Quelques exemples

Si vous aviez décroché, c’est le moment de reprendre. Parlons un peu des assistants de preuve qui existent. Les plus connus sont :

• Rocq, anciennement nommé Coq, développé à l’Inria depuis 1989, écrit en OCaml, sous licence LGPL 2.1. Il est assez lié à l’histoire de la théorie des types, car il a été créé par Thierry Coquand comme première implémentation du calcul des constructions, une théorie des types inventée par Coquand et devenue l’une des principales existantes. (Oui, Coq a été renommé en Rocq à cause de l’homophonie en anglais entre « Coq » et « cock ». J’apprécierais que les commentaires ne se transforment pas en flame war sur ce sujet très peu intéressant, merci.)

• Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.

• Agda, créé par Ulf Norrell en 1999, écrit en Haskell et sous licence BSD 1-clause.

• D’autres que je connais moins, notamment Isabelle et F* (liste sur Wikipédia).

Pour illustrer comment peuvent fonctionner les choses en pratique, voici un exemple très simple de code en Agda :

open import Agda.Primitive using (Level) open import Data.Product using (_×_; _,_) swap : {ℓ₁ ℓ₂ : Level} → {P : Set ℓ₁} {Q : Set ℓ₂} → P × Q → Q × P swap (p , q) = (q , p)

Vue comme un programme, cette fonction swap inverse simplement les deux éléments d’une paire. Vue comme une preuve, elle montre que pour toutes propositions et , si et , alors et . Comme le veut Curry-Howard, les deux ne sont pas distingués. Les types et sont eux-mêmes dans des types avec un « niveau » , ceci parce que, pour des raisons logiques, il serait incohérent que le type des types soit de son propre type, donc on a un premier type de types , qui est lui-même de type , et ainsi de suite avec une hiérarchie infinie de niveaux appelés univers. À un niveau plus superficiel, on remarquera qu’Agda a une syntaxe qui ressemble fort à Haskell (et utilise intensivement Unicode).

Voilà la même chose en Rocq :

Definition swap {P Q : Prop} : P /\ Q -> Q /\ P := fun H => match H with conj p q => conj q p end.

La syntaxe est assez différente et ressemble plutôt à OCaml (normal, vu que Rocq est écrit en OCaml et Agda en Haskell). Mais à un niveau plus profond, on voit apparaître un type Prop dont le nom évoque furieusement les propositions. Or j’avais promis que les propositions seraient confondues avec les types, donc pourquoi a-t-on un type spécial pour les propositions ?

En réalité, pour diverses raisons, il peut être intéressant de briser l’analogie d’origine de Curry-Howard et de séparer les propositions et les autres types en deux mondes qui se comportent de façon extrêmement similaire mais restent néanmoins distincts. Notamment, un principe qu’on applique sans réfléchir en maths est que si deux propositions sont équivalentes, alors elles sont égales (extensionnalité propositionnelle), mais on ne veut clairement pas ceci pour tous les types (on peut donner des fonctions bool -> int et int -> bool, pourtant on ne veut certainement pas bool = int), donc séparer les propositions des autres permet d’ajouter l’extensionnalité propositionnelle comme axiome. (Mais il y a aussi des différences comme l'imprédicativité dans lesquelles je ne vais pas rentrer.)

Et voici encore le même code, cette fois en Lean :

def swap {P Q : Prop} : P ∧ Q → Q ∧ P := fun ⟨p, q⟩ => ⟨q, p⟩

À part les différences de syntaxe, c’est très similaire à Rocq, parce que Lean a aussi une séparation entre les propositions et les autres types.

Cependant, en Rocq et Lean, on peut aussi prouver la même proposition de façon différente :

Lemma swap {P Q : Prop} : P /\ Q -> Q /\ P. Proof. intros H. destruct H as [p q]. split. - apply q. - apply p. Qed.

et

def swap {P Q : Prop} : P ∧ Q → Q ∧ P := by intro h have p := h.left have q := h.right exact ⟨q, p⟩

Avec Proof. ou by, on entre dans un mode où les preuves ne sont plus écrites à la main comme programmes, mais avec des tactiques, qui génèrent des programmes. Il existe toutes sortes de tactiques, pour appliquer des théorèmes existants, raisonner par récurrence, résoudre des inégalités, ou même effectuer de la recherche automatique de démonstration, ce qui s’avère extrêmement utile pour simplifier les preuves.

Ce mode « tactiques » permet aussi d’écrire la preuve de façon incrémentale, en faisant un point d’étape après chaque tactique pour voir ce qui est prouvé et ce qui reste à prouver. Voici par exemple ce qu’affiche Rocq après le destruct et avant le split :

P, Q : Prop p : P q : Q ============================ Q /\ P

Cette notation signifie que le contexte ambiant contient les variables P et Q de type Prop ainsi que p une preuve de P (donc un élément du type P) et q une preuve de Q. Le Q /\ P en dessous de la barre horizontale est le but à prouver, c’est-à-dire le type dont on cherche à construire un élément.

Agda fonctionne assez différemment : il n’y a pas de tactiques, mais il existe néanmoins un système de méta-programmation qui sert à faire de la recherche de preuves (donc contrairement à Rocq et Lean, on n’écrit pas la majeure partie des preuves avec des tactiques, mais on peut se servir d’un équivalent quand c’est utile). Pour écrire les preuves incrémentalement, on met ? dans le programme quand on veut ouvrir une sous-preuve, et Agda va faire le type-checking de tout le reste et donner le contexte à l’endroit du ?.

Quelques succès de la formalisation

En 2025, la formalisation reste très fastidieuse, mais elle a déjà eu plusieurs grands succès :

• Le théorème des quatre couleurs, formalisé en Rocq (2005).
• Le théorème de Feit-Thompson (étape dans la fameuse classification des groupes finis simples) en Rocq (2012).
• Un théorème de Peter Scholze sur les « espaces vectoriels liquides » en Lean (2022).
• Le retournement de la sphère en Lean (2022).
• La valeur de BB(5) en Rocq (2024).

Actuellement, Lean a réussi à attirer une communauté de mathématiciens qui développent mathlib (1,1 million de lignes de code Lean au moment où j’écris), une bibliothèque de définitions et théorèmes mathématiques qui vise à être la plus unifiée possible.

Les équivalents dans d’autres assistants de preuve se développent même s’ils ne sont pas (encore) aussi gros : citons mathcomp, unimath, agda-unimath entre autres.

Un autre grand succès, dans le domaine de la vérification cette fois, est CompCert (malheureusement non-libre), qui est un compilateur C entièrement écrit en Rocq et vérifié par rapport à une spécification du C également encodée en Rocq.

La recherche en théorie des types

La théorie des types est un domaine de recherche à part entière, qui vise à étudier du point de vue logique les théories des types existantes, et à en développer de nouvelles pour des raisons à la fois théoriques et pratiques.

Historiquement, une grande question de la théorie des types est celle de comprendre à quel type doivent correspondre les propositions d’égalité. Par exemple, on veut que deux propositions équivalentes soient égales, et que deux fonctions qui prennent les mêmes valeurs soient égales, et éventuellement pour diverses raisons que deux preuves de la même proposition soient égales, mais s’il est facile d’ajouter toutes ces choses comme axiomes, il est très compliqué de les rendre prouvables sans obtenir, comme avec le tiers exclu, des programmes qui ne peuvent pas s’exécuter à cause des axiomes qui sont déclarés sans définition.

Vladimir Voedvodsky a fait une contribution majeure en proposant un nouvel axiome, appelé univalence, qui dit très sommairement que si deux types ont la même structure (on peut donner une « équivalence » entre les deux), alors ils sont en fait égaux (résumé simpliste à ne pas prendre au mot). Cet axiome est très pratique pour faire des maths parce qu’on travaille souvent avec des objets qui ont la même structure (on dit qu’ils sont isomorphes), et qui doivent donc avoir les mêmes propriétés, et cet axiome permet de les identifier (même s’il a aussi des conséquences qui peuvent paraître choquantes). Sa proposition a donné naissance à une branche appelée théorie homotopique des types, qui explore les maths avec univalence. Le prix à payer est que les types ne se comprennent plus comme de simples ensembles de valeurs (ou de preuves d’une proposition), mais comme des espaces géométriques munis de toute une structure complexe (techniquement, les égalités sont des chemins entre points, et il y a des égalités non-triviales, des égalités entre égalités, etc.), et la compréhension de ces espaces-types est fondée sur la théorie de l’homotopie. Il y a bien d’autres théories des types, avec univalence ou non : théorie cubique des types, théorie des types observationnelle, etc.

Conclusion

J’espère avoir communiqué un peu de mon enthousiasme pour le domaine (dans lequel je suis probablement parti pour démarrer une thèse). Si vous voulez apprendre un assistant de preuve, une ressource assez abordable est la série Software Foundations avec Rocq. Il existe également Theorem proving in Lean 4 et divers tutoriels Agda. Vous pouvez aussi essayer ces assistants de preuve directement dans votre navigateur : Rocq, Lean ou Agda. Et bien sûr les installer et jouer avec : Rocq, Lean, Agda.

Télécharger ce contenu au format EPUB

Commentaires : voir le flux Atom ouvrir dans le navigateur

L'OMJC organise avec l'Association Club Linux Nord Pas de Calais organise chaque samedi une permanence Logiciels Libres ouverte à tous, membre de l'association ou non, débutant ou expert, curieux ou passionné.

Le Centre d’Infos Jeunes a mis en place une démarche d’accompagnement des jeunes aux pratiques actuelles pour l’informatique et le numérique : * Lieu d’accès public à Internet ( 5 postes avec Wifi libre et gratuit ) * Web collaboratif et citoyen pour que chacun puisse trouver sa place et passer du rôle de simple usager à celui d’initiateur de processus collaboratif * Éducation à l’information par les nouveaux médias ( diffusion par le biais du numérique ) * Logiciels libres ( bureautique, sites, blogs, cloud, infographie et vidéo, musique, réseaux sociaux, chat, … ).

Cette rencontre a lieu sur rendez-vous, tous les samedis matins hors vacances scolaires à la Maison communale de la ferme Dupire, rue Yves Decugis à VILLENEUVE D’ASCQ

Calendrier Web, regroupant des événements liés au Libre (logiciel, salon, atelier, install party, conférence), annoncés par leurs organisateurs. Voici un récapitulatif de la semaine à venir. Le détail de chacun de ces 37 événements (France: 34, internet: 3) est en seconde partie de dépêche.

• lien nᵒ 1 : April
• lien nᵒ 2 : Agenda du Libre
• lien nᵒ 3 : Carte des événements
• lien nᵒ 4 : Proposer un événement
• lien nᵒ 5 : Annuaire des organisations
• lien nᵒ 6 : Agenda de la semaine précédente
• lien nᵒ 7 : Agenda du Libre Québec

Sommaire

• • [FR Montpellier] Émission | Radio FM-Plus | Temps Libre | Diffusion – Le lundi 24 février 2025 de 09h00 à 10h00.
  • [internet] Mapathon 2024-2025 par CartONG – Le lundi 24 février 2025 de 18h00 à 20h00.
  • [FR Saint-Étienne] OpenStreetMap, rencontre Saint-Étienne et sud Loire – Le lundi 24 février 2025 de 19h00 à 21h00.
  • [internet] Émission «Libre à vous!» – Le mardi 25 février 2025 de 15h30 à 17h00.
  • [FR Vallauris – Sophia Antipolis] Rencontre Accès Libre – Le mardi 25 février 2025 de 18h00 à 21h00.
  • [FR Pau] Assemblée générale de l’association PauLLA – Le mardi 25 février 2025 de 19h00 à 22h00.
  • [FR Lille] Permanence associative autour du Libre – Le mardi 25 février 2025 de 20h00 à 22h00.
  • [internet] Permanence numérique (visio) – Le mardi 25 février 2025 de 20h00 à 21h30.
  • [FR Le Mans] Permanence du mercredi – Le mercredi 26 février 2025 de 12h30 à 17h00.
  • [FR Le Blanc] Ateliers “Libres” – Le mercredi 26 février 2025 de 14h00 à 14h00.
  • [FR Le Blanc] Ateliers “Libres” de Linux au Blanc – Le mercredi 26 février 2025 de 14h00 à 17h00.
  • [FR Pessac] Cours gratuit d’Espéranto, langue Libre – Le mercredi 26 février 2025 de 17h30 à 19h00.
  • [FR Vandœuvre-lès-Nancy] Réunion OpenStreetMap – Le mercredi 26 février 2025 de 18h00 à 20h00.
  • [FR Beauvais] Sensibilisation et partage autour du Libre – Le mercredi 26 février 2025 de 18h00 à 20h00.
  • [FR Simandre] Causerie numérique – Le mercredi 26 février 2025 de 18h00 à 20h00.
  • [FR Parempuyre] Participez au prochain ĞBlabla – Le mercredi 26 février 2025 de 18h30 à 22h30.
  • [FR Saint Laurent du Pont] Permanence Rézine Chartreuse – Le mercredi 26 février 2025 de 19h00 à 20h00.
  • [FR Montpellier] Permanence | OpenStreetMap | HérOSM (hybride) – Le mercredi 26 février 2025 de 19h00 à 22h00.
  • [FR Joué-lès-Tours] Atelier du Libre – Le jeudi 27 février 2025 de 13h30 à 16h00.
  • [FR Sète] Permanence | GNU/Linux et Logiciels Libres – Le jeudi 27 février 2025 de 18h00 à 20h00.
  • [FR Toulouse] Repas du Libre – Le jeudi 27 février 2025 de 20h30 à 23h00.
  • [FR Quimperlé] Point info GNU/Linux – Le vendredi 28 février 2025 de 13h30 à 17h30.
  • [FR Lyon] Permanence contre l’obsolescence – Le vendredi 28 février 2025 de 16h00 à 18h30.
  • [FR Toulon] Install Partie Linux – Le vendredi 28 février 2025 de 17h00 à 21h00.
  • [FR Annecy] Réunion hebdomadaire AGU3L Logiciels Libres – Le vendredi 28 février 2025 de 20h00 à 23h59.
  • [FR Marignier] Utilisation d’internet – Le samedi 1 mars 2025 de 09h00 à 12h00.
  • [FR Contamine sur Arve] Bidouille Informatique – Le samedi 1 mars 2025 de 09h00 à 12h00.
  • [FR Vanves] Portes ouvertes – Installations – Dépannages – Le samedi 1 mars 2025 de 09h30 à 18h00.
  • [FR Figeac] Café bidouille, réparation informatique – Le samedi 1 mars 2025 de 10h00 à 13h00.
  • [FR Ivry sur Seine] Cours de l’École du Logiciel Libre – Le samedi 1 mars 2025 de 10h30 à 18h30.
  • [FR Rennes] Atelier Pixel Quest – Le samedi 1 mars 2025 de 14h00 à 17h00.
  • [FR Rennes] Atelier Pixel Quest – Le samedi 1 mars 2025 de 14h00 à 17h00.
  • [FR Le Mans] Permanence mensuelle du samedi – Le samedi 1 mars 2025 de 14h00 à 18h00.
  • [FR Quimper] Permanence Linux Quimper – Le samedi 1 mars 2025 de 16h00 à 18h00.
  • [FR Vire] Atelier Cartographie participative – Le samedi 1 mars 2025 de 17h00 à 19h00.
  • [FR Montigny Le Bretonneux] Soirée Cult' : Plongée dans l’univers du hacking – Le samedi 1 mars 2025 de 19h00 à 20h30.
  • [FR Gaillac] Repair café – Le dimanche 2 mars 2025 de 10h00 à 13h00.

[FR Montpellier] Émission | Radio FM-Plus | Temps Libre | Diffusion – Le lundi 24 février 2025 de 09h00 à 10h00.

Montpel'libre réalise une série d’émissions régulières à la Radio FM-Plus intitulées « Temps Libre ». Ces émissions sont la présentation hebdomadaire des activités de Montpel’libre.

Après le jingle où l’on présente brièvement Montpel'libre, nous donnerons un coup de projecteur sur les activités qui seront proposées prochainement.

Ces émissions seront l’occasion pour les auditeurs de découvrir plus en détails les logiciels libres et de se tenir informés des dernières actualités sur le sujet.

Alors, que vous soyez débutant ou expert en informatique, que vous ayez des connaissances avancées du logiciel libre ou que vous souhaitiez simplement en savoir plus, Montpel'libre, au travers de cette émission, se fera un plaisir pour répondre à vos attentes et vous accompagner dans votre découverte des logiciels libres, de la culture libre et des communs numériques.

Vous vous demandez peut-être ce qu’est un logiciel libre. Il s’agit simplement d’un logiciel dont l’utilisation, la modification et la diffusion sont autorisées par une licence qui garantit les libertés fondamentales des utilisateurs. Ces libertés incluent la possibilité d’exécuter, d’étudier, de copier, d’améliorer et de redistribuer le logiciel selon vos besoins.

Inscription | GPS 43.60524/3.87336

Fiche activité:
https://montpellibre.fr/fiches_activites/Fiche_A5_017_Emission_Radio_Montpellibre_2024.pdf

• Radio FM-Plus, 4 rue Saint Barthelemy, Montpellier, Occitanie, France
• https://montpellibre.fr
• montpel-libre, radio, fm-plus, temps-libre, diffusion

[internet] Mapathon 2024-2025 par CartONG – Le lundi 24 février 2025 de 18h00 à 20h00.

Vous voulez vous engager pour une cause, rencontrer de nouvelles personnes et découvrir la cartographie participative et humanitaire? CartONG vous invite à participer à un ou plusieurs mapathons en ligne!