Un peu creux pour l’instant, j’imagine que c’est pas les tentatives échouées de faire ce genre de chose par le passé qui ont manqué et qui ont aboutit à des échecs. Une analyse de ce qui a marché ou pas serait sans doute essentielle à la crédibilité, sous peine de n’être qu’une tentative de plus qui tombera dans les mêmes travers.
Aussi un truc me fait sourire, cette prétention à se débarrasser de l’idéologie …
il serait possible de proposer des solutions pragmatiques et non des constructions idéologiques
… Tout en nommant son machin « Institut national d’excellence en éducation », comme si ce terme n’avait rien d’idéologique. On devine d’entrée de jeu une orientation plutôt à droite ou il s’agit de favoriser des "premiers de cordées" qui réussiraient mieux que les autres, ou suis-je médisant ?
DPLL est l’algorithme derrière les solveurs comme z3, qui permettent de résoudre des problèmes de combinaisons logique de formules dans une théorie mathématique.
À l’origine l’algorithme était de "Davis Putnam", pour décider de la satisfaction de formules booléennes (c’est à dire de savoir s’il y a moyen de rendre une formule booléenne vraie en affectant des valeurs à ses variables). C’est un algorithme de recherche arborescente.
L’algorithme a été étendu (par d’autres) pour plus d’efficacité pour donner DPLL, qui a permis de résoudre des formules SAT de grande taille efficacement au fil des ans et des optimisations des solveurs, il y a une communauté qui travaille encore dessus.
Et par dessus a été rajouté avec DPLL(T) la possibilité de résoudre des formules non plus simplement booléennes, mais dans lesquels on a remplacés les booléens par des formules d’une théories, par exemple un ensemble d’équations. La résolution des équations est déléguées à un solveur "fils" à qui on file des ensembles de formule et qui dit si cet ensemble de formule est cohérent (a une solution) ou pas. Cet algorithme a fait florès, Microsoft a développé z3 https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ pour la communauté de la vérification logicielle entre autre, qui a eu son petit succès, autour.
Il semble cependant que si l’algorithme DP a fait florès, cette contribution est assez ignorée par la communauté mathématique qui le considère plus comme un historien de la logique.
C’est pas que ce soit marrant ou pas, c’est juste que faut savoir à qui tu t’adresses en faisant des leçons de morales sur le sourçage. L’auteur du journal, il sait qu’il trolle peu de chance que ça l’atteigne. Les lecteurs, ici, moinssent en masse, personne n’y croit spécialement.
En même temps ce journal posté là juste à brûle pourpoint sur un sujet HS ne fait même pas semblant d’être crédible et ressemble plus à un troll clickbait qu’autre chose.
D’un autre côté, si on commençait à vraiment sourcer absolument tout ce qu’on dit dans une conversation casual ça deviendrait assez vite invivable. S’il s’agit de faire la démonstration qu’il faut pas faire ça en postant un journal sur linuxfr HS c’est pas forcément représentatif de la situation ou on pourrait prendre des pincettes par incertitude au comptoir …
Le mode lecture semble ne donner accès qu’à un extrait de l’article chez moi (c’est annoncé 9 minutes de lectures et il y a uniquement 2 paragraphes, même lent le compte n’y est pas)
Sans vouloir minimiser le fait que c’est un phénomène qui existe, les détransitions, oui bien évidemment tu peux te douter que c’est bel et bien une panique morale utilisé par les transphobes : https://www.tandfonline.com/doi/abs/10.1080/13825577.2020.1730052 donc … à manier avec des pincettes évidemment. On doit avoir à peu prêt fait le tour de ce type d’arguments.
L’article détransition donne quelque clés, en particulier que c’est minoritaires, et que 5% des personnes semblent réellement regretter leur transition parce qu’elles se seraient trompé … la majorité semblent le faire pour des raisons sociales : pression de l’entourage ou difficulté à trouver du boulot du fait de rejet social.
Tu vas un peu vite sur les causes de la dépression. Est-ce l'état où les réactions de l'entourage, ou l'anticipation des réactions de l'entourage qui provoquent cette dépression ? C'est pas spécialement pareil, et sur ces sujets sensibles dire des contre verités peut faire plus de mal que de bien.
Ah oui, un truc à rajouter au résumer : dans le cas de l’humain et de différentes identitées de genre, on a bel et bien trouvé des corrélations entre genre et certaines structures cérébrales, ce qui fait bel et bien du genre une réalité biologique observable au moins dans certains cas.
Il s’agit de températures ou le risque de mourir est réel, rendant de fait le territoire non réellement habitable. Dans le désert par exemple, quasi personne ne vit parce que la survie est pas assurée. On sait aussi que sous les tropiques certaines combinaisons températures / humidité seront ou sont mortelles, l’humidité rend la transpiration inefficace donc impossible de survivre à l’extérieur, on crève de chaud. A partir de certains degrés de réchauffement ça pourra concernées des portions très peuplées de la planète, comme l’Inde … Ça c’est pas nouveau c’est dans les rapports du Giec.
L’article définit les zones habitable en extrapolant les densité de population actuelles en fonction des conditions climatiques, plus ou moins. En extrapolant les conditions futures, par des projections, tu trouves les zones ou les conditions futures sont incompatibles avec les densité actuelles ou les projections futures.
Oui c’est le revers de la médaille de trop d’expressivité, ça ouvre la possibilité d’être inutilement blessant ou de créer des formes d’ironies qui compliquent l’interprétation, l’inverse du résultat souhaité. Les émoticônes "je pleure de rire" sont fréquemment utilisées pour indiquer "c’est ridicule" sans discuter des arguments, par exemple.
Dans les systèmes de chat récents il y a la possibilité de mettre une "réaction" sous forme d’une émoticône à une réponse. Les autres participants peuvent abonder et il y a un décompte des gens qui partagent la réaction. C’est plus riche que "pertinent/inutile" et évite l’écueil de "faut deviner le pourquoi du comment de la note", dans une certaine mesure (faut avoir les codes pour savoir comment et pourquoi est utilisée une icône en particulier)
Que tu le veuilles ou non, tu as des chromosomes XX, ou XY, ou autre dans moins de 0.5% des cas (ce qui fait quand même beaucoup sur 8 milliards). Cette réalité biologique est bien différente de comme tu exprimes ton toi intérieur, ou même de qui est ton toi intérieur.
C’est un argument typique des transphobes. Et il est pas spécialement vrai, en tout cas dans ce qu’il implique : insister une fait que c’est une "réalité biologique" veut dire que la personne qui souhaiterait changer de sexe "nie" sa réalité biologique ("que tu le veuilles ou non"). De là à en conclure que "c’est dans la tête", il n’y a qu’un pas. Or c’est complètement faux de réduire la réalité biologique à une paire de chromosome. Faut pas s’étonner de semer la confusion, en reprenant des arguments caractérisiques transphobes faux.
Bonne vidéo, documentée et divertissante, qui détaille un peu la réalité biologique. TLDR : la réalité biologique, c’est toujours ultra compliqué et tout plein de variation, c’est vrai dans tout le vivant y compris chez l’homme et pour le sexe. Les exceptions sont en un sens la règle.
C’est tellement commun que des gens ont écris des bouquins sur les difficultés cognitives liées à la surabondances des choix : Surabondance_des_choix . Il y a des stratégies bien sûr, genre ne pas tenter d’obtenir "le meilleur" tout le temps, faire un choix peut être sous optimal mais qui convient.
Mais peut être que rejeter le problème sur l’utilisateur quand c’est un problème qui concerne tout le monde c’est pas spécialement utile.
Je n'explique pas aux gens ce qu'ils doivent ressentir. Je fais justement la distinction entre ce que tu as dans tes cellules et ce que tu ressens. Relis bien ce que j'ai écrit.
Relis bien mon commentaire parce que j’essaye d’expliquer que ce n’est pas "ce que tu as dans les cellules", c’est "ce que tu peux observer de ce que tu as dans les cellules", et que c’est réductionnistes de croire que ce que ce que tu as dans tes cellules ou dans ton corps se réduit à ce qui est observable. Un chromosome, c’est plein de gènes, deux mêmes chromosomes chez deux personnes différentes c’est pas les mêmes gènes, c’est pas les mêmes gènes exprimés, et caetera.
En bref, il se passe des trucs compliqués qu’on comprend pas forcément, peut-être des combinaisons d’expression des gènes complexes et pas "cohérentes" entre ce que tu peux observer et d’autres choses qui ne sont pas visibles dans la biologie ? Il me parait donc dangereux de faire du réductionnisme un peu bas du front qui masque probablement tout une partie de la réalité biologique pour expliquer aux gens ce qu’ils devraient ressentir. Tu crois que la nature en a quelque chose à faire de ta combinaison de chromosome ? Non, elle s’en fout. T’en as quelque chose à foutre que quelqu’un veuille changer de sexe ? Si la personne est prête à se bouffer des traitements à vie et à subir des opération un poil lourdes et les conséquences qui vont avec en surveillant ses niveaux d’hormones, elle est probablement motivée.
Mais a à beau être ludique, pas certain que ça les fasse rêver. Pour ceux qui aiment les jeux vidéos par exemple il y a une marge entre avoir ça dans les doigts et penser coder leur jeu préféré. Il y a potentiellement comme un gouffre.
Avec des combinaisons de preuves automatique sur le code généré ça va commencer à être très intéressant https://twitter.com/johnterickson/status/1665773713353216000 (si il est capable de générer des tests, il va pouvoir générer des specs aussi)
(bon, c’est pas forcément un bon exemple parce que modéliser un jeu à deux joueurs par une simple formule SAT c’est peut être généralement pas possible, mais on peut modéliser des sous problèmes)
On peut modéliser le jeu d'échecs par une formule sat. Il y a pas besoin d'ia pour résoudre satw par conséquent il y p pas besoin d'ia pour jouer aux échecs.
Encore une fois recherche opérationnelle ou simplement les algo de résolution de problème NP-complet. aptitude n'a pas besoin d'IA pour résoudre un SAT-3.
Les problèmes de dépendances ne sont pas forcément les problèmes les plus compliqués qu’on puisse générer avec SAT donc ils ne nécessitent pas forcément de mettre en œuvre les algorithmes les plus malins pour résoudre les formules. Faudrait mettre aptitude sur les problèmes de https://satcompetition.github.io/2023/ pour voir comment il s’en sort ! Dans mon souvenir son solveur s’en sortait pas bien déjà dans certains cas de résolution de dépendance dans le temps. L’opposition avec la recherche opérationnelle, je dirai que ça a pas spécialement de sens vu qu’il n’y a aucun obstacle a utiliser des méthodes d’IA en RO. Il faut chercher la définition ailleurs.
Un des trucs que perso j’utiliserai pour caractériser une IA, c’est qu’elle a besoin de mémoire pour se faire "sa propre" représentation du problème, non établie à l’avance. Par exemple un robot qui doit agir dans un environnement peut avoir à se fabriquer un plan interne de cet environnement, un modèle, il a besoin de mémoire pour ça. Ensuite si on lui fait effectuer un parcours dans cet environnement il pourra l’utiliser pour planifier ce parcours, et prévoir des éventuelles difficultés le cas échéant …
Une IA doit être capable de résoudre un problème qu’on peut considérer comme non trivial sans avoir été spécifiquement conçue pour résoudre ce problème.
Par extension, vu qu’on peut exprimer n’importe quel problème NP-complet sous la forme de SAT, mais qu’il n’est pas évident qu’un algorithme générique de SAT soit bon pour résoudre les instances spécifiques générées pour résoudre un autre problème, un solveur SAT "intelligent" devrait être capable d’exploiter la structure spécifique générée par ce problème sans qu’on la lui ait expliqué ou conçu pour. Donc, plus que "générer un algorithme"
On ne veut pas détailler l'algorithme donc on tente de le générer.
Ou alors c’est trop pénible de détailler l’algorithme donc on tente de généraliser en en concevant un qui permettra de résoudre ce problème et aussi une vaste classe de problème similaires au lieu de juste "reconnaître super bien une vache". Après oui, il faut que le résultat soit "opérationnel", en ce sens on peut parler d’algorithme. Ton histoire me fait un peu penser à l’extraction de programme en preuve automatique de théorème : https://www.fing.edu.uy/~amiquel/publis/hdr.pdf une fois qu’on a démontré un théorème on peut, mais c’est pas nécessairement obligé je crois, ça dépend des système de preuve (il faut que ce soit "constructif", en extraire un programme qui pourrait résoudre des problèmes correspondant au théorème. Mais je suis pas certain que dans le cas général de l’IA, ce soit vraiment nécessaire d’extraire un algorithme spécifique de la procédure de résolution. Notamment parce qu’en imaginant un processus évolutif ce soit potentiellement plus efficace d’être dynamique et de suivre un certain algorithme dans certains cas, genre au début de procédure, mais de réagir à certains autre moment ou cet "algorithme" montre son inefficacité et de faire évoluer la procédure vers autre chose.
# Démarche intéressante mais …
Posté par thoasm . En réponse au lien Enseigner à l’aveugle, sans données fiables ni avis sérieux . Évalué à 3.
Un peu creux pour l’instant, j’imagine que c’est pas les tentatives échouées de faire ce genre de chose par le passé qui ont manqué et qui ont aboutit à des échecs. Une analyse de ce qui a marché ou pas serait sans doute essentielle à la crédibilité, sous peine de n’être qu’une tentative de plus qui tombera dans les mêmes travers.
Aussi un truc me fait sourire, cette prétention à se débarrasser de l’idéologie …
… Tout en nommant son machin « Institut national d’excellence en éducation », comme si ce terme n’avait rien d’idéologique. On devine d’entrée de jeu une orientation plutôt à droite ou il s’agit de favoriser des "premiers de cordées" qui réussiraient mieux que les autres, ou suis-je médisant ?
# Le "D" de DPLL
Posté par thoasm . En réponse au lien Martin Davis (1928–2023). Évalué à 7.
DPLL est l’algorithme derrière les solveurs comme z3, qui permettent de résoudre des problèmes de combinaisons logique de formules dans une théorie mathématique.
À l’origine l’algorithme était de "Davis Putnam", pour décider de la satisfaction de formules booléennes (c’est à dire de savoir s’il y a moyen de rendre une formule booléenne vraie en affectant des valeurs à ses variables). C’est un algorithme de recherche arborescente.
L’algorithme a été étendu (par d’autres) pour plus d’efficacité pour donner DPLL, qui a permis de résoudre des formules SAT de grande taille efficacement au fil des ans et des optimisations des solveurs, il y a une communauté qui travaille encore dessus.
Et par dessus a été rajouté avec DPLL(T) la possibilité de résoudre des formules non plus simplement booléennes, mais dans lesquels on a remplacés les booléens par des formules d’une théories, par exemple un ensemble d’équations. La résolution des équations est déléguées à un solveur "fils" à qui on file des ensembles de formule et qui dit si cet ensemble de formule est cohérent (a une solution) ou pas. Cet algorithme a fait florès, Microsoft a développé z3 https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/ pour la communauté de la vérification logicielle entre autre, qui a eu son petit succès, autour.
Il semble cependant que si l’algorithme DP a fait florès, cette contribution est assez ignorée par la communauté mathématique qui le considère plus comme un historien de la logique.
[^] # Re: Ça vient d'où ?
Posté par thoasm . En réponse au journal Ne pas subir son couple.. Évalué à 4.
Quelques éléments de bio : https://www.letemps.ch/societe/albert-einstein-devoile-entre-femmes-fbi
[^] # Re: Ça vient d'où ?
Posté par thoasm . En réponse au journal Ne pas subir son couple.. Évalué à 6.
C’est pas que ce soit marrant ou pas, c’est juste que faut savoir à qui tu t’adresses en faisant des leçons de morales sur le sourçage. L’auteur du journal, il sait qu’il trolle peu de chance que ça l’atteigne. Les lecteurs, ici, moinssent en masse, personne n’y croit spécialement.
[^] # Re: Ça vient d'où ?
Posté par thoasm . En réponse au journal Ne pas subir son couple.. Évalué à 6.
En même temps ce journal posté là juste à brûle pourpoint sur un sujet HS ne fait même pas semblant d’être crédible et ressemble plus à un troll clickbait qu’autre chose.
[^] # Re: Ça vient d'où ?
Posté par thoasm . En réponse au journal Ne pas subir son couple.. Évalué à 4.
D’un autre côté, si on commençait à vraiment sourcer absolument tout ce qu’on dit dans une conversation casual ça deviendrait assez vite invivable. S’il s’agit de faire la démonstration qu’il faut pas faire ça en postant un journal sur linuxfr HS c’est pas forcément représentatif de la situation ou on pourrait prendre des pincettes par incertitude au comptoir …
[^] # Re: Le Pire et Avenir
Posté par thoasm . En réponse au lien Des parlementaires européens rejettent la loi sur la restauration de la nature. Évalué à 6.
Le mode lecture semble ne donner accès qu’à un extrait de l’article chez moi (c’est annoncé 9 minutes de lectures et il y a uniquement 2 paragraphes, même lent le compte n’y est pas)
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 9.
Sans vouloir minimiser le fait que c’est un phénomène qui existe, les détransitions, oui bien évidemment tu peux te douter que c’est bel et bien une panique morale utilisé par les transphobes : https://www.tandfonline.com/doi/abs/10.1080/13825577.2020.1730052 donc … à manier avec des pincettes évidemment. On doit avoir à peu prêt fait le tour de ce type d’arguments.
L’article détransition donne quelque clés, en particulier que c’est minoritaires, et que 5% des personnes semblent réellement regretter leur transition parce qu’elles se seraient trompé … la majorité semblent le faire pour des raisons sociales : pression de l’entourage ou difficulté à trouver du boulot du fait de rejet social.
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 6.
Tu vas un peu vite sur les causes de la dépression. Est-ce l'état où les réactions de l'entourage, ou l'anticipation des réactions de l'entourage qui provoquent cette dépression ? C'est pas spécialement pareil, et sur ces sujets sensibles dire des contre verités peut faire plus de mal que de bien.
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 5.
Ah oui, un truc à rajouter au résumer : dans le cas de l’humain et de différentes identitées de genre, on a bel et bien trouvé des corrélations entre genre et certaines structures cérébrales, ce qui fait bel et bien du genre une réalité biologique observable au moins dans certains cas.
[^] # Re: Légende ?
Posté par thoasm . En réponse au lien Climat : deux milliards de personnes pourraient être exposées à une chaleur extrême d’ici à 2100. Évalué à 7.
Il y a des réponses dans l’article publié dans Nature : https://www.nature.com/articles/s41893-023-01132-6
Il s’agit de températures ou le risque de mourir est réel, rendant de fait le territoire non réellement habitable. Dans le désert par exemple, quasi personne ne vit parce que la survie est pas assurée. On sait aussi que sous les tropiques certaines combinaisons températures / humidité seront ou sont mortelles, l’humidité rend la transpiration inefficace donc impossible de survivre à l’extérieur, on crève de chaud. A partir de certains degrés de réchauffement ça pourra concernées des portions très peuplées de la planète, comme l’Inde … Ça c’est pas nouveau c’est dans les rapports du Giec.
L’article définit les zones habitable en extrapolant les densité de population actuelles en fonction des conditions climatiques, plus ou moins. En extrapolant les conditions futures, par des projections, tu trouves les zones ou les conditions futures sont incompatibles avec les densité actuelles ou les projections futures.
[^] # Re: Est-ce vraiment un système d'auto-modération ?
Posté par thoasm . En réponse au journal Suggestion : supprimer complètement les notes du site. Évalué à 10.
Oui c’est le revers de la médaille de trop d’expressivité, ça ouvre la possibilité d’être inutilement blessant ou de créer des formes d’ironies qui compliquent l’interprétation, l’inverse du résultat souhaité. Les émoticônes "je pleure de rire" sont fréquemment utilisées pour indiquer "c’est ridicule" sans discuter des arguments, par exemple.
[^] # Re: Est-ce vraiment un système d'auto-modération ?
Posté par thoasm . En réponse au journal Suggestion : supprimer complètement les notes du site. Évalué à 7.
Dans les systèmes de chat récents il y a la possibilité de mettre une "réaction" sous forme d’une émoticône à une réponse. Les autres participants peuvent abonder et il y a un décompte des gens qui partagent la réaction. C’est plus riche que "pertinent/inutile" et évite l’écueil de "faut deviner le pourquoi du comment de la note", dans une certaine mesure (faut avoir les codes pour savoir comment et pourquoi est utilisée une icône en particulier)
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 2.
C’est un argument typique des transphobes. Et il est pas spécialement vrai, en tout cas dans ce qu’il implique : insister une fait que c’est une "réalité biologique" veut dire que la personne qui souhaiterait changer de sexe "nie" sa réalité biologique ("que tu le veuilles ou non"). De là à en conclure que "c’est dans la tête", il n’y a qu’un pas. Or c’est complètement faux de réduire la réalité biologique à une paire de chromosome. Faut pas s’étonner de semer la confusion, en reprenant des arguments caractérisiques transphobes faux.
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 6.
Bonne vidéo, documentée et divertissante, qui détaille un peu la réalité biologique. TLDR : la réalité biologique, c’est toujours ultra compliqué et tout plein de variation, c’est vrai dans tout le vivant y compris chez l’homme et pour le sexe. Les exceptions sont en un sens la règle.
[^] # Re: So what?
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 10.
C’est tellement commun que des gens ont écris des bouquins sur les difficultés cognitives liées à la surabondances des choix : Surabondance_des_choix . Il y a des stratégies bien sûr, genre ne pas tenter d’obtenir "le meilleur" tout le temps, faire un choix peut être sous optimal mais qui convient.
Mais peut être que rejeter le problème sur l’utilisateur quand c’est un problème qui concerne tout le monde c’est pas spécialement utile.
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 5.
Relis bien mon commentaire parce que j’essaye d’expliquer que ce n’est pas "ce que tu as dans les cellules", c’est "ce que tu peux observer de ce que tu as dans les cellules", et que c’est réductionnistes de croire que ce que ce que tu as dans tes cellules ou dans ton corps se réduit à ce qui est observable. Un chromosome, c’est plein de gènes, deux mêmes chromosomes chez deux personnes différentes c’est pas les mêmes gènes, c’est pas les mêmes gènes exprimés, et caetera.
[^] # Re: pareil mais
Posté par thoasm . En réponse au journal Linus Torvalds proclame sa wokeness . Évalué à 3.
La forme des chromosomes dit peu de l’expression des gènes sur ces chromosomes. Et la biologie réserves parfois quelques surprises, https://fr.wikipedia.org/wiki/Syndrome_du_m%C3%A2le_XX par exemple, ou encore la disparition programmée du chromosome Y chez les mammifères, avec des espèces ou c’est déjà arrivé [https://www.sciencesetavenir.fr/archeo-paleo/evolution/evolution-le-chromosome-masculin-en-voie-de-disparition_170989 sans pour autant que les mâles aient disparus].
En bref, il se passe des trucs compliqués qu’on comprend pas forcément, peut-être des combinaisons d’expression des gènes complexes et pas "cohérentes" entre ce que tu peux observer et d’autres choses qui ne sont pas visibles dans la biologie ? Il me parait donc dangereux de faire du réductionnisme un peu bas du front qui masque probablement tout une partie de la réalité biologique pour expliquer aux gens ce qu’ils devraient ressentir. Tu crois que la nature en a quelque chose à faire de ta combinaison de chromosome ? Non, elle s’en fout. T’en as quelque chose à foutre que quelqu’un veuille changer de sexe ? Si la personne est prête à se bouffer des traitements à vie et à subir des opération un poil lourdes et les conséquences qui vont avec en surveillant ses niveaux d’hormones, elle est probablement motivée.
[^] # Re: Rien de nouveau sous le soleil
Posté par thoasm . En réponse au journal Les jeunes aiment les smartphones, mais pas le numérique. Évalué à 6.
Il y a toujours moyen de tenter de leur refiler https://scratch.mit.edu/ scratch ou des variantes comme https://www.supercodingball.com/ c’est adapté pour coder avec glisser / déplacer.
Mais a à beau être ludique, pas certain que ça les fasse rêver. Pour ceux qui aiment les jeux vidéos par exemple il y a une marge entre avoir ça dans les doigts et penser coder leur jeu préféré. Il y a potentiellement comme un gouffre.
[^] # Re: Copilot et Copilot chat sont fabuleux
Posté par thoasm . En réponse au journal AI générative pour scripter en Python ?. Évalué à 5.
Avec des combinaisons de preuves automatique sur le code généré ça va commencer à être très intéressant https://twitter.com/johnterickson/status/1665773713353216000 (si il est capable de générer des tests, il va pouvoir générer des specs aussi)
[^] # Re: Pandémie !
Posté par thoasm . En réponse au journal Vraiment toujours pas convaincu par l'Hydroxychloroquine ?. Évalué à 7.
Seuls les complotistes ont leur réponse avant même que la question soit posée.
[^] # Re: Pandémie !
Posté par thoasm . En réponse au journal Vraiment toujours pas convaincu par l'Hydroxychloroquine ?. Évalué à 7.
Ils se reconnaissent parce qu’ils ont un index beaucoup plus long que le notre.
[^] # Re: Simulation
Posté par thoasm . En réponse au journal Une simulation de drone de combat qui tourne mal. Évalué à 3. Dernière modification le 04 juin 2023 à 10:08.
(bon, c’est pas forcément un bon exemple parce que modéliser un jeu à deux joueurs par une simple formule SAT c’est peut être généralement pas possible, mais on peut modéliser des sous problèmes)
[^] # Re: Simulation
Posté par thoasm . En réponse au journal Une simulation de drone de combat qui tourne mal. Évalué à 4.
On peut modéliser le jeu d'échecs par une formule sat. Il y a pas besoin d'ia pour résoudre satw par conséquent il y p pas besoin d'ia pour jouer aux échecs.
[^] # Re: Simulation
Posté par thoasm . En réponse au journal Une simulation de drone de combat qui tourne mal. Évalué à 4.
Les problèmes de dépendances ne sont pas forcément les problèmes les plus compliqués qu’on puisse générer avec SAT donc ils ne nécessitent pas forcément de mettre en œuvre les algorithmes les plus malins pour résoudre les formules. Faudrait mettre aptitude sur les problèmes de https://satcompetition.github.io/2023/ pour voir comment il s’en sort ! Dans mon souvenir son solveur s’en sortait pas bien déjà dans certains cas de résolution de dépendance dans le temps. L’opposition avec la recherche opérationnelle, je dirai que ça a pas spécialement de sens vu qu’il n’y a aucun obstacle a utiliser des méthodes d’IA en RO. Il faut chercher la définition ailleurs.
Un des trucs que perso j’utiliserai pour caractériser une IA, c’est qu’elle a besoin de mémoire pour se faire "sa propre" représentation du problème, non établie à l’avance. Par exemple un robot qui doit agir dans un environnement peut avoir à se fabriquer un plan interne de cet environnement, un modèle, il a besoin de mémoire pour ça. Ensuite si on lui fait effectuer un parcours dans cet environnement il pourra l’utiliser pour planifier ce parcours, et prévoir des éventuelles difficultés le cas échéant …
Une IA doit être capable de résoudre un problème qu’on peut considérer comme non trivial sans avoir été spécifiquement conçue pour résoudre ce problème.
Par extension, vu qu’on peut exprimer n’importe quel problème NP-complet sous la forme de SAT, mais qu’il n’est pas évident qu’un algorithme générique de SAT soit bon pour résoudre les instances spécifiques générées pour résoudre un autre problème, un solveur SAT "intelligent" devrait être capable d’exploiter la structure spécifique générée par ce problème sans qu’on la lui ait expliqué ou conçu pour. Donc, plus que "générer un algorithme"
Ou alors c’est trop pénible de détailler l’algorithme donc on tente de généraliser en en concevant un qui permettra de résoudre ce problème et aussi une vaste classe de problème similaires au lieu de juste "reconnaître super bien une vache". Après oui, il faut que le résultat soit "opérationnel", en ce sens on peut parler d’algorithme. Ton histoire me fait un peu penser à l’extraction de programme en preuve automatique de théorème : https://www.fing.edu.uy/~amiquel/publis/hdr.pdf une fois qu’on a démontré un théorème on peut, mais c’est pas nécessairement obligé je crois, ça dépend des système de preuve (il faut que ce soit "constructif", en extraire un programme qui pourrait résoudre des problèmes correspondant au théorème. Mais je suis pas certain que dans le cas général de l’IA, ce soit vraiment nécessaire d’extraire un algorithme spécifique de la procédure de résolution. Notamment parce qu’en imaginant un processus évolutif ce soit potentiellement plus efficace d’être dynamique et de suivre un certain algorithme dans certains cas, genre au début de procédure, mais de réagir à certains autre moment ou cet "algorithme" montre son inefficacité et de faire évoluer la procédure vers autre chose.