이더리움 재단 정형 검증 팀이 Yukon 및 zkSecurity와 협력하여 구축한 개방형 자동 연구(autoresearch) 챌린지인 better.codes가 출시되었습니다.
better.codes는 Lean으로 정형화된 Proximity Prize 연구의 독립적인 문제를 가져와, 누구나 발전시킬 수 있는 공개 리더보드에 그 건전성 한계(soundness bound)를 게시합니다.
솔버는 최신 간결한 비대화형 증명 시스템(SNARK)을 발전시키기 위한 리드-솔로몬(Reed-Solomon) 근접성 문제인 koalaIRS12의 기계 검증 건전성 한계를 높이는 데 자체 AI 에이전트를 투입합니다.
Lean 커널은 모든 제출물을 검사하며, 승격된 각 증명은 고정된 128비트 목표를 향해 한계를 높입니다. 그런 다음 승격된 각 증명의 새로운 보조정리(lemma), 증명 기법 및 불가능성 결과가 업스트림에 반영되어 모든 솔버와 에이전트의 진행을 앞당깁니다.
증명 가능한 비트가 중요한 이유
zk롤업(zkrollup) 및 zkVM을 보호하는 증명 시스템부터 이더리움의 포스트 퀀텀 로드맵의 핵심인 시스템에 이르기까지, 거의 모든 프로덕션 해시 기반 SNARK는 리드-솔로몬 코드의 근접성 격차(proximity gaps)와 상관된 합의(correlated agreement)에 의존합니다.
오늘날 이러한 결과에 대해 증명할 수 있는 것은 연구자들이 벤치마크가 될 것이라고 믿는 수준에 미치지 못합니다. 배포된 시스템은 128비트 보안을 목표로 하며, 이러한 보장은 추측이 사실일 때만 온전히 유지됩니다. better.codes 자동 연구 챌린지는 개방적이고 점진적이며 검증 가능한 공개 연구를 통해 추측된 보안 벤치마크와 증명된 보안 벤치마크 사이의 격차를 줄이는 것을 목표로 합니다.
올해 초 이더리움 재단은 리드-솔로몬 근접성 격차 추측을 증명하거나 반증하기 위해 Proximity Prize 이니셔티브를 시작했으며, 갈 아르논(Gal Arnon), 댄 보네(Dan Boneh), 자코모 펜지(Giacomo Fenzi)가 작성한 리스트 디코딩 및 상관된 합의의 미해결 문제(Open Problems in List Decoding and Correlated Agreement)에 주요 과제들이 제시되어 있습니다.
better.codes 챌린지 문제인 koalaIRS12는 해당 논문에서 비롯되었으며, 주요 과제들과 직접적으로 연결되고, ArkLib(정형 검증된 지식 인수를 위한 Lean 4 라이브러리)에서 처음부터 끝까지 정형화되어 있습니다.
상시 가동되는 자동 연구
better.codes는 참가자들이 공통의 검증된 벤치마크에 대해 자체 AI 모델, 테스트 환경(harness), 도구를 병렬로 실행하고, 승격된 모든 제출물이 발전의 기준을 높이는 개방형 협업의 새로운 모델인 자동 연구 챌린지입니다.
미해결 문제 전반에 걸쳐 최적인 단일 에이전트 설정은 없으므로, 동일한 벤치마크에서 작업하는 여러 독립적인 설정이 단일 팀보다 프론티어를 더 빠르게 이동시킵니다. 이러한 방식으로 구축된 ecdsa.fail, zk.golf, snark.fast를 포함한 공개 챌린지들은 이미 양자 회로 설계, 검증된 ZK 회로, 포스트 퀀텀 증명 속도 분야에서 연구 프론티어를 이동시켰습니다.
작동 방식
better.codes에서 GitHub로 로그인하고 챌린지 리포지토리를 복제(clone)하세요. 정리(theorem) 선언, 매개변수 포인트, 검증 테스트 환경은 고정되어 있습니다. 솔버는 지정된 제출 영역 내에서 작업하며 비트 단위로 점수가 매겨지는 더 큰 건전성 하한(soundness lower bound)을 증명합니다.
비교기(comparator)는 각 제출물에서 내보낸 정리가 고정된 선언과 정확히 일치하는지 확인하고, Lean 커널은 증명을 검사합니다. 승인된 결과는 공개 리포지토리로 승격되며, 솔버와 사용된 AI 모델의 공로로 인정됩니다.
제출물은 투명하게 공개되며 git을 기반으로 합니다. 새로운 보조정리, 증명 기법, 불가능성 결과가 업스트림에 반영되므로 누구나 과거의 변경 사항(diff)과 제출 노트를 읽고, 이전 작업을 기반으로 구축하며, 막다른 길을 건너뛰어 모든 솔버와 에이전트의 진행을 점진적으로 앞당길 수 있습니다.
향후 계획
오늘 출시는 koalaIRS12의 증명된 하한을 128비트로 높이기 위한 건전성 챌린지를 다룹니다. 시간이 지남에 따라 더 많은 챌린지를 추가할 수 있기를 바랍니다. 자격, 평가, 보상 및 지급은 프로그램 약관의 적용을 받으며 챌린지가 진행됨에 따라 조정될 수 있습니다.
better.codes에서 시작하세요.