better.codes, um desafio aberto de autopesquisa construído pela equipe de verificação formal da Fundação Ethereum em colaboração com a Yukon e a zkSecurity, já está no ar.
O better.codes pega um problema independente da pesquisa do Proximity Prize, formalizado em Lean, e coloca seu limite de solidez em uma tabela de classificação pública que qualquer um pode impulsionar.
Os solucionadores direcionam seus próprios agentes de IA para elevar o limite de solidez verificado por máquina do koalaIRS12, um problema de proximidade de Reed-Solomon para avançar os modernos sistemas de provas sucintas não interativas (SNARKs).
O kernel do Lean verifica cada submissão e cada prova promovida eleva o limite em direção à meta fixa de 128 bits. Os novos lemas, técnicas de prova e resultados de impossibilidade de cada prova promovida são então integrados (upstreamed) para avançar o progresso de todos os solucionadores e agentes.
Por que bits comprováveis
Quase todos os SNARKs baseados em hash em produção, desde os sistemas de prova que garantem a segurança de zkrollups e zkVMs até aqueles centrais para o roteiro pós-quântico do Ethereum, dependem de lacunas de proximidade e concordância correlacionada para códigos Reed-Solomon.
O que pode ser provado sobre esses resultados hoje fica aquém do que os pesquisadores acreditam que os benchmarks possam ser. Os sistemas implantados visam uma segurança de 128 bits, e essa garantia só se mantém totalmente se as conjecturas também se mantiverem. O desafio de autopesquisa better.codes visa fechar a lacuna entre os benchmarks de segurança conjecturados e os benchmarks de segurança comprovados por meio de pesquisa aberta, incremental, verificável e pública.
No início deste ano, a Fundação Ethereum lançou a iniciativa Proximity Prize para provar, ou refutar, as conjecturas de lacunas de proximidade de Reed-Solomon, com grandes desafios apresentados em Open Problems in List Decoding and Correlated Agreement por Gal Arnon, Dan Boneh e Giacomo Fenzi.
O problema do desafio better.codes, koalaIRS12, vem do artigo, faz a ponte diretamente com os grandes desafios e é formalizado de ponta a ponta na ArkLib (a biblioteca Lean 4 para argumentos de conhecimento formalmente verificados).
Autopesquisa sempre ativa
O better.codes é um desafio de autopesquisa, um novo modelo de colaboração aberta onde os participantes executam seus próprios modelos de IA, ambientes de teste (harnesses) e ferramentas em paralelo contra um benchmark verificado comum, e cada submissão promovida eleva o piso para o progresso.
Nenhuma configuração agêntica única é ideal para um problema aberto, portanto, muitas configurações independentes trabalhando no mesmo benchmark movem a fronteira mais rápido do que qualquer equipe sozinha conseguiria. Desafios abertos construídos dessa forma, incluindo ecdsa.fail, zk.golf e snark.fast, já moveram as fronteiras de pesquisa em design de circuitos quânticos, circuitos ZK verificados e velocidade de prova pós-quântica.
Como funciona
Faça login com o GitHub no better.codes e clone o repositório do desafio. A declaração do teorema, o ponto de parâmetro e o ambiente de verificação estão fixados; os solucionadores trabalham dentro de uma superfície de submissão designada e provam um limite inferior de solidez maior, pontuado em bits.
Um comparador verifica se o teorema exportado de cada submissão corresponde exatamente à declaração fixada e o kernel do Lean verifica a prova. Os resultados aceitos são promovidos para o repositório público, creditados ao solucionador e ao modelo de IA utilizado.
As submissões são transparentes e baseadas em git. Novos lemas, técnicas de prova e resultados de impossibilidade são integrados para que qualquer pessoa possa ler diffs anteriores e notas de submissão, construir sobre trabalhos prévios e pular becos sem saída, avançando incrementalmente o progresso para todos os solucionadores e agentes.
O que vem a seguir
O lançamento de hoje cobre o desafio de solidez para elevar o limite inferior comprovado do koalaIRS12 para 128 bits. Esperamos adicionar mais desafios ao longo do tempo. Elegibilidade, avaliação, prêmios e pagamentos são regidos pelos termos do programa e podem ser ajustados à medida que o desafio avança.
Comece em better.codes.