Anthropic, zkSNARK로 LLM 추론 증명하는 FlashProve 공개... H100 한 장에 초당 110토큰
- Anthropic이 zkSNARK 기반 추론 증명 시스템 FlashProve를 공개함. Llama 4 Maverick(400B MoE)에서 H100 한 장이 초당 약 110토큰으로 증명을 생성하고, 1,024토큰 요청당 증명 크기는 약 19MB이며, 이는 vLLM으로 모델 자체를 돌릴 때의 70~95배 GPU 시간임.
- 가중치 커밋과 추론 증명으로 모델 가중치는 숨기지만 아키텍처 은닉은 목표가 아님. 4비트 양자화 가중치와 정수 연산 prefill을 사용하고, 기존 오픈소스 시스템보다 수백 배 빠름.
- Claude가 만든 프로토콜 명세와 함께 C++ 빠른 검증기, Lean으로 최상위 보안 보장 명제를 형식 검증한 검증기와 증명을 공개함. Lean 정리를 감사할 수 있는 대화형 시각화 도구도 포함됨.
- 블로그, 기술 보고서, 프로토콜 명세, 실행 코드, Lean 증명 다섯 개 산출물을 Apache 2.0으로 공개함. 중간 단계 연구이며 다른 사람들이 가져다 개선하는 것이 목표라고 밝힘.
- 현재는 greedy 디코딩과 짧은 컨텍스트만 지원해 실사용에는 제약이 있음. 정수 버전 가중치가 부동소수점 추론과 작은 오차 안에 있다는 전제에는 adversarial 프롬프트가 빠져 있음.
Hacker News 의견들
응답이 진짜 그 모델에서 나왔는지 사용자가 확인할 수 없다니, 그런 걱정을 하게 만든 개발자가 누굴까 싶음. 사용자한테 안 보이게 ML 요청을 inferior 모델로 돌린 회사가 이런 PR 하는 거 웃기지.
OpenRouter 같은 데서 다른 모델로 라우팅하는 경우는 이게 잡아줄 듯. 근데 호스트가 진짜 가중치로 서명만 하고 실제론 양자화 모델을 돌리면 어떻게 막나?
정수 버전 가중치를 증명하고 각 토큰이 그 모델의 greedy 선택임을 증명한다고 하더라. 부동소수점이나 샘플링 디코딩이면 어느 지점에서 어긋날 수 있대. 그럼 못 잡는 거 아님?
오차 크기를 보면 알 수 있지 않을까. 정수 버전이 부동소수점 추론과 작은 오차율 안에 있다고 테스트됐대. adversarial 프롬프트는 커버 안 되고.
오픈 가중치는 잡힐걸. 공개 가중치로 커밋하고 시드를 공개하면 Hugging Face 파일에서 커밋을 다시 계산해서 체크포인트랑 양자화가 맞는지 확인 가능함. Maverick 데모가 그렇게 한 거고. 다만 greedy 디코딩이랑 짧은 컨텍스트만 되고 GPU 시간이 70-95배라 TEE가 더 쌀 수도 있음.
흥미롭긴 한데 증명하는 속성이 별로 중요하지 않아 보임. Anthropic이 안 쓴 싼 모델로 바꿔치기 안 했다, MiTM 안 당했다 정도잖아. 그건 기본 아닌가. 데이터 안 털렸다는 것도, 답변이 쓸모 있다는 것도 알려주지 않음.
Anthropic 사용자들이 가장 많이 하는 불평이 바로 그거임. 오늘 Opus 왜 이래 같은 소리가 다 사라질 수도 있는데 그걸 기본이라고? 지금은 확인할 방법이 아예 없음.
처음엔 LLM 출력이 정답인지 증명하는 훨씬 중요한 문제인 줄 알았는데 모델 뭐 쓰는지 증명하는 사소한 문제였음. 누가 씀? 제공자를 못 믿으면 이미 끝난 거고, 어차피 프라이빗 데이터 다 주면서 서비스에 의존하는데 혼자 돌리는 게 아니면 소용 없음.
클라이언트랑 Anthropic API 서버 사이에 콘텐츠 프록시가 요즘 많아서 그럴 때 유용함.
서론 첫 단락만 읽어도 나옴. 독립 평가자가 배포 전후로 같은 모델을 평가하는지, 서드파티 라우팅 쓰는 클라이언트가 돈 낸 모델 토큰을 받는지, 공격자가 토큰 스트림을 바꿔치기하는지 확인할 수 있게 해줌.
장점은 이거임. FP 연산이 하드웨어마다 조금씩 달라지는데 하드웨어 설정이 제대로 출력 내는지 검증해줌. 외부 제공자가 말한 추론을 돌리는지도 확인되고, 양자화하면 증명이 깨져서 새 서명이 필요함. 파인튜닝이나 모델 바꿔치기도 마찬가지고 Kimi나 DeepSeek가 요청을 포워딩해서 증류한다는 의혹 같은 것도 걸러짐. 다만 지금은 정수 가중치에 1k 컨텍스트라 장난감 수준임.
고객은 출력이 맞는지 신경 쓰고 Anthropic은 자기 모델이 생성했는지 신경 씀. 후자만 풀고 전자는 얼버무림. 결국 싼 모델 라우팅에 FUD 주려는 거고 자기 비즈니스 모델과 상충하지.
중국 리셀러들이 Claude 접근권을 팔면서 다른 모델로 바꿔치기하는 사기를 치는데 그런 건 막아줄 듯. OpenRouter나 Fireworks 사용자한테도 추가 보장이 되고.