Discussion :

[alex_pi]

Prouver certaines choses, oui, comme des programmes CRITIQUES, mais prouver n'importe quoi, non.

Pour ça je suis raisonnablement d'accord avec toi, de même que je pense que chercher la performance "à tout prix" est absurde pour la majorité des application.

Mais je voudrais quand même tempérer ton propos. Je ne sais plus où et quand j'ai lu ou entendu ça, mais l'informatique est une industrie completement à part. Si tu achètes un mixeur, et que quand tu appuies sur un bouton, le mixeur explose, tu retournes au magasin, furax, et tu te fais rembourser. Quand tu achetes un logiciel, si quand tu cliques sur un bouton, il plante, tu cherches sur internet comment te passer de ce bouton. Les exigences de qualités sont absolument ridicules. Et sans pousser jusqu'à une preuve formelle sur le comportement du programme, une amélioration de la qualité générale des programmes serait plus que la bienvenue.

Ce que je déplore, c'est que certaines personnes n'aient pas conscience que l'informatique est une science et un domaine à part entière.

Alors là par contre, je ne vois absolument pas le rapport. Est ce que tu vas aller voir un physicien quantique et lui dire "annnnnnnh, mais t'as pas compris que la mécaQ est une science à part entière, pourquoi tu parles de tenseurs, d'espace de Hilbert et de base orthonormée ??". En quoi la formalisation de l'informatique par les mathématiques la rabaisserait ? Bien au contraire, c'est ce qui perment de la promouvoir au rang de science. C'est sans doute ce qui manquait avant, et qui fait que Knuth a appelé son ouvrage "The art of computer programming" et non science.

Et enfin, tu dis que beaucoup de gens s'en moque éperduement, mais c'est souvent parce qu'ils ne savent pas qu'autre chose existe, et c'est aussi par habitude. Si les gens en IA codent en Lisp, ce n'est pas parce que c'est mieux qu'un autre langage, c'est parce que "c'est comme ça". Si les numériciens s'en moque de la validité de leurs programmes, c'est sans doute parce qu'ils codent dans des langages où montrer la moindre propriété d'un programme est une migraine garantie. Disons qu'il me semble étrange de dire "ça ne sert à rien de créer quelque chose, la preuve, personne ne s'en sert". Autant abandonner la notion de recherche.

[Garulfo]

[...] (En système B, on parle d'obligation de preuve)[...]

Petites remarques sur le B.

Concernant les obligations de preuve, on peut cependant « esquiver » le problème en B. Il existe des moyens d'écrire des axiomes.

Matra a été très content de son investissement dans le B puisque le nombre de retour atelier sur la partie écrite en B frisait le 0 atelier. Des projets subséquents ont permis de rendre le travail de Meteor encore plus rentable (réutilisation, raffinement automatique etc.).

Humm je m'en tiendrais là dans mes avis sur le B

[DrTopos]

Concernant les obligations de preuve, on peut cependant « esquiver » le problème en B. Il existe des moyens d'écrire des axiomes.

Il me semble que remplacer un théorème par un axiome est équivalent à dire qu'on renonce à prouver. Toutefois, je conçois qu'il soit utile (et même indispensable) d'introduire des axiomes pour codifier des propriétés indémontrables du matériel lui-même (ou par exemple du temps). C'est certainement ce qui a dû être fait. Mais dans ce cas, ces axiomes ont dû être soigneusement vérifiés par des spécialistes.

J'ai lu quelque part, qu'après que les systèmes automatiques de recherche de preuve du B aient terminé de prouver ce qu'ils pouvaient prouver sans intervention humaine, il restait encore quelques 6000 obligations de preuves à finaliser pour Météor. Elles ont toutes été traités par des moyens interactifs. Il est probable que pour beaucoup d'entre elles, il y avait peu de choses à faire. Il n'empèche que cela représente effectivement un investissement. Il a été jugé rentable par la RATP.

[Garulfo]

Il me semble que remplacer un théorème par un axiome est équivalent à dire qu'on renonce à prouver.

Effectivement.

J'ai lu quelque part, qu'après que les systèmes automatiques de recherche de preuve du B aient terminé de prouver ce qu'ils pouvaient prouver sans intervention humaine, il restait encore quelques 6000 obligations de preuves à finaliser pour Météor. Elles ont toutes été traités par des moyens interactifs. Il est probable que pour beaucoup d'entre elles, il y avait peu de choses à faire. Il n'empèche que cela représente effectivement un investissement. Il a été jugé rentable par la RATP.

Je ne connais pas le chiffre exact. Mais c'était parfois très chiant à prouver oui ^_^ Certes c'est formateur de se rendre compte qu'une évidence humaine ne l'est pas pour un ordinateur, mais c'était long. Attention cependant, Matra n'a jamais utilisé l'option que je citais ci-dessus. Toutes les obligations de preuves ont bien été déchargées à l'aide de l'Atelier B. Mais ce qui est sûr c'est qu'avec leur système de raffinement automatique, ils approchent le 98% je crois. Ce qui fait qu'ils n'ont pas eu besoin de mon travail sur la génération de preuve automatique -_- Menfinbon.

[DrTopos]

c'est formateur de se rendre compte qu'une évidence humaine ne l'est pas pour un ordinateur

C'est dû à quoi à ton avis ? Un manque de moyens formels d'investigation, ou l'absence de modèles pouvant jouer le rôle de ce qu'on appelle l'intuition ? (Ou autre chose ?)

Par ailleurs, réciproquement, il y a des choses qu'un prouveur automatique trouve facilement et qui sont difficiles pour nous.

Ce qui fait qu'ils n'ont pas eu besoin de mon travail sur la génération de preuve automatique -_- Menfinbon.

Petit cachotier. Si tu nous parlais un peu de cela ?

[alex_pi]

c'est formateur de se rendre compte qu'une évidence humaine ne l'est pas pour un ordinateur

C'est dû à quoi à ton avis ? Un manque de moyens formels d'investigation, ou l'absence de modèles pouvant jouer le rôle de ce qu'on appelle l'intuition ? (Ou autre chose ?)

Etant un adepte des différentes thèses de Church (qui disent, grosso-modo qu'aucun système physique ne peut calculer plus que ce qui est "calculable", avec comme définition de "calculable" celle donnée par le lambda-calcul ou les approches équivalentes (comme les machines de Turing), et qui dit aussi qu'un être humain, en tant que partie de la nature, est un système physique), je ne pense pas qu'un humain soit capable, dans l'absolu, de démontrer plus qu'un ordinateur. En revanche, il est assez évident que dans l'état actuel des connaissances et des implémentation des prouveurs automatiques, nous sommes capables de faire bien mieux qu'eux.

Pourquoi ? Il me semble que la différence fondamentale est dans l'approche. Les prouveurs automatiques sont rigoureux à chaque étape du raisonnement. Ils procèdent (plus ou moins) par une exploration rigoureuse de l'arbre des dérivations possibles (avec bien sûr tout un paquet d'euristique et de méthodes pour ne pas aller s'enfoncer n'importe où). Alors que l'être humain a une capacité, indispensable pour les preuves, au manque momentané de rigueur qui lui permet de se dire "si je suis capable de montrer ces résultats intermédiaires dont je ne connais pas la véracité, je serais sans doute capable de démontrer le résultat final. Attaquons nous à ces résultats intermédiaires". Même si les nombreux théorème de suppression des coupures montrent que ce n'est généralement pas indispensable, c'est néanmoins un gros plus et un moyen de gagner beaucoup de temps. Il n'y a qu'à voir la taille d'une preuve après suppression des coupures !

De plus, le cerveau humain, réseau de neuronne s'il en est, a des capacités de classification considérables. Nous sommes capables de "lier" des théorèmes à démontrer avec d'autres, déjà démontrer, et d'éliminer ceux qui n'ont, a priori, rien à voir. Dans certain cas, c'est une erreur, ce qui peut expliquer qu'un outil automatique, qui n'aura pas écarté cette possibilité, sera meilleurs, mais dans de très nombreux cas, cela permet de réduire de façon drastique l'arbre des dérivations possibles, rendant la recherche de preuve bien plus efficace.

Mais bien sûr, ce qui me semble fondamental est la capacité d'apprentissage du cerveau humain. Après avoir bouffé pendant des années des preuves déjà faites de théorème, l'homme apprend à démontrer, à appliquer des méthodes génériques, à les adapter, etc. Alors qu'un prouveur basique saura ce qu'on lui a dit de savoir, et le faire tourner sur 10000 problèmes ne lui fera pas résoudre le 10001-ieme plus rapidement.

[InOCamlWeTrust]

Simplement pour répondre à ce qui suit...

Si les numériciens s'en moque de la validité de leurs programmes, c'est sans doute parce qu'ils codent dans des langages où montrer la moindre propriété d'un programme est une migraine garantie. Disons qu'il me semble étrange de dire "ça ne sert à rien de créer quelque chose, la preuve, personne ne s'en sert". Autant abandonner la notion de recherche.

Non. Si les numériciens se moquent de la preuve de leurs programmes, c'est que toute preuve, je crois, en l'état de l'art actuellement serait fausse. En effet, ce qui présente un réel problème dans le domaine du numérique, c'est le fait que les calculs sont tous plus faux les uns que les autres, et ce dû au problème de représentation machine des nombres flottants. On peut mener le même calcul de deux manières différentes, toutes deux théoriquement équivalentes, mais avoir des résultats complètement différents. Il faut s'être réellement battu avec ce genre d'erreurs pour s'en appercevoir, car une chose est le cadre du cours où l'on donne des problèmes visiblement instables, et l'autre est le cadre de la "vraie vie" où des tous petits problèmes tout simples posent d'énormes difficultés quant à leur résolution. Dernièrement, ça m'est arrivé avec des matrices 2 x 2, tout à fait anodines, a priori...

Le problème est encore plus grave si l'on a expérimenté ce genre de phénomène en changeant non pas le code, mais quelques options de compilation... la preuve, ce coup-ci, si elle devait exister, ne serait même pas portable d'une compilation à une autre !

Un système permettant de garantir ou de prouver , de façon automatique ou non, une certaine qualité quant aux erreurs numériques serait le bienvenu.

Quand on vous dit que ce n'est pas demain la veille où on aura des bilans météo fiables sur 24 heures !

[alex_pi]

Non. Si les numériciens se moquent de la preuve de leurs programmes, c'est que toute preuve, je crois, en l'état de l'art actuellement serait fausse.

Bon alors changeons la formulation :-) S'il s'en moque donc, ce n'est pas qu'il s'en moque intrinsequement, c'est que l'outil n'existe pas. Ce qui ne signifie donc pas que la chose est inintéressante !

Le problème est encore plus grave si l'on a expérimenté ce genre de phénomène en changeant non pas le code, mais quelques options de compilation... la preuve, ce coup-ci, si elle devait exister, ne serait même pas portable d'une compilation à une autre !

Si la preuve part du principe que les calculs se font avec une précision d'au moins flottant 64 bits, ça ne devrait pas poser de problème. Ce qui change d'une compilation à l'autre généralement, c'est qu'une valeur est ou non transporter d'un registre interne 80 bits à une case mémoire 64 bits, perdant au passage une grosse précision. Si on part du principe qu'on est au moins en 64 bits, mais sans supposer plus (ni qu'on est *exactement* en 64 bits), une preuve pourrait être résistante aux changement de compilo.

[InOCamlWeTrust]

Il n'y a pas que ça : suivant les options de compilation, tu peux accepter ou non d'effectuer les calculs de fonctions mathématiques en interne (comprendre, version câblée dans le processeur vs version écrite à la main en C dans une librairie)... et là, c'est pas du tout pareil non plus... quand à celà s'ajoutent les différentes versions de BLAS, aucune codée comme le voisin, ça complique encore plus l'affaire !

[Steki-kun]

Il te faut bien faire des hypothèses pour montrer un théorème... Si une opération a un résultat non spécifié, on ne peut pas blâmer un système de certification de programmes pour ne rien pouvoir conclure sur cette opération !
Si l'on fait l'hypothèse (raisonnable!) que les seuls problèmes de calcul sont ceux dus à la représentation finie des réels dans les machines, alors les opérations étant parfaitement spécifiées, il n'y a aucun problème pour prouver des propriétés sur des calculs 'faux'. J'en veux pour preuve le fait que, grâce entre autres aux travaux de Sylvie Boldo, Why/Caduceus permettent désormais de certifier l'absence d'overflows ou une précision minimale dans les calculs effectués par un programme.

[InOCamlWeTrust]

Les gens avec qui j'ai travaillé cet été, dans le domaine des maillages, on trouvé une parade qui vaut toutes les preuves possibles et imaginables : le calcul en précision fixe. Et ça marche !

[HanLee]

Il n'y a pas que ça : suivant les options de compilation, tu peux accepter ou non d'effectuer les calculs de fonctions mathématiques en interne (comprendre, version câblée dans le processeur vs version écrite à la main en C dans une librairie)... et là, c'est pas du tout pareil non plus... quand à celà s'ajoutent les différentes versions de BLAS, aucune codée comme le voisin, ça complique encore plus l'affaire !

Bah, même sans aller voir les travaux du post de Steki-kun, il y a bien des méthodes et théorèmes pour le calcul numérique, pour démontrer la convergence d'un calcul et sa stabilité (ça, c'est par rapport aux erreurs de calculs), ce qui suffit pour montrer que ton calcul numérique est très proche de la réalité.

[InOCamlWeTrust]

Tu n'as pas compris ce que je disais : je ne parlais pas de théorèmes, mais d'implantation d'algorithmes (prouvés avec des théorèmes).