STARK 검사 200회→148회 가능성…수학 과제 3개 공개

STARK 증명의 검사 횟수를 줄이기 위한 수학 과제 세 개가 공개됐다. 과제 페이지는 특정 조건에서 100비트 보안에 필요한 검사 횟수가 200회에서 148회로 줄 수 있다는 계산 예도 제시했지만, 이는 목표 증명과 전체 보안성 분석을 전제로 한 수치다.

provably.fast의 공식 과제 페이지에는 세 목표가 제시돼 있다. 각 명제는 수학 정리 증명 도구인 Lean에 고정돼 있으며, 독립적인 검토를 거친 증명만 해결로 인정된다. 현재 세 목표는 모두 열려 있다.

STARK는 해시 함수를 기반으로 하는 영지식 증명 체계다. 리드·솔로몬 코드는 이 체계에서 검증할 데이터의 신뢰성을 다루는 데 쓰이며, 검증자는 무작위 조합을 검사해 제출된 데이터가 코드에 가까운지 확인한다.

과제는 이 검사 과정에서 잘못된 데이터가 정상적인 코드처럼 보이게 할 수 있는 ‘나쁜 도전값’의 수를 제한하는 데 초점을 맞췄다. 나쁜 도전값의 상한이 줄면 검증에 필요한 무작위 검사를 낮출 근거가 생기지만, 상한 개선만으로 실제 증명 크기나 보안성이 바뀌는 것은 아니다.

목표는 코드의 동의율 구간에 따라 나뉜다. T1은 1차 경계와 Johnson 경계 사이 구간에서 알려진 이차식 상한을 선형 상한으로 낮추려는 과제다. T2는 1차 경계 아래의 더 넓은 범위에서 이차식 상한을 증명하는 것을 목표로 한다.

T3는 증명 생성에 쓰이는 평가 영역의 상한을 다룬다. 과제 페이지는 동의율 5/8, 비율 1/2인 첫 사례에서 기존 구성의 나쁜 도전값 수가 114n/16까지 이르는 조건에 대해 16n 상한을 증명하도록 제시했다.

페이지가 든 검사 횟수 예시는 FRI 방식, 비율 1/2, n=2²⁰, 124비트 필드 등 특정 조건을 전제로 한다. 이 계산에서는 100비트 보안에 필요한 검사가 현재 200회이며, T3의 첫 사례가 증명되면 148회로 줄어든다. 페이지는 이 수치가 검사 횟수 계산에 한정되며, 실제 적용에는 전체 보안성 분석이 필요하다고 설명했다.

이전 연구에서는 수학적 상한을 실제 구현의 증명 크기와 연결한 결과가 나왔다. 꽝 다오(Quang Dao), 스콧 듀크 코미너스(Scott Duke Kominers), 저스틴 탈러(Justin Thaler)가 9월 17일 등록한 프리프린트는 같은 보안 목표에서 ProveKit 여권 증명을 79.4KB(11.1%), ZisK 압축 최종 증명을 13.2KB(4.63%), LambdaVM CPU 하위 증명을 59.8KB(4.85%) 줄였다고 보고했다. 해당 결과는 논문의 구체적인 구현과 설정에서 나온 것이다.

적용 범위에는 경계가 있다. 10월 9일 공개된 별도 논문은 이진 필드에서 Johnson 경계 아래의 근접성 간격이 성립하지 않는 반례를 제시했다. 과제의 배경 설명은 이 결과가 충분히 큰 특성의 필드를 조건으로 하는 이번 목표를 해결하거나 반박하지는 않는다고 설명한다.

사람과 AI 에이전트 모두 과제에 참여할 수 있으며, 아이디어와 보조정리, 반례, 증명 등 기여 내용이 기록된다. 오픈AI가 내부 모델의 수학 결과와 일부 Lean 형식화를 공개한 사례처럼 형식화된 수학 결과 공개도 이어지고 있다.

세 공개 과제가 해결됐거나 실제 STARK 구현의 증명 크기가 추가로 줄었다는 결과는 아직 나오지 않았다. 과제의 수학적 상한이 증명되더라도 실제 효과를 확인하려면 적용 대상 프로토콜의 보안성과 증명 크기를 별도로 분석해야 한다.