이더리움 재단이 better.codes 챌린지를 출시하여 해시 SNARK의 증명 가능한 안전성을 향상시킵니다

이더리움 재단 형식 검증 팀이 Yukon, zkSecurity와 협력하여 만든 오픈 자동 연구 챌린지 better.codes가 이제 온라인으로 제공됩니다. 이 플랫폼은 Proximity Prize의 자가 포함 문제를 Lean으로 형식화하고, koalaIRS12의 기계 검사 신뢰성 경계를 공공 순위에 넣어 누구나 이를 개선할 수 있도록 하여 해시 기반 SNARK 및 후양자 이더리움 관련 보안 기준을 발전시키는 데 기여합니다.

해결자는 AI 지능체를 가져와 Reed-Solomon 근접 문제에 대해 더 높은 신뢰성 하한을 증명하며 고정된 128비트 목표를 향해 나아갈 수 있습니다. Lean 커널은 제출된 모든 내용을 검증하며, 승격된 증명은 공개 경계를 높이고, 새로운 보조 정리, 증명 기술 및 불가능성 결과는 상류와 동기화되어 모든 참가자가 재사용할 수 있도록 합니다. 생산 환경에서 대부분의 해시 SNARK는 관련 근접 간격 및 관련 합의 결론에 의존하며, 현재 증명 가능한 결과는 연구자가 신뢰하는 기준보다 낮습니다. 이 챌린지는 개방적이고 점진적이며 검증 가능한 방식으로 이 격차를 줄이는 것을 목표로 합니다.

koalaIRS12는 관련 논문에서 유래되었으며 ArkLib에서 엔드 투 엔드 형식화되었습니다. 참가자는 GitHub를 통해 로그인하고 챌린지 저장소를 클론하여 고정 정리 진술 및 검증 프레임워크 하에 제출할 수 있습니다; 비교기와 Lean 커널이 확인한 후 결과는 공공 저장소에 기록되며 해결자와 사용된 모델이 명시됩니다. 오늘 온라인으로 제공되는 것은 koalaIRS12의 증명된 하한을 128비트로 높이는 신뢰성 챌린지이며, 이후 더 많은 문제를 추가할 수 있으며 세부 사항은 프로젝트 약관에 따릅니다.