Algorithmes puissants qui sont tout simplement trop difficiles à mettre en œuvre - comment être sûr qu'ils ont raison?

9

Je me réfère à la question ici: des algorithmes puissants trop complexes à mettre en œuvre .

Si un algorithme est puissant, mais trop complexe à implémenter, comment pouvez-vous être sûr que l'algorithme est correct? Sans implémentation, vous ne pourrez pas tester l'algorithme dans un scénario réel, et un algorithme aussi complexe peut contenir des bogues, ce qui peut invalider l'algorithme.

Voilà ce que je ne comprends pas; si vous avez les techniques pour prouver l'exactitude d'un algorithme, alors vous auriez déjà l'algorithme pour l'implémenter, n'est-ce pas? Ou bien comment pouvons-nous être sûrs que la technique de vérification est correcte?

Je suis désolé si j'ai l'air élémentaire!

Mise à jour de Kaveh (reproduite ici car l'argument est meilleur!):

Si vous pouvez prouver formellement l'exactitude d'un algorithme dans un système formel comme Coq, vous pouvez également extraire l'algorithme (car vous avez essentiellement implémenté l'algorithme), mais le fait clé est que pour la plupart des algorithmes, nous ne donnons pas de preuves formelles de l'exactitude de l'algorithme, nous utilisons des preuves informelles d'exactitude. Les preuves peuvent être fausses, ce qui arrive de temps en temps, et même une preuve formelle de correction ne nous garantira pas absolument que l'algorithme est correct.

ds.algorithms implementation Graviton
la source
6
C'est pourquoi nous avons des techniques pour prouver l' exactitude des algorithmes, même si l'implémentation (correcte) sur une vraie machine est difficile.
Raphael
9
Je suis d'accord avec Raphael. Il semble que la question repose sur l'hypothèse que l'exactitude d'un algorithme est généralement prouvée par sa mise en œuvre, mais ce n'est pas le cas. Prouver la justesse d'un algorithme et implémenter un algorithme sont des choses complètement différentes, et une chose n'implique pas l'autre dans les deux sens.
Tsuyoshi Ito du
8
Algorithmes simples avec preuves de correction complexes - comment savez-vous qu'ils ont raison? Ce n'est pas parce qu'un algorithme fonctionne sur des exemples de test qu'il fonctionne sur toutes les entrées.
Peter Shor
2
Je suis d'accord avec la plupart des commentaires, mais je pense qu'ils manquent un point clé. Si vous pouvez prouver formellement l'exactitude d'un algorithme dans un système formel comme Coq, vous pouvez également extraire l'algorithme (car vous avez essentiellement implémenté l'algorithme), mais le fait clé est que pour la plupart des algorithmes, nous ne donnons pas de preuves formelles de l'exactitude de l'algorithme, nous utilisons des preuves de correction informelles . Les preuves peuvent être fausses, cela arrive de temps en temps, et même une preuve formelle de correction ne nous assurera pas absolument que l'algorithme est correct.
Kaveh
5
"Méfiez-vous des bogues dans le code ci-dessus; je l'ai seulement prouvé correct, pas essayé." ~ Donald Knuth
Lev Reyzin

Réponses:

11

Il y a plusieurs années, il y a eu un débat (assez dur) sur un sujet similaire à celui-ci. Tout a commencé lorsque plusieurs preuves complexes se sont révélées incorrectes, et certains chercheurs ont commencé à émettre des doutes sur la nature même des preuves (enfin, j'aurais dû dire "cryptographie prouvable", mais pour des raisons générales, je ne l'ai pas fait) . Les deux côtés de la controverse ont accusé l'autre de mal comprendre les concepts. Voici un lien pour plus d'informations .

Les preuves sont nos outils (mathématiques) pour prouver que les théorèmes / algorithmes sont corrects, mais quand ils sont devenus trop complexes, nous pouvons glisser et prouver que les choses fausses sont correctes. La récente épreuve d'une centaine de pages sur P ≠ NP en est un excellent exemple. Cependant, cela n'exclut pas la nature même des preuves: il n'y a rien de mal avec elles.

Un dernier point: je pense que l'étude de la philosophie des sciences nous donnera plus de détails à ce sujet. (Sous le lien donné, voir la puce " Comment savoir si une preuve mathématique est correcte? ")

MS Dousti
la source