, стверджує, що розробляє прототип нової мови програмування.){kind=link}
Le calcul haute performance est nécessaire pour résoudre de plus en plus de tâches - telles que le traitement d'images ou diverses applications d'apprentissage en profondeur sur des réseaux de neurones - où vous devez traiter d'énormes quantités de données, et le faire assez rapidement, sinon cela peut prendre une quantité incroyable de temps. temps. Il est largement admis que lors de l'exécution de telles opérations, un compromis entre rapidité et fiabilité est inévitable. Selon cette réflexion, si la vitesse est une priorité, la fiabilité risque d'en souffrir et vice versa.
Cependant, un groupe de chercheurs basé principalement au Massachusetts Institute of Technology (MIT) conteste cette notion, affirmant que vous pouvez réellement tout avoir. Selon Amanda Liu, étudiante de deuxième année au Laboratoire d'informatique et d'intelligence artificielle (CSAIL) du MIT, avec un nouveau langage de programmation qu'ils ont écrit spécifiquement pour le calcul haute performance, "la vitesse et l'exactitude ne doivent pas rivaliser. Au contraire, ils peuvent aller de pair, côte à côte, dans les programmes que nous écrivons." Liu et son équipe ont parlé du potentiel de leur nouveau langage A Tensor (ATL) le mois dernier lors de la conférence Principles of Programming Languages à Philadelphie.
"Tout dans notre langue", dit Liu, "vise à obtenir soit un nombre unique, soit un tenseur". Les tenseurs, à leur tour, sont une généralisation des vecteurs et des matrices. Alors que les vecteurs sont des objets unidimensionnels (souvent représentés par des flèches individuelles) et que les matrices sont des tableaux de nombres bidimensionnels familiers, les tenseurs sont des tableaux à n dimensions qui peuvent prendre la forme d'un tableau 3 × 3 × 3, par exemple, ou même dimension supérieure (ou inférieure).
L'essence d'un algorithme ou d'un programme informatique est d'initier un certain calcul. Mais il peut y avoir de nombreuses façons différentes d'écrire ce programme - "une variété surprenante d'implémentations de code différentes", comme l'écrivent Liu et ses co-auteurs dans leur article - dont certaines sont nettement plus rapides que d'autres. La principale raison d'être de l'ATL, explique-t-elle, est la suivante : "Étant donné que le calcul haute performance est si gourmand en ressources, vous voulez pouvoir modifier ou réécrire les programmes sous une forme optimale pour accélérer les choses. Souvent, vous commencez avec le programme le plus facile à écrire, mais ce n'est peut-être pas le moyen le plus rapide de l'exécuter, vous devez donc encore faire d'autres ajustements."
Le nouveau langage de commande est basé sur le langage Coq existant, qui inclut un assistant de preuve. L'assistant de preuve, à son tour, a la capacité de prouver mathématiquement ses déclarations avec précision. Coq a une autre propriété qui l'a rendu attractif pour le groupe MIT : les programmes écrits dans ce langage, ou une adaptation de celui-ci, se terminent toujours et ne peuvent pas tourner indéfiniment dans des boucles infinies.
C'est maintenant le premier et jusqu'à présent le seul langage tenseur avec des optimisations formellement vérifiées. L'équipe du MIT prévient cependant qu'ATL n'est encore qu'un prototype - bien que prometteur - qui a été testé sur un certain nombre de petits programmes.
Lisez aussi: