Lean 커널로 모든 제출 증명 검증해 공개 순위 반영
채택된 새 보조정리·증명 기법을 공개 저장소에 지속 반영
핵심 요약
- 이더리움 재단 형식 검증팀은 2026년 8월 20일 koalaIRS12의 입증된 건전성 하한을 128비트로 높이는 better.codes를 시작했다.
- better.codes는 2026년 8월 20일부터 참가자의 제출 정리를 비교기로 대조하고 Lean 커널로 모든 증명을 검증한다.
- 이더리움 재단은 2026년 8월 20일 채택된 증명의 새 보조정리·증명 기법·불가능성 결과를 공개 저장소에 반영한다고 밝혔다.
이더리움 재단 형식 검증팀은 2026년 8월 20일 AI 에이전트로 koalaIRS12의 기계 검증 보안 하한을 128비트까지 높이는 공개 자동 연구 과제 better.codes를 시작했다고 밝혔다. Yukon·zkSecurity와 공동 구축한 이 과제는 참가자가 만든 증명을 공개 순위표에서 비교한다.
koalaIRS12는 간결한 비대화형 증명 시스템(SNARK) 발전을 위한 리드-솔로몬 근접성 문제다. 참가자는 자체 AI 모델과 도구를 이용해 비트 단위로 평가되는 더 높은 건전성 하한을 증명한다.
이번 과제는 실제 시스템이 목표로 삼는 128비트 보안과 현재 증명된 보안 수준의 간극을 줄이는 데 초점을 맞췄다. 해시 기반 SNARK는 zk롤업·zkVM과 이더리움의 포스트퀀텀 로드맵에 이르기까지 리드-솔로몬 부호의 근접성 간극과 상관 합의에 의존하지만, 현재 입증 가능한 결과는 연구자들이 예상하는 기준에 미치지 못한다고 이더리움 재단은 설명했다.
better.codes의 문제는 이더리움 재단이 2026년 앞서 시작한 Proximity Prize 연구에서 가져왔다. Gal Arnon·Dan Boneh·Giacomo Fenzi가 논문 ‘Open Problems in List Decoding and Correlated Agreement’에 제시한 주요 과제와 직접 연결되며, 형식 검증된 지식 논증용 Lean 4 라이브러리 ArkLib에 처음부터 끝까지 형식화됐다.
참가자는 GitHub 계정으로 better.codes에 로그인해 과제 저장소를 복제한 뒤 지정된 제출 영역에서 증명을 작성한다. 정리 명세·매개변수 지점·검증 도구는 고정되며, 비교기가 제출된 정리가 고정 명세와 정확히 일치하는지 확인하고 Lean 커널이 모든 증명을 검사한다.
검증을 통과해 채택된 결과는 참가자와 사용한 AI 모델의 이름을 붙여 공개 저장소에 반영한다. 새 보조정리와 증명 기법, 불가능성 결과도 함께 공유해 다른 참가자와 에이전트가 이전 변경 내역과 제출 기록을 읽고 후속 연구에 활용할 수 있게 했다.
참가자들은 서로 다른 AI 모델과 실행 체계, 도구를 같은 검증 기준에 병렬로 적용한다. 이더리움 재단은 단일 에이전트 구성이 공개 문제의 모든 영역에서 최적일 수 없다는 판단에 따라 여러 독립적 접근이 연구 진전을 앞당기는 구조를 택했다.
2026년 8월 20일 시작한 과제는 우선 koalaIRS12의 입증된 건전성 하한을 128비트로 높이는 문제를 다룬다. 이더리움 재단은 향후 과제를 추가하기를 기대한다고 밝혔으며, 참가 자격·평가·상금·지급 조건은 프로그램 약관에 따르고 진행 과정에서 조정될 수 있다.
