Les ordinateurs sont-ils prêts à résoudre ce problème mathématique notoirement difficile à manier ?

Mme Tech | SuperRembo via codingtrain

L'informaticien Marijn Heule est toujours à la recherche d'un bon défi mathématique. Professeur agrégé à l'Université Carnegie Mellon, Heule a une réputation impressionnante pour la résolution de problèmes mathématiques insolubles avec des outils informatiques. Son résultat de 2016 avec le problème des triplets booléens de Pythagore était une énorme preuve qui faisait la une des journaux : La preuve mathématique de deux cents téraoctets est la plus grande jamais réalisée . Maintenant, il déploie une approche automatisée pour attaquer la conjecture d'une simplicité séduisante de Collatz.

Proposé pour la première fois (selon certains récits) dans les années 1930 par le mathématicien allemand Lothar Collatz, ce problème de théorie des nombres fournit une recette, ou un algorithme, pour générer un nombre séquence : Commencez par n'importe quel entier positif. Si le nombre est pair, divisez par deux. Si le nombre est impair, multipliez par trois et ajoutez un. Et puis faites la même chose, encore et encore. La conjecture affirme que la séquence se terminera toujours à 1 (puis passera continuellement par 4, 2, 1).

Le nombre 5, par exemple, ne génère que six termes :

5, 16, 8, 4, 2, 1

Le nombre 27 parcourt 111 termes, oscillant de haut en bas - à son apogée atteignant 9 232 - avant d'atterrir finalement à 1.

Le nombre 40 génère une autre brève séquence :

40, 20, 10, 5, 16, 8, 4, 2, 1

À ce jour, la conjecture a été vérifiée par ordinateur pour toutes les valeurs de départ jusqu'à près de 300 milliards de milliards et chaque nombre atteint finalement 1.

La plupart des chercheurs croient que la conjecture est vraie. Il a attiré des multitudes de mathématiciens et de non-mathématiciens, mais personne n'a produit de preuve. Au début des années 1980, le mathématicien hongrois Paul Erdős déclarait : Les mathématiques ne sont pas encore prêtes pour de tels problèmes.

Ce que nous voulons savoir, c'est si les humains ou les ordinateurs sont meilleurs pour résoudre de tels problèmes.

Marijn Heule

Et il a probablement raison, dit Heule. Pour Heule, l'attrait de Collatz n'est pas tant la perspective d'une percée que l'avancement des techniques de raisonnement automatisé. Après l'avoir bricolé pendant cinq ans, Heule et ses collaborateurs, Scott Aaronson et Emre Yolcu, ont récemment publié un papier sur le serveur de préimpression arXiv. Bien que nous ne réussissions pas à prouver la conjecture de Collatz, écrivent-ils, nous croyons que les idées ici représentent une nouvelle approche intéressante.

C'est un noble échec, déclare Aaronson, informaticien à l'Université du Texas à Austin. Un échec parce qu'ils n'ont pas prouvé la conjecture. Nobles parce qu'ils ont fait des progrès dans un autre sens : Heule y voit un point de départ pour déterminer si les humains ou les ordinateurs sont meilleurs pour prouver de tels problèmes.

Traduire les mathématiques en calcul

Pour de nombreux problèmes mathématiques, les ordinateurs sont sans espoir, car ils n'ont pas accès à la vaste œuvre mathématique accumulée à travers l'histoire. Mais parfois, les ordinateurs excellent là où les humains sont sans espoir. Dites à un ordinateur à quoi ressemble une solution - donnez-lui une cible et un espace de recherche bien défini - et ensuite, avec une force brute, l'ordinateur pourrait la trouver. Bien qu'il s'agisse de débat si les résultats de calcul équivalent à des ajouts significatifs au canon mathématique. L'opinion traditionnelle est que seules la créativité et l'intuition humaines, via des concepts et des idées, étendent la portée des mathématiques, tandis que les progrès via l'informatique sont souvent rejetés comme de l'ingénierie.

Histoire connexe

Cet algorithme peut dire quelles séquences de nombres un humain trouvera intéressant Le résultat laisse entendre que les machines pourraient un jour être entraînées à repérer l'élégance et la beauté mathématiques.

Dans un sens, l'ordinateur et la conjecture de Collatz correspondent parfaitement. D'une part, comme le note Jeremy Avigad, logicien et professeur de philosophie à Carnegie Mellon, la notion d'algorithme itératif est à la base de l'informatique - et les séquences de Collatz sont un exemple d'algorithme itératif, procédant étape par étape selon à une règle déterministe. De même, montrer qu'un processus se termine est un problème courant en informatique. Les informaticiens veulent généralement savoir que leurs algorithmes se terminent, c'est-à-dire qu'ils renvoient toujours une réponse, explique Avigad. Heule et ses collaborateurs tirent parti de cette technologie pour s'attaquer à la conjecture de Collatz, qui n'est en réalité qu'un problème de terminaison.

La beauté de cette méthode automatisée est que vous pouvez allumer l'ordinateur et attendre.

Jeffrey Lagarias

L'expertise de Heule est avec un outil de calcul appelé un solveur SAT - ou un solveur de satisfiabilité, un programme informatique qui détermine s'il existe une solution pour une formule ou un problème compte tenu d'un ensemble de contraintes. Bien que crucial, dans le cas d'un défi mathématique, un solveur SAT a d'abord besoin que le problème soit traduit, ou représenté, dans des termes que l'ordinateur comprend. Et comme Yolcu, doctorant chez Heule, le dit : La représentation compte beaucoup.

Un longshot, mais ça vaut le coup d'essayer

Lorsque Heule a mentionné pour la première fois s'attaquer à Collatz avec un solveur SAT, Aaronson a pensé: Il n'y a aucun moyen que cela fonctionne. Mais il était facilement convaincu que cela valait la peine d'essayer, car Heule voyait des moyens subtils de transformer ce vieux problème qui pourrait le rendre malléable. Il avait remarqué qu'une communauté d'informaticiens utilisait des solveurs SAT pour trouver avec succès des preuves de terminaison pour une représentation abstraite du calcul appelée système de réécriture. C'était long, mais il suggéra à Aaronson que la transformation de la conjecture de Collatz en un système de réécriture pourrait permettre d'obtenir une preuve de terminaison pour Collatz (Aaronson avait auparavant aidé à transformer l'hypothèse de Riemann en un système informatique, en l'encodant dans un petit Turing machine). Ce soir-là, Aaronson a conçu le système. C'était comme un devoir, un exercice amusant, dit-il.

'Dans un sens très littéral, je combattais un Terminator - au moins un démonstrateur de théorème de terminaison.'

Scott Aaronson

Le système d'Aaronson a capturé le problème de Collatz avec 11 règles. Si les chercheurs pouvaient obtenir une preuve de terminaison pour ce système analogue, en appliquant ces 11 règles dans n'importe quel ordre, cela prouverait que la conjecture de Collatz est vraie.

Heule a essayé avec des outils de pointe pour prouver la fin des systèmes de réécriture, ce qui n'a pas fonctionné - c'était décevant sinon si surprenant. Ces outils sont optimisés pour les problèmes qui peuvent être résolus en une minute, alors que toute approche pour résoudre Collatz nécessite probablement des jours, voire des années de calcul, explique Heule. Cela les a motivés à affiner leur approche et à mettre en œuvre leurs propres outils pour transformer le problème de réécriture en un problème SAT.

Une représentation du système de réécriture à 11 règles pour la conjecture de Collatz.

MARINE HEULE

Aaronson a pensé qu'il serait beaucoup plus facile de résoudre le système sans l'une des 11 règles, laissant un système de type Collatz, un test décisif pour l'objectif plus large. Il a lancé un défi humain contre ordinateur : le premier à résoudre tous les sous-systèmes avec 10 règles gagne. Aaronson a essayé à la main. Heule essayé par le solveur SAT : il a encodé le système comme un problème de satisfiabilité - avec encore une autre couche de représentation intelligente, traduisant le système dans le jargon informatique des variables qui peuvent être des 0 et des 1 - puis a laissé son solveur SAT s'exécuter sur les cœurs , à la recherche de preuves de résiliation.

Le système suit ici la séquence de Collatz pour la valeur de départ 27—27 est en haut à gauche de la cascade diagonale, 1 est en bas à droite. Il y a 71 étapes, au lieu de 111, puisque les chercheurs ont utilisé une version différente mais équivalente de l'algorithme de Collatz : si le nombre est pair alors divisez par 2 ; sinon multipliez par 3, ajoutez 1, puis divisez le résultat par 2.

MARINE HEULE

Ils ont tous deux réussi à prouver que le système se termine avec les différents ensembles de 10 règles. Parfois, c'était une entreprise triviale, tant pour l'humain que pour le programme. L'approche automatisée de Heule a pris au plus 24 heures. L'approche d'Aaronson a nécessité un effort intellectuel important, prenant quelques heures ou même une journée - un ensemble de 10 règles qu'il n'a jamais réussi à prouver, bien qu'il croit fermement qu'il pourrait l'avoir, avec plus d'efforts. Dans un sens très littéral, je combattais un Terminator, dit Aaronson – au moins un démonstrateur de théorème de terminaison.

Yolcu a depuis affiné le solveur SAT, calibrant l'outil pour mieux s'adapter à la nature du problème de Collatz. Ces astuces ont fait toute la différence en accélérant les preuves de terminaison pour les sous-systèmes à 10 règles et en réduisant les durées d'exécution à quelques secondes.

La principale question qui demeure, dit Aaronson, est la suivante : qu'en est-il de l'ensemble complet de 11 ? Vous essayez d'exécuter le système sur l'ensemble complet et il fonctionne pour toujours, ce qui ne devrait peut-être pas nous choquer, car c'est le problème de Collatz.

Selon Heule, la plupart des recherches sur le raisonnement automatisé ferment les yeux sur les problèmes qui nécessitent beaucoup de calculs. Mais sur la base de ses percées précédentes, il pense que ces problèmes peuvent être résolus. D'autres ont Collatz transformé as a système de réécriture , mais c'est la stratégie consistant à utiliser un solveur SAT affiné à grande échelle avec une formidable puissance de calcul qui pourrait gagner du terrain vers une preuve.

Jusqu'à présent, Heule a mené l'enquête Collatz en utilisant environ 5 000 cœurs (les unités de traitement alimentant les ordinateurs ; les ordinateurs grand public ont quatre ou huit cœurs). En tant qu'Amazon Scholar, il reçoit une invitation ouverte d'Amazon Web Services pour accéder à des ressources pratiquement illimitées, jusqu'à un million de cœurs. Mais il hésite à en utiliser beaucoup plus.

Je veux une indication qu'il s'agit d'une tentative réaliste, dit-il. Sinon, Heule pense qu'il gaspillerait des ressources et de la confiance. Je n'ai pas besoin d'une confiance à 100 %, mais j'aimerais vraiment avoir des preuves qu'il y a une chance raisonnable que cela réussisse.

Supercharger une transformation

La beauté de cette méthode automatisée est que vous pouvez allumer l'ordinateur et attendre, explique le mathématicien Jeffrey Lagarias, de l'Université du Michigan. Il a joué avec Collatz pendant une cinquantaine d'années et est devenu le gardien du savoir, compilant des bibliographies annotées et éditant un livre sur le sujet, Le défi ultime. Pour Lagarias, l'approche automatisée évoque une papier 2013 par le mathématicien de Princeton John Horton Conway, qui pensait que le problème de Collatz pourrait faire partie d'une classe insaisissable de problèmes qui sont vrais et indécidables - mais à la fois non indécidables de manière prouvée. Comme Conway l'a noté : … il se pourrait même que l'affirmation selon laquelle ils ne sont pas prouvables ne soit pas elle-même prouvable, et ainsi de suite.

Si Conway a raison, dit Lagarias, il n'y aura aucune preuve, automatisée ou non, et nous ne connaîtrons jamais la réponse.

L'humain qui s'en rapproche le plus est sans doute le mathématicien Terence Tao, de l'Université de Californie à Los Angeles. En 2019, Tao a prouvé que la conjecture de Collatz est presque vrai pour presque tous les nombres (s'appuie presque sur deux définitions techniques différentes, néanmoins conformes au sens anglais ordinaire).

Tao pense qu'une preuve humaine de la conjecture serait mathématiquement plus significative - atteindre le Pourquoi de celui-ci— qu'une preuve informatique. Mais le fait qu'un problème majeur non résolu revienne à un démonstrateur automatisé pourrait accélérer une transformation révolutionnaire dans la façon dont les mathématiciens utilisent l'assistance informatique dans leur travail, dit-il. Avec un problème aussi insoluble que celui-ci, nous prendrons toutes les informations que nous pourrons obtenir.

Ce que Heule et ses collaborateurs recherchent en réalité, cependant, c'est un scénario tel que - en utilisant cette approche, avec ce problème - l'ordinateur réussisse là où l'humain échoue, ou vice versa. À ce stade, nous ne savons pas si ces techniques sont beaucoup plus puissantes que ce que les humains peuvent faire à la main ou non, ou si les humains peuvent faire des choses que l'ordinateur ne peut pas faire, dit Heule. Ce que nous voulons savoir, c'est si les humains ou les ordinateurs sont meilleurs pour résoudre de tels problèmes.

À cette fin, voyons qui résout la conjecture de Collatz en premier.

cacher