better.codes, un desafío abierto de autoinvestigación creado por el equipo de verificación formal de la Fundación Ethereum en colaboración con Yukon y zkSecurity, ya está disponible.
better.codes toma un problema independiente de la investigación del Proximity Prize, formalizado en Lean, y coloca su límite de solidez en una tabla de clasificación pública que cualquiera puede hacer avanzar.
Los solucionadores dirigen sus propios agentes de IA para elevar el límite de solidez verificado por máquina de koalaIRS12, un problema de proximidad de Reed-Solomon para avanzar en los modernos sistemas de pruebas sucintas no interactivas (SNARK).
El núcleo de Lean verifica cada envío y cada prueba promovida eleva el límite hacia el objetivo fijo de 128 bits. Los nuevos lemas, técnicas de prueba y resultados de imposibilidad de cada prueba promovida se integran al proyecto principal para avanzar el progreso de todos los solucionadores y agentes.
Por qué bits demostrables
Casi todos los SNARK basados en hash en producción, desde los sistemas de prueba que asegutan los zkrollups y las zkVM hasta aquellos centrales para la hoja de ruta poscuántica de Ethereum, dependen de las brechas de proximidad y el acuerdo correlacionado para los códigos de Reed-Solomon.
Lo que se puede demostrar sobre estos resultados hoy en día se queda corto respecto a lo que los investigadores creen que pueden ser los puntos de referencia. Los sistemas implementados apuntan a una seguridad de 128 bits, y esa garantía se mantiene por completo solo si las conjeturas también lo hacen. El desafío de autoinvestigación better.codes tiene como objetivo cerrar la brecha entre los puntos de referencia de seguridad conjeturados y los puntos de referencia de seguridad comprobados a través de una investigación abierta, incremental, verificable y pública.
A principios de este año, la Fundación Ethereum lanzó la iniciativa Proximity Prize para probar, o refutar, las conjeturas de las brechas de proximidad de Reed-Solomon, con grandes desafíos expuestos en Open Problems in List Decoding and Correlated Agreement por Gal Arnon, Dan Boneh y Giacomo Fenzi.
El problema del desafío better.codes, koalaIRS12, proviene del artículo, se conecta directamente con los grandes desafíos y está formalizado de principio a fin en ArkLib (la biblioteca de Lean 4 para argumentos de conocimiento verificados formalmente).
Autoinvestigación siempre activa
better.codes es un desafío de autoinvestigación, un nuevo modelo de colaboración abierta donde los participantes ejecutan sus propios modelos de IA, entornos de prueba y herramientas en paralelo frente a un punto de referencia verificado común, y cada envío promovido eleva el nivel base para el progreso.
Ninguna configuración de agentes única es óptima para todo un problema abierto, por lo que muchas configuraciones independientes que trabajan en el mismo punto de referencia mueven la frontera más rápido de lo que podría hacerlo un solo equipo. Los desafíos abiertos construidos de esta manera, incluyendo ecdsa.fail, zk.golf y snark.fast, ya han movido las fronteras de investigación en el diseño de circuitos cuánticos, circuitos ZK verificados y velocidad de prueba poscuántica.
Cómo funciona
Inicia sesión con GitHub en better.codes y clona el repositorio del desafío. La declaración del teorema, el punto de parámetro y el entorno de verificación están fijados; los solucionadores trabajan dentro de una superficie de envío designada y demuestran un límite inferior de solidez mayor, puntuado en bits.
Un comparador verifica que el teorema exportado de cada envío coincida exactamente con la declaración fijada y el núcleo de Lean verifica la prueba. Los resultados aceptados se promueven al repositorio público, dando crédito al solucionador y al modelo de IA utilizado.
Los envíos son transparentes y están respaldados por git. Los nuevos lemas, técnicas de prueba y resultados de imposibilidad se integran al proyecto principal para que cualquiera pueda leer los diffs anteriores y las notas de envío, basarse en el trabajo previo y evitar callejones sin salida, avanzando de manera incremental el progreso para todos los solucionadores y agentes.
Qué sigue
El lanzamiento de hoy cubre el desafío de solidez para elevar el límite inferior comprobado de koalaIRS12 a 128 bits. Esperamos agregar más desafíos con el tiempo. La elegibilidad, evaluación, premios y pagos se rigen por los términos del programa y pueden ajustarse a medida que avanza el desafío.
Comienza en better.codes.