à propos de l’automate [trop long pour un commentaire]

Dans une première version du commentaire auquel vous m’avez fait la joie de répondre, j’avais dressé une liste non exhaustive des qualités-type que j’estimais nécessaires pour chercher des preuves, puis j’ai supprimé ces passages car réalisé que seule une approche proche du machine learning serait en mesure de traiter ces problèmes efficacement sous l’angle que je préconisais . En effet, les stratégies que je proposais pour tenter d’implémenter ces qualités artificiellement, me semblaient trop reposer sur des compétences non GOFAI.  Après réflexion, je pense qu’il y a peut-être une alternative GOFAI à ces problématiques.  Je vais donc énoncer ces qualités-types ici et quand même résumer l’approche que j’aurais proposée s’il n’y avait pas les restrictions au GOFAI. Le but de ceci est non seulement d’être bien certain que ces pistes sont à écarter, mais aussi (et surtout) de proposer les alternatives GOFAI qui me sont venues. Une troisième raison de partager ces ébauches d’idées est que certaines pourraient quand même être pertinentes, à plus forte raison si un jour, un couplage avec du machine learning était à envisager…

 Les 5 points de votre texte de présentation qui pointent les lacunes du machine learning (ML) ne sont pas, me semble-t-il, propres au machine learning mais à l’intelligence artificielle en général, et la notion de machine learning orienté humain me semble avoir autant de sens (si ce n’est plus) que la notion homologue GOFAI. Ceci est d’ailleurs corroboré par la mince expérience qu’on a notamment avec Alpha Zero aux échecs : il y a des coups étranges « sortis du chapeau »…à première vue… mais pas plus que la plupart des coups de  Stockfish, le meilleur GOFAI en date (peut-être que ce n’est pas du GOFAI stricto-sensu mais peu importe…) Et non seulement il n’y a pas plus de « coups sortis du chapeau » chez Alpha Zero, mais en plus on peut les justifier stratégiquement (aux échecs : stratégie = long terme), ce qui était très souvent impossible pour les « coups sortis du chapeau » de stockfish, car la pertinence de ces coups n’était  principalement due qu’à des prouesses combinatoires (tactique = court terme) tandis que les coups proposés par Alpha Zero  (supérieur à Stockfish) avaient en plus une justification stratégique palpable et en adéquation avec les principes élaborés par les humains pour palier justement à ses lacunes combinatoires : une fois gommée la supériorité combinatoire du court terme (supérieure chez Stockfish mais pas assez pour battre Alpha Zero) , c’est bien des principes stratégiques qui font la différence, et  le monde des échecs a été en quelque sorte rassuré de constater la confirmation des « grands principes stratégiques » qu’on aurait pu, à tort, croire invalidé par Stockfish et ses prédécesseurs, et qu’Alpha Zero a « trouvé tout seul ».

 Je dis cela pour justifier que je ne vois pas de contradictions à la recherche d’un ML orienté humain (et donc je ne pense pas que ça soit spécifiquement « l’orienté humain » qui opposent ML et GOFAI). Peut-être que le ML orienté humain n’est pas assez fouillé par ceux qui travaillent sur la question (je n’en sais rien) mais ça c’est autre chose.

 Ce qui semble propre au ML est qu’on n’a pas de prise sur le rendu, et ceci a tendance à faire passer le machine learning pour une discipline moins noble (d’autant que les maths qu’il y a derrière sont réputées moins poussées, il me semble), mais selon moi ça n’est qu’une catégorisation arbitraire étroitement liée à la culture mathématique actuelle. Et si on regarde le ML comme un cas parmi d’autre, d’automate cellulaire randomisé, ce qui parait « moins mathématique » (le fait qu’on ait pas de prise sur le rendu) devient au contraire, sous cet angle, fortement digne d’intérêt mathématique, et le fait de ne pas « comprendre d’où ça vient » (localement à propos de tel ou tel problème précis résolu par l’automate, ou globalement  : quels sont les principes statistiques, logiques, etc. qui  favorisent ce phénomène remarquable?) est, sous cet angle encore, intéressant au même titre que tout problème mathématique qu’on ne comprend pas bien…

 Pour moi, l’homme et le ML ne sont pas opposés par le point 3 ( Learning based on just a small number of examples.) d’une part parce que l’homme a lui même beaucoup appris avant de ne pouvoir se contenter que d’un « small set of example » et d’autre part parce qu’on peut imaginer une fois l’apprentissage d’un automate ML assez poussé, qu’il lui suffirait de peu d’exemples (et de la définition d’un cadre de routine) pour qu’il soit en mesure d’en tirer parti efficacement dans le cadre qu’on aura défini. Je pense comprendre, d’après votre expertise, que  ce n’est pas le cas à l’heure actuelle des recherches, mais, encore une fois, je ne pense pas que ça soit spécifique au ML vs GOFAI…

 Je dis cela non pas pour fuir le problème et l’angle GOFAI, mais au contraire pour l’aborder sous un angle autre que l’opposition, car cette opposition laisse croire qu’il y a une contradiction fondamentale entre ces deux approches ; ainsi comme parfois on le fait en maths, je propose ici d’étendre provisoirement  le problème en gardant toutes les exigences du projet excepté  la contrainte GOFAI, dans le but d’exhiber des caractéristiques dont on a besoin, ainsi que celles qu’on pourrait rechercher, pour ensuite viser ces caractéristiques, si/quand c’est possible (et quitte à les adapter), dans le but de s’en inspirer pour une approche exclusivement GOFAI. 

 Cela me semble être une ligne de conduite prometteuse à condition de savoir différencier ce qui relie les deux approches de ce qui les distingue fondamentalement (en observant que sur un beaucoup plus long terme, et en cas de succès, ce qui les relie tendra à s’imposer face à ce qui les distingue, qui ne sera, dès lors, qu’anecdotique).

Voici  quelques idées (dont certaines sont presque « concrètes ») , assorties du  cheminement qui m’y a mené.

Le recul

La faculté de se questionner, ou bien en généralisant ou bien en sortant du cadre d’une étude minutieuse est je pense fortement  liée à la fois à notre façon de résoudre les problèmes et à celle de sélectionner ceux qui nous intéressent. Ainsi, offrir la possibilité à un automate de « challenger » ses fondements me semble digne d’intérêt, cependant comme je l’ai dit précédemment ceci me semble PRESQUE indissociable des méthodes d’apprentissage statistique. Comme je l’ai évoqué dans le  commentaire, il est possible que la notion de  « faculté de réplication » de nature fractale qui baigne notre univers soit l’expression d’un principe fondamental des mathématiques (au sens où, par exemple, la loi des grands nombres est un résultat mathématique avant d’être un concept physique) et que le fait que nous, humains, soyons portés à explorer le « meta », à prendre du recul, et j’irai même jusqu’à dire, à identifier ces mêmes phénomènes (méta^2)…. soit encore une expression de ce principe naturel en action (peut-être, je le redis,  de nature aussi mathématique que l’est la loi normale).

Dans ces conditions et vu l’importance des sélections statistiques qui ont forgé notre perception, nos images mentales, nos maths, etc. il semble sans doute tentant de diriger un apprentissage machine de façon subtile pour que son objet (ou du moins un de ses objets) soient liés au meta (j’ai toujours l’impression d’être peu rigoureux, voire « fumiste »  quand j’emploie ce terme, mais comme ce mail est long, je ne veux pas l’allonger davantage par trop de pincettes et d’efforts de modestie terminologique)

Si cette piste tentante (apprentissage statistique) ne peut être employée en GOFAI, on peut néanmoins espérer deux choses :

a) Pour rester dans $M\subset B$ on a pas « vraiment » besoin de ça

b) Il existe une façon de tirer parti de ces phénomènes sans avoir recours à de l’apprentissage statistique

…peut être aussi une combinaisons de a) et b)

c) Certains principes peuvent être appliqués à *$M$* pour une efficacité tangible, certes approximative, en vue d’obtenir  une capacité effective proche de notre aptitude à  « se remettre en question », et plus généralement à  « poser des questions » pour espérer mieux en/les résoudre.. 

 Ceci relève peut-être du fantasme mais imaginons qu’on identifie un peu certaines caractéristiques du « principe de réplication fractale » (PRF) dont j’ai parlé tout à l’heure, un concept flou, certes, mais qui est omniprésent dans notre univers (et dont je soupçonnais tout à l’heure qu’il puisse être en quelque sorte, plus fondamental encore que le temps ou l’espace, en effet, si par exemple l’espace et le temps étaient des grandeurs physiques émergentes, comme certains physiciens sont portés à le croire, le PRF serait en quelque sorte plus fondamental, car directement lié à la façon dont une propriété émerge…)

Précision : Ce que j’appelle PRF est lié (on pourrait dire même que c’en EST un des aspect) au fait que certains principes mathématiques ont une trace dans d’autres, et  la reconnaissance par nous de « motifs », est tout autant due  au fait que ces motifs se déclinent à foison, qu’au fait que nous mêmes, en tant que « machine PRF », sommes enclins à identifier à la fois ces motifs et le fait qu’ils se déclinent.^^

 Ce principe s’applique à lui même en quelque sorte et est donc également lié au meta. C’est comme si on étendait la notion de fractal à un domaine plus vaste que la géométrie, les mêmes principes s’exportent d’échèle en échèle (géométriquement) mais aussi, par extension, de domaine en domaine, même si la notion de domaine est floue, il n’y a pas un domaine ouvert, et ce presque  quelque soit la définition qu’on donnera à « domaine » , qui échapperait à ce foisonnement potentiel. Ce dont je parle est si présent et si évident qu’il peut paraître brutal et inexact de tenter de l’exhiber/définir, et on ne peut pas le faire très précisément sans quelques restrictions liées à un cadre formel et terminologique, et ce faisant on ne ferait qu’approcher l’idée intuitive et vague de PRF. Je pense que ça serait très profitable de tenter de le faire, il faudra notamment traiter l’omniprésence, la permanence et le caractère contagieux du PRF (enfin d' »un PRF » satisfaisant, car encore une fois cette notion est vague…) et si on y parvient on sera peut-être en mesure de trouver des substantifiques raccourcis qui mènent à b) ou à c)

Pour résumer ce point :  il ne me semble quasiment raisonnable (et presque inéluctable) de penser qu’il existera un jour un automate de démonstration très performant qui sera dirigé consciemment ou non suivant les PRF afin d’exploiter au mieux ces mêmes PRF, quasiment de lui même,  mais la restriction GOFAI semble rendre inexploitable ces considérations….. Cependant le fantasme dont je parlais tout à l’heure serait de progresser si bien dans la direction d’une  définition/formalisation comme dans  l’établissement de mécanismes du PRF,  qu’on puisse en extraire des principes encadrés et approximatifs qui puissent être utiles et efficaces même en GOFAI. Mais cela semble aussi compliqué que de mettre de la foudre en boite^^

Une autre chose que je suggère à la fin de mon premier commentaire, et la conclusion de votre réponse me semble autoriser l’approfondissement de ce point,  est qu’il pourrait être profitable de restreindre le champ des problèmes de l’automate  à des problèmes d’algorithmiques ou des problèmes de nature discrète, voire la topologie produit sur 2^N, ou encore une catégorie de problèmes ad hoc… ceci a un lien avec le paragraphe précédent et bien que les considérations qui vont suivre semblent peu adaptées au  GOFAI, j’aimerai en toucher un mot, car elles m’ont donné une idée qui pourra être utilisée (je vais spoiler : il s’agit de définir une « distance » liée à la « complexité »)

 Je vais écrire ce que je me suis dit et que je n’aurais pas trop osé dire au grand jour de prime abord, de peur de passer pour un peu fou,… :

moi à moi-même : « Sur le long terme il est profitable de donner à l’automate un sujet d’étude proche de sa nature, car ce qui le constitue non seulement fait ce qu’il est, mais (par le PRF), aura de grande chance de se manifester de diverses et prolifiques manières, et si on encourage l’exploitation de ces manifestations, celles-ci seront d’autant plus fructueuses… laissons nous aller à la divagation d’imaginer ce que c’est que d’être un hardware, car en vertu de ce que je viens de dire, cela nous donnera peut-être des idées, ce petit exercice irréaliste sera un raccourcis pour dénicher le terrain d’investigation optimal, sujet d’étude de l’automate, celui qui entrera en résonnance avec le PRF et devrait gagner à être proche de sa constitution…une version parfaite et aboutie de cette automate aura certainement développé quelque chose d’équivalent à nos images mentales, en quelque sorte des  « images mentales artificielles » qu’il aurait acquises par d’innombrables va-et-vient de « lui-à-lui » (du général au particulier, etc.), ses images constitueraient une  sorte de  « sens » qui aurait émergé, et qui serait lié, à la fois à son domaine d’étude (sa fonction) et à sa constitution (sa « nature » algorithmique),  sens  d’autant plus efficace que sa nature et sa fonction seraient alignées….il me semble alors envisageable que ce  « sens », relatif à la notion de distance (homologue de notre distance euclidienne) , se développe naturellement chez l’automate en rapport avec la notion  complexité : ce qui nous semble « loin » est ce que nos sens ont du mal à percevoir, ainsi, ce qui semblerait loin à cet automate très abouti, serait  ce qui est difficile à résoudre, et ce que je sens, en « me mettant à sa place », c’est qu’il serait bien plus à l’aise avec la topologie de l’ensemble de Cantor qu’avec la topologie usuelle et qu’il utiliserait  la notion de « distance algorithmique »  avec la même aisance que nous utilisons la distance euclidienne »

Ceci n’est valable que si on a trouvé une technique pour que les outils d’évaluation de l’automate soient en grande partie fabriqués par lui, ce qui suppose un long apprentissage statistique doublé de méthodes intelligentes pour qu’il parvienne à puiser dans lui-même… on me dira que puiser dans lui-même ne signifie pas qu’il puisera dans le hardware, et l’équivalent chez lui de ce qui est pour nous « images mentales » serait lié à son domaine d’étude (fonction), beaucoup plus qu’à sa nature (sa constitution algorithmique, qu’on peut voir de façon abstraite ou pour simplifier qu’on peut ramener au hardware).Je pense pourtant que les PRF seraient beaucoup plus foisonnant et fructueux si fonction et nature peuvent entrer en résonnance, dire le contraire équivaudrait plus ou moins à dire qu’il n’y a aucun lien entre hardware et software, ce qui  est absurde puisque le software fonctionne 😀

 Ces phénomènes seraient le fruits de très longs et infinitésimaux va-et-vient aussi longs et infinitésimaux que ce qui a constitué notre espèce, ou plus localement notre apprentissage et notre intuition du monde physique. 

Donc, sans se limiter spécifiquement au GOFAI dans un premier temps, je vais réfléchir  à ce que je ferais si je voulais que l’automate révé ait cette aptitude au  « meta », constitutive d’une grande part, selon moi, de notre habileté mathématique. Ensuite je vais dresser de possibles directions à fouiller pour s’approcher de ces pistes en intégrant cette fois les contraintes  GOFAI.

De ce qu’on pourrait faire à ce qu’on pourra faire [titre de section provisoire car le pourra est aussi beaucoup un pourrait]

  Ainsi, si je voulais mettre sur pied l’automate (sans restriction GOFAI) j »encouragerais celui-ci à faire des liens (1), à constamment généraliser dans les bonnes directions (il jugera de « bonne » selon son « sens » (lié à la complexité) dont j’ai parlé tout à l’heure), je mettrais au point des techniques qui lui permettent de dérigidifier ses fondements (2), et l’encouragerai à lui-même trouver des techniques pertinentes et efficientes de dérigidification des fondements, plus généralement je souhaiterais qu’il fût  enclin à établir\appliquer une « théorie du lien » (peut-être proche de la théorie des catégories mais peu importe) ce qui serait, je pense,  d’autant plus fécond et fructueux que ça serait aussi l’objet de son étude!! Je lui fabriquerais donc un domaine d’étude initial ad hoc (3), pour optimiser les mécanismes dont j’ai parlé. Plus tard se dessinerait alors d’autres sens que « la complexité » qui lui sert à évaluer les distances, une sorte de complexité modulo les techniques acquises (4), comme nous avons plusieurs sens nous même… il développerait surement un « goût » pour la symétrie et la dualité (5), goût qu’on pourra encourager mais qu’il est probable si on s’y prend bien au début, qu’il les trouverait tout seul. 

Je pense que ces considérations (le pourrait) nous donne du moins une idée de direction (le pourra) pour GOFAI :

(1) (5) : developper une « link strategie »

(2) : Peut-être que les topos seraient  une inspiration, en tous cas j’ouvre mon esprit pour diverses idées en ce sens (pour l’instant je n’ai que de vagues pistes très floues, qui embrassent d’un vague regard un panel des possibles, allant  de l’espérance d’un miracle combinatoire à des considérations trop triviales pour être efficaces en elles-mêmes).

(3) (4) : pour autant, le domaine  qu’on inventerait (qui serait plutôt une redirection vers un point de vue ad hoc qu’une invention) n’est pas dénué d’intérêt. De plus on a rien à perdre (si l’on devait restreindre le domaine au moins pour une version d’un automate) à donner à résoudre à l’automate des problèmes orientés vers ce domaine ad hoc! Peut-être que cette étude nous donnerait des pistes pour b) ou c)… 

De plus, j’irai même jusqu’à dire qu’on a beaucoup à gagner du simple fait d’inclure dans M des problèmes d’un domaine nouveau, car cela nous aiderait à identifier plus facilement ce qui caractérise M – dont une des difficultés à le réaliser vient du fait qu’on en est proche… 

The link strategy

Quand je dois résoudre un problème, il arrive souvent que j’en trouve plusieurs énoncés équivalents. J’aime aussi trouver des conditions nécessaires et des conditions suffisantes. Si je cherche une preuve d’un énoncé que je sais vrai (parce que, par exemple, on me l’a dit)  j’aurai tendance à chercher des conditions suffisantes, mais la recherche de conditions nécessaires peut s’avérer très fructueuse même dans ce cas, en particulier pour éliminer des pistes, mais aussi pour trouver une condition suffisante plus forte, et de façon plus globale « s’approprier »  le problème. Je peux aussi faire des liens qui ne sont ni des conditions nécessaires ni des conditions suffisantes, ou bien fabriquer des situations où le problème vit sous une autre forme, parfois proche du problème et de son cadre, parfois moins, et il arrive souvent qu’après cette balade guidée par le plaisir de l’exploration, j’arrive à trouver le cadre (souvent plus général) dans lequel notre problème devient naturel. 

Il y a selon moi deux raisons à cela, ou plutôt deux angles de justification : l’un plus théorique et l’autre plus  pratique.

Je serai cependant très prudent pour la justification théorique, n’étant pas du tout spécialiste, et même franchement béotien.

Il m’a été confié de source sûre qu’il  existe un théorème de théorie de la démonstration dû à Christophe Chalons qui dit « en gros » que :

tout théorème est conséquence triviale d’une trivialité 

L’auteur lorsqu’il parle de son résultat, précise bien la double occurrence de « trivial » : non seulement c’est la conséquence d’une trivialité mais de plus, la déduction que l’on fait de cette trivialité est elle aussi triviale. Ce résultat, à l’instar de  son auteur (qui a aussi mis au point les « degrés ludiques » dont je dirai deux mots tout à l’heure) , n’est pas très connu, mais peut-être plus que je ne l’imagine…  …ou alors peut-être qu’une de ses expressions est connue de la plupart des théoriciens de la démonstration…

Si besoin,  je peux me documenter plus précisément à ce sujet et fournir (en tentant de le comprendre) un énoncé précis. Je vais ici me contenter d’exposer informellement ce qui m’a été dit tout aussi informellement, informellement mais néanmoins tout à fait sérieusement : 

« conséquence triviale » et « trivialité » ont  un sens formel précis, qui n’est PAS une interprétation vague et arrangeante  de la notion informelle de trivialité, mais bien précisément ce à quoi on s’attend (selon l’auteur mais aussi les autres logiciens qui m’en ont parlé).  Ce théorème n’est pas non plus une sorte de tautologie déguisée : je serais tenté de dire qu’il n’est pas  trivial (même si comme tout théorème c’est une conséquence triviale d’une trivialité hahaha)

La difficulté de trouver une telle preuve d’un quelconque énoncé  réside donc dans celle de  trouver DE QUELLE EVIDENCE c’est une conséquence.

Je m’excuse à nouveau pour le caractère informel de ces allégations, et je demanderai plus de détails aux logiciens que je connais et qui connaissent ce résultat si toutefois cela semblait nécessaire – peut-être que ça ne servirait à rien en pratique… 

Justement, la justification pratique (certes naïve et déconnectée d’une myriade d’autres facteurs, disons que c’est une tendance…)  est qu’en créant suffisamment  de liens (pertinents), en ouvrant des boites, en se baladant (« autour » du problème) on augmente nos chances de trouver sa « fully justified proof » (FJP) Que veut dire « pertinent » et « autour du problème »… cela fait partie des nombreuses question floues qu’il serait sans doute utile d’étudier… et je reviendrai à ça tout à l’heure, au moment d’aborder diverses stratégies (long terme)  et  tactiques (court terme) pour tenter de garantir une forme de « pertinence », en rapport avec celle qui nous guide lorsque nous explorons des pistes… d’ailleurs me vient une remarque : peut-être que nous n’évitons pas  les « silly options« … peut-être que notre goût (ou d’autres facteurs) nous font sélectionner des chemins plus intéressants que d’autres… cette approche « positive » est peut être équivalente à un rejet par défaut, mais je pointe ceci pour soumettre l’idée que l’automate, plutôt que d' »éliminer » des pistes, soit « naturellement », par des critères  à établir, porté à en explorer…

Par exemple, supposons, pour simplifier, qu’on connaisse le résultat à l’avance et qu’on cherche une démonstration par l’absurde (si on ne connaît pas le résultat, on fera ce qui suit dans les deux sens…)

En allant de conséquence en conséquences (et en en tirant les bonnes conséquences, si j’ose dire) on pourrait se dire qu’à un moment, on trouvera une contradiction, car  l’absurdité n’est pas viable si on la confronte avec suffisamment de cohérence. Comme ceci n’est qu’une direction floue et qu’il faudra préciser beaucoup de choses je ne ferai pas de remarque sur les inconvénients  possibles du raisonnement par l’absurde vs FJP, et j’insiste sur le fait que ceci est avant tout une métaphore vaguement heuristique pour faire comprendre le point de départ d’une stratégie. 

Entrons plus en détail dans les processus qui pourraient guider une « balade » qui caractérise les idées de la « link stratégy » que je viens d’essayer de dépeindre.

L’erreur, l’approximation fainéante

Les erreurs qu’on commet sont à mon avis une partie de la raison de ce qui nous fait apprécier « les fois où ça marche » . D’autre part, elles sont source d’inspiration. Parfois on cherche à démontrer quelque chose et, pour conserver une vue d’ensemble, on passe les étapes sans être certains qu’elles sont valides. En tous cas je le fais souvent et j’ai remarqué que d’autres le faisaient aussi. Il m’arrive souvent que mes « approximations fainéantes » soient en fait trop optimistes et parfois c’est irrattrapable… mais en général quelques modifications suffisent pour venir à bout de la démonstration. Si je m’étais bloqué et interdit de poursuivre, je n’aurais pas eu la puissance de calcul nécessaire. Je n’ai donc pas « éliminé » des pistes proches mais au contraire j’ai été directement vers une piste lointaine (en sautant de pistes proches incertaines en  piste proches incertaines et en ayant une vague vision du but (++)). Le mot « incertaine » garantit une faible exigence en calcul, c’est son avantage, peut-être qu’on peut s’inspirer de ces considérations. (++) :  Pour ce qui est de la vision vague du but (autre bien sûr, que le but trivial de démontrer l’énoncé) je pense qu’elle pourrait se forger efficacement avec la link stratégie. Pour mieux viser ce but, l’idée serait (pour la machine), de « grossir la cible » par des conditions suffisantes proches de l’énoncé à prouver, mais pas exclusivement des conditions suffisantes, comme j’en ai parlé dans le paragraphe « link strategy ».

Un outil qui pourrait s’avérer utile serait la notion de  degré ludique développée par Chalons (j’ai dit plus haut que j’en reparlerai…) Cette notion est une extension des degré de Tuckey et informellement elle permet de donner « le degré de magie qu’il faut pour qu’une assertion soit vraie » (si l’assertion est vraie, son degré ludique est  trivial). Comme pour le reste je n’ai qu’une vision vague de cette théorie. Elle est peu connue et assez récente, mais certains mathématiciens de premier plan la considèrent comme remarquable. Comme pour beaucoup de choses que j’ai évoquées en tant que béotien, je fournirai des sources précises sur demande, ainsi qu’un travail vers une forme d’acquisition de ces techniques, si nécessaire…

Images mentales

Ce qui différencie le plus le GOFAI du ML me semble être lié à ce qui a été mentionné dans beaucoup de commentaire comme des « images mentales ». Il me semble qu’on a pas d’autre choix que de livrer à la machine, pour chaque domaine, un petit ensemble  « d’images mentales » ainsi (et surtout) que la façon de s’en servir.

Si je ne me trompe pas, il me semble que  c’est en quelque sorte,  un des buts du projet, et que vous faites le pari que nous-même, dans chaque domaine, n’utilisons qu’un petit nombre de ces « images mentales » (je simplifie peut-être un peu trop…) 

Après les avoir « recensées » (je trouve à ce propos  la tentative de  Bruce Smith dans un de ces commentaires, relativement à la géométrie plane, tout à fait complète et pertinente), on devra essayer de les « appliquer »  – peut-être que couplé à de la link stratégie, même une link strategy rudimentaire, on aurait déjà des résultats intéressants…:  l’automate pourrait « jeter », ça et là, des « images mentales artificielles », dans le but qu’elles « adhèrent » à des énoncés « voisins » de l’énoncé à prouver…

Il faudrait alors réfléchir techniquement à comment cet « adhérence/adhésion(+) » s’effectuerait. Je pense que ça devra se faire au cas par cas.

(+) [adhésion est le fait d’être en accord, d’accepter, adhérence est le fait de « coller », les deux racines du verbe « adhérer » conviennent, d’ailleurs  « it fits » se traduit familièrement en français par « ça colle » hahaha]

Je vais faire des commentaires (en anglais) plus précis directement à l’endroit où Bruce Smith dresse sa remarquable liste d’images mentales, en proposant de coupler ces réflexions (et peut-être celles du présent commentaire)  avec un système abstrait de droite/points vérifiant certains axiomes (notamment axiomatique de Bachmann)

Un commentaire sur “à propos de l’automate [trop long pour un commentaire]

Votre commentaire

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l’aide de votre compte WordPress.com. Déconnexion /  Changer )

Image Twitter

Vous commentez à l’aide de votre compte Twitter. Déconnexion /  Changer )

Photo Facebook

Vous commentez à l’aide de votre compte Facebook. Déconnexion /  Changer )

Connexion à %s