Oui il y un lien avec le programme de Hilbert (et c'était bien à cela que voulait répondre entre autre Turing), mais ce que je voulais dire est plus simple.
Ton commentaire auquel j'ai répondu en premier contenait ce paragraphe :
Exemple limite : un raisonnement mathématique. Prend un ensemble de démonstration mathématiques, à classer comme "correctes" ou "incorrecte", entraine le donc à discriminer le mathématiquement correct du mathématiquement incorrect. Les lois de la logiques ont des règles du jeu. Un réseau de neurone "séquentiel" peut en principe apprendre les différentes règles pertinentes, et classer leur application correcte ou pas, voire pointer directement les applications incorrectes.
Dans son article originaire, Turing, où il développe sa notion de machine à calculer, traite justement de cette question mais sans recourir à un apprentissage automatique. Relativement à cette question, on se retrouve dans le cas que Liorel, dans sa dépêche, décrit en ces termes :
En définitive, on peut voir le réseau de neurones comme un outil qui résout approximativement un problème mal posé. S’il existe une solution formelle, et qu’on sait la coder en un temps acceptable, il faut le faire. Sinon, le réseau de neurones fera un taf acceptable.
Et justement, Turing, dans son article, donne une telle solution formelle. Il a montré qu'il existe une machine à calculer qui prend en entrée un argumentaire P et un théorème T et qui vérifie si P est bien une preuve de T et cela en un temps fini. Cette machine prend n'importe quelle preuves et n'importe quel théorème et s'arrête toujours pour répondre à la question. Une telle machine, ou un tel programme, est ce que l'on appelle un type checker.
Mais continuant son raisonnement, pour répondre au problème de Hilbert, il construit idéalement un autre machine. Celle ci ne va pas seulement vérifier qu'une preuve est correcte mais elle va en chercher une. En entrée, elle ne prend plus une preuve et un théorème mais seulement un théorème et elle cherche à savoir si on peut le prouver ou le réfuter. Pour la décrire, il se sert de la machine précédente (le type checker), puis constate que tous les argumentaires possibles sont récursivement énumérables : il a une seconde machine qui va alimenter la première avec toutes les preuves possibles. En gros il fait de la composition de fonctions pour faire du brut forcing. Puis, il montre, finalement, que pour certaines entrées sa technique de brut force mouline sans fin : c'est le problème de l'arrêt ou l'existence d'énoncés indécidables.
Chercher un preuve pour un théorème donné, c'est cela que font des logiciels LLM comme copilot. Mais il ne peuvent pas simuler bien mieux qu'un programmeur junior. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Pourquoi dire IA si on ne parle que des réseaux de neurones ?
Posté par kantien . En réponse à la dépêche Une intelligence artificielle libre est-elle possible ?. Évalué à 2.
Oui il y un lien avec le programme de Hilbert (et c'était bien à cela que voulait répondre entre autre Turing), mais ce que je voulais dire est plus simple.
Ton commentaire auquel j'ai répondu en premier contenait ce paragraphe :
Dans son article originaire, Turing, où il développe sa notion de machine à calculer, traite justement de cette question mais sans recourir à un apprentissage automatique. Relativement à cette question, on se retrouve dans le cas que Liorel, dans sa dépêche, décrit en ces termes :
Et justement, Turing, dans son article, donne une telle solution formelle. Il a montré qu'il existe une machine à calculer qui prend en entrée un argumentaire
Pet un théorèmeTet qui vérifie siPest bien une preuve deTet cela en un temps fini. Cette machine prend n'importe quelle preuves et n'importe quel théorème et s'arrête toujours pour répondre à la question. Une telle machine, ou un tel programme, est ce que l'on appelle un type checker.Mais continuant son raisonnement, pour répondre au problème de Hilbert, il construit idéalement un autre machine. Celle ci ne va pas seulement vérifier qu'une preuve est correcte mais elle va en chercher une. En entrée, elle ne prend plus une preuve et un théorème mais seulement un théorème et elle cherche à savoir si on peut le prouver ou le réfuter. Pour la décrire, il se sert de la machine précédente (le type checker), puis constate que tous les argumentaires possibles sont récursivement énumérables : il a une seconde machine qui va alimenter la première avec toutes les preuves possibles. En gros il fait de la composition de fonctions pour faire du brut forcing. Puis, il montre, finalement, que pour certaines entrées sa technique de brut force mouline sans fin : c'est le problème de l'arrêt ou l'existence d'énoncés indécidables.
Chercher un preuve pour un théorème donné, c'est cela que font des logiciels LLM comme copilot. Mais il ne peuvent pas simuler bien mieux qu'un programmeur junior. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.