Comment automatiser la récompense pour des problèmes difficiles avec Bitcoin

Le site ProofMarket propose de rémunérer de manière automatisée ceux qui arrivent à démontrer des théorèmes de mathématiques. Ceci ouvre un horizon où l'on pourrait rémunérer l'écriture de programmes passant certains tests, de manière décentralisée et sûre pour toutes les parties.

Coq

Coq est à la fois un langage de preuves formelles, c'est-à-dire de preuves de mathématiques vérifiées par ordinateur, et de programmation fonctionelle [1]. Il est utilisé pour vérifier des preuves de théorèmes (par exemple) de mathématiques, de langages de programmation, etc... La garantie qu'un tel logiciel offre en acceptant une preuve est probablement la plus grande possible connue, et en tous cas bien supérieure à une preuve humaine "à la main".

ProofMarket

ProofMarket est un site réalisé par Kazuhiko Sakaguchi qui propose trois choses à ses utilisateurs:

  1. Mettre en ligne un énoncé de théorème en Coq;
  2. Ajouter des bitcoins à la récompense associée à un énoncé;
  3. Prouver un théorème et récupérer la récompense.

Pourquoi distinguer ce site de tous ceux qui, d'une manière ou d'une autre, utilisent les bitcoins? C'est qu'il ne s'agit pas seulement d'une copie de concept existant qui remplace les euros ou les dollars par des bitcoins. Un tel site n'existait pas auparavant, parce qu'il ne pouvait pas exister.
L'argent d'Internet, qu'il soit Visa, Mastercard, Paypal ou autre, n'est pas facilement programmable. Il demande des autorisations d'un serveur central et que des tierces parties viennent prélever leur commission. Il est inimaginable de rendre automatique le remplissage d'un compte en banque automatique par des utilisateurs, suivi d'un vidage de ce compte par un algorithme vérifiant une preuve en Coq.

Bitcoin, sur ProofMarket, permet de faire régner en maître les mathématiques. Si la preuve est correcte, vous récupérez toute la récompense. Sinon, vous n'avez rien. Pas de corruption, pas de triche, pas de commission de Paypal.

Un peu trop de centralisation

ProofMarket est centralisé, puisque c'est un particulier qui le fait tourner et qui vérifie les scripts Coq. Les dangers sont (non exhaustif probablement):

  1. Que le créateur parte avec les récompenses non encore touchées;
  2. Que le créateur change le script de vérification des preuves, laisse des gens déposer des récompenses pour des énoncés dont ils voudraient connaître la preuve, puis dépose sa propre preuve fausse grâce à laquelle il récupère de manière apparemment légitime les fonds déposés.
  3. Que le créateur disparaisse ou arrête de faire tourner le site.

On pourrait croire 2. superflu étant donné que 1. est un moyen plus sûr de voler l'argent des contributeurs. Cependant, un avantage pour le gérant du site d'adopter la tactique 2. est que personne ne peut résoudre le problème entre temps. Ensuite, on verra plus tard que l'on peut imaginer que les dépôts de récompenses soient faits à l'aide d'adresses multi-signatures, ce qui empêche le vol direct des bitcoins mais pas si le vérificateur peut être saboté.

Pistes d'améliorations

On pourrait imaginer faire encore mieux.

Étendre ProofMarket à "Program Market"

On sait tout d'abord depuis longtemps que les preuves sont essentiellement des programmes dont le type (dans un certain système de typage) est l'énoncé du théorème qu'elles démontrent pour des définitions adéquates. Pourquoi donc ne pas étendre ProofMarket aux programmes?
Prouver la correction d'un programme est une tâche ardue, dira-t-on, d'autant plus si elle doit être formelle (i.e dans un langage de preuves comme Coq). Souvent, on se contente pour vérifier qu'un programme fait ce qu'on pense de le soumettre à une batterie de tests pré-établis, de vérifier qu'il les passe tous avec succès en un temps raisonnable. Si cela peut paraître une hérésie aux théoriciens de la programmation, c'est une pratique courante dans l'industrie, et tout à fait raisonnable dans beaucoup de cas pratiques.

Supposons par exemple que je veuille un programme qui inverse les matrices d'entiers de taile (n,n) à une certaine précision. Si je choisis un entier n au hasard entre 1 et 100, et que je remplis une matrice (n,n) d'entiers uniformément pris entre 1 et 100, et que le programme que vous m'avez soumis sans connaître n me renvoie le bon résultat à la bonne précision (résultat que j'aurai pu obtenir à l'aide d'un autre programme), j'ai une confiance suffisamment grande en la correction de votre programme pour vous payer la récompense sans en examiner le code, quitte à vérifier en sus quelques cas limites (matrice non inversible, matrice vide, mauvais format d'entrée).

Bien sûr, le problème précédent a deux propriétés qui ne se généralisent pas:

  1. La probabilité que le programme soit faux étant donné un résultat correct sur un cas aléatoire est extrêmement faible et elle l'est de plus en plus, jusqu'à ce que le doute ne soit plus permis, si l'on répète l'expérience quelques fois.
  2. Au choix:

    2.1 forme forte : on sait calculer d'une autre manière le résultat sur une instance aussi grande que celle que l'on espère soumettre au programme candidat.

    2.2 forme faible: on sait vérifier le résultat, toujours sur une instance de la taille envisagée. Quand bien même nous ne saurions pas inverser les matrices, nous pouvons vérifier le résultat par une simple multiplication [2].

L'absence pour un problème de la première propriété ne se résout hélas pas simplement, autrement qu'en augmentant le nombre de cas d'entrée ou en exigeant une preuve formelle de la correction, ce qui risque de faire fuir les candidats potentiels à sa résolution.

Si la seconde est absente, on ne peut pas faire grand chose. Ceci nous dit que les problèmes qui seront soumis sur un ProgramMarket devront être d'une sorte dont la solution se vérifie aisément. Les problèmes NP-complets sont par exemple parfaitement adaptés à ce contexte.

Augmenter la confiance dans le vérificateur

Utiliser le hash de la solution: pas toujours une bonne idée

Une idée aussi vieille que Bitcoin est d'utiliser des solutions connues à des problèmes pour déverouiller des transactions, par l'intermédiaire du hash de la solution. Il pourrait s'agir d'un jeu de piste, d'un challenge de recrutement d'une agence de renseignement, d'une tentative de motivation de ses élèves par un professeur généreux.. Voici le déroulement.

Supposons que la solution de mon problème est s et que le hash de s est h.

Je crée une transaction qui n'est utilisable que si celui qui la dépense peut fournir une valeur dont le hash est h, ce qui permet de payer la première personne à trouver cette valeur. h est public puisque sur la blockchain, mais si la solution ne se "bruteforce" pas (par exemple, si c'est un entier entre 1 et 1 million, ceci n'est PAS une bonne idée), il est impossible de retrouver la solution à partir de son hash, seulement vérifier que l'on a la bonne solution en comparant son hash à h.

Parfois cela ne suffit vraiment pas

Ceci marche très bien lorsque le problème que l'on soumet a une solution constante (par opposition à une fonction), connue par celui qui le soumet et non triviale (c'est-à-dire qu'on ne peut pas la bruteforcer en essayant toutes les possibilités dans un ensemble petit). Si l'une des deux premières conditions vient à manquer, on n'a pas d'autre choix que de devoir exécuter un programme pour savoir si la solution proposée est satisfaisante, ce que ne permet pas au-delà de quelques instructions d'assembleur (certes augmentées de primitives cryptographiques) le langage de script de Bitcoin.

La solution: un oracle

L'idée est alors de faire appel à un oracle: une entité en laquelle on a confiance, qui va exécuter le script de vérification et qui va, s'il est satisfait, nous délivrer un sésame permettant de revendiquer la récompense. Ce sésame consisterait selon toute vraisemblance en une signature avec une certaine clé privée (siège de la confiance de l'oracle et donc donnée extrêmement sensible) de la transaction extrayant la récompense vers l'adresse du candidat.
Un avantage des oracles est qu'ils peuvent interagir avec le monde physique, et vérifier par exemple des avis de décès, des résultats sportifs ou d'élections, ou encore les précipitations dans une certaine station météo.

Le problème de la confiance resurgit aussitôt: qui choisir pour être cet oracle? Un serveur? Un humain? Comment garantir qu'il est incorruptible?

Deux solutions s'offrent à nous, que nous pouvons combiner pour un résultat très fiable:

  1. Utiliser un serveur dont on peut prouver qu'il exécute un certain programme dont le code est public, donc vérifiable par tous;
  2. Utiliser plusieurs oracles en exigeant qu'une majorité d'oracles soient d'accord avant de valider la transaction pour augmenter encore la sécurité et se prémunir contre les accidents et autres "downtime".

Amazon Web Services (AWS) fournit un moyen d'accomplir 1., moyennant la confiance en l'entreprise américaine. La création de moyens de garantir 1. est un projet d'entreprise qui pourrait avoir de l'avenir, si les contrats numériques (et surtout algorithmiques) prennent le pas sur leurs confrères en papier.
Quant à 2., il s'agit simplement d'établir une adresse multi-signature.

Comment faire si on ne veut pas que le vérificateur soit public?

Dans ce cas, il y a deux intérêts contradictoires: celui qui soumet le problème peut vouloir cacher le test auquel il soumet les programmes candidats (penser au cas du produit de matrices), tandis que celui qui veut contribuer à la récompense ou celui qui veut le résoudre veut s'assurer que le test n'est pas une arnaque et teste bien ce qu'il prétend.

Une première solution serait que celui qui soumet donne une batterie de disons 10 tests, et que le serveur choisisse "au hasard" 1 test pour rester privés, et 9 qui deviennent publics. Si l'un des tests est incorrect, celui qui soumet le problème prend un gros risque d'être démasqué (on pourrait imaginer qu'il soumette une caution pour pouvoir utiliser l'oracle et que cette caution lui soit confisquée en cas de malfaisance avérée).
Une autre serait qu'à la résolution du problème, la transaction doive attendre un certain temps avant d'être dépensée et que tous les tests ainsi que la solution soient publics pendant ce délai, afin qu'une arnaque puisse être détectée et signalée, et que la transaction puisse être invalidée.

Conclusion

Si on examine bien la situation, la nécessité même d'avoir une plateforme qui héberge les problèmes et les solutions a disparu avec les étapes de décentralisation proposées. On n'a plus de point de défaillance unique, et on a créé un marché des programmes décentralisé, sans confiance aveugle en une tierce partie isolée.

Des propositions fantastiques de marchés décentralisés utilisant des cryptomonnaies apparaissent ces temps-ci, mais elles se concentrent sur des biens matériels (service à la eBay) ou sur des services bien définis (assurance, prêt, escrow). Pourtant, elles ne sont pas armées pour gérer la matière première d'Internet et de l'informatique: le code et les algorithmes.

La monnaie d'Internet mérite un projet qui comble ce vide.

[1] À noter qu'il n'est pas Turing complet, i.e toutes les fonctions récursives terminent.
[2] On ne s'occuper pas ici de questions numériques, ce n'est pas le sujet :-)
comments powered by Disqus