better.codes, un défi de recherche automatisée ouvert, conçu par l'équipe de vérification formelle de la Fondation Ethereum en collaboration avec Yukon et zkSecurity, est maintenant en ligne.
better.codes reprend un problème autonome issu de la recherche du Proximity Prize, formalisé dans Lean, et place sa borne de solidité sur un classement public que tout le monde peut faire progresser.
Les solutionneurs orientent leurs propres agents d'IA pour augmenter la borne de solidité vérifiée par machine de koalaIRS12, un problème de proximité de Reed-Solomon visant à faire progresser les systèmes modernes de preuves succinctes non interactives (SNARKs).
Le noyau Lean vérifie chaque soumission et chaque preuve promue augmente la borne vers l'objectif fixé de 128 bits. Les nouveaux lemmes, techniques de preuve et résultats d'impossibilité de chaque preuve promue sont ensuite intégrés en amont pour faire avancer les progrès de tous les solutionneurs et agents.
Pourquoi des bits prouvables
Presque tous les SNARKs basés sur les hashs en production, des systèmes de preuve sécurisant les zkrollups et les zkVMs à ceux qui sont au cœur de la feuille de route post-quantique d'Ethereum, s'appuient sur les écarts de proximité et l'accord corrélé pour les codes de Reed-Solomon.
Ce qui peut être prouvé concernant ces résultats aujourd'hui n'atteint pas ce que les chercheurs estiment être les références possibles. Les systèmes déployés visent une sécurité de 128 bits, et cette garantie ne tient pleinement que si les conjectures sont exactes. Le défi de recherche automatisée better.codes vise à combler l'écart entre les références de sécurité conjecturées et les références de sécurité prouvées grâce à une recherche ouverte, incrémentale, vérifiable et publique.
Plus tôt cette année, la Fondation Ethereum a lancé l'initiative Proximity Prize pour prouver, ou réfuter, les conjectures sur les écarts de proximité de Reed-Solomon, avec de grands défis exposés dans Open Problems in List Decoding and Correlated Agreement par Gal Arnon, Dan Boneh et Giacomo Fenzi.
Le problème du défi better.codes, koalaIRS12, provient de l'article, fait directement le lien avec les grands défis, et est formalisé de bout en bout dans ArkLib (la bibliothèque Lean 4 pour les arguments de connaissance formellement vérifiés).
Recherche automatisée en continu
better.codes est un défi de recherche automatisée, un nouveau modèle de collaboration ouverte où les participants exécutent leurs propres modèles d'IA, harnais et outils en parallèle par rapport à une référence vérifiée commune, et où chaque soumission promue élève le niveau de base des progrès.
Aucune configuration d'agent unique n'est optimale pour un problème ouvert, c'est pourquoi de nombreuses configurations indépendantes travaillant sur la même référence repoussent les limites plus rapidement que ne pourrait le faire une seule équipe. Les défis ouverts construits de cette manière, notamment ecdsa.fail, zk.golf et snark.fast, ont déjà repoussé les frontières de la recherche dans la conception de circuits quantiques, les circuits ZK vérifiés et la vitesse de preuve post-quantique.
Comment ça marche
Connectez-vous avec GitHub sur better.codes et clonez le dépôt du défi. L'énoncé du théorème, le point de paramètre et le harnais de vérification sont épinglés ; les solutionneurs travaillent à l'intérieur d'une surface de soumission désignée et prouvent une borne inférieure de solidité plus grande, notée en bits.
Un comparateur vérifie que le théorème exporté de chaque soumission correspond exactement à l'énoncé épinglé et le noyau Lean vérifie la preuve. Les résultats acceptés sont promus vers le dépôt public, et attribués au solutionneur ainsi qu'au modèle d'IA utilisé.
Les soumissions sont transparentes et sauvegardées sur git. Les nouveaux lemmes, techniques de preuve et résultats d'impossibilité sont intégrés en amont afin que quiconque puisse lire les diffs passés et les notes de soumission, s'appuyer sur les travaux antérieurs et éviter les impasses, faisant ainsi progresser de manière incrémentale tous les solutionneurs et agents.
Et ensuite
Le lancement d'aujourd'hui couvre le défi de solidité visant à élever la borne inférieure prouvée pour koalaIRS12 à 128 bits. Nous espérons ajouter d'autres défis au fil du temps. L'éligibilité, l'évaluation, les récompenses et les paiements sont régis par les conditions du programme et peuvent être ajustés à mesure que le défi progresse.
Commencez sur better.codes.