Anthropic, 암호학적 AI 추론 증명 기술 FlashProve 공개

Anthropic은 2026년 11월 2일 FlashProve를 공개했다. FlashProve는 언어 모델의 응답이 공개하지 않은 채 커밋된 가중치에서 생성되었음을 암호학적 증명으로 입증하는 오픈 소스 연구용 프로토타입이다. 회사는 Meta의 Llama 4 Maverick에서 초당 110토큰의 속도로 증명을 생성했다고 밝혔다.

이 연구는 호스팅 AI의 검증 공백을 해소하기 위한 것이다. 답변의 품질이 높다고 해서 어떤 모델이 답변을 생성했는지 확인되는 것은 아니다. 라우팅 서비스가 다른 시스템으로 바꿔치기할 수 있고, 평가자가 테스트 대상으로 의도한 모델과 다른 모델을 제공받을 수도 있으며, 공격자가 토큰 스트림을 변조할 수도 있다. 가중치가 비공개이고 상당한 하드웨어가 필요한 경우, 사용자가 모델을 다시 실행해 확인하는 방법은 현실적이지 않다.

숨겨진 가중치에 응답을 결속하기

FlashProve는 신뢰할 수 있는 하드웨어에 의존하는 대신 소프트웨어만으로 구현되며, 영지식 간결 지식 논증(zkSNARK)을 사용한다. 오프라인 단계에서 제공자는 가중치의 정확한 한 세트를 식별하는 짧은 커밋먼트를 공개하면서 해당 가중치는 비밀로 유지한다. 프롬프트와 응답이 완료된 쌍마다 시스템은 출력 토큰이 커밋된 모델에서 생성되었음을 증명한다. 커밋먼트와 프롬프트, 응답을 가진 사람은 누구나 가중치에 접근하지 않고도 증명을 확인할 수 있다.

이 기술이 목표로 하는 속성은 완전성, 건전성, 영지식성과 간결성이다. 정직하게 생성된 증명은 받아들여져야 하며, 거짓 진술을 참이라고 인증하려면 널리 신뢰받는 암호학적 가정을 깨야 한다. 증명을 확인해도 가중치나 중간 계산값이 드러나지 않아야 한다. 또한 모델의 아키텍처 자체는 공개되지만, 각 토큰을 생성할 때 어떤 전문가 혼합 하위 네트워크가 실행됐는지는 숨긴다.

이 구현은 Maverick의 전문가 혼합 구조를 활용한다. 증명 생성에 필요한 연산량은 전체 4,000억 개가 아니라 토큰 하나에 활성화되는 약 170억 개의 매개변수에 비례하면서도, 어떤 전문가가 선택됐는지는 숨긴다. 분할된 가중치를 호스트 메모리에서 스트리밍하므로, 호스트 메모리 약 290GB와 함께 사용하는 GPU 한 대(80GB)에서 증명을 생성할 수 있다.

Anthropic은 고객 대상 무결성 검사, 독립 평가, 규제 도구, 승인된 모델 사용 요건의 집행 등을 활용 사례로 제시한다. 추론 인증서는 요청이 주장된 모델을 통해 처리됐음을 증명할 수 있지만, 동일한 하드웨어가 다른 모델을 학습하는 데에도 사용되지 않았음을 입증하지는 못한다. 따라서 컴퓨팅 용량의 사용 방식에 근거한 규정 준수 요건에 대해 인증서가 입증할 수 있는 범위에는 한계가 있다.

증명 성능과 추론 오버헤드

Anthropic은 공개적으로 이용할 수 있는 모델의 4비트 변환본으로 평가를 진행했다. H100 한 대와 CPU 코어 24개를 탑재한 서버는 요청 24건으로 구성된 배치의 증명을 약 223초 만에 생성했으며, 요청마다 18.78MB의 증명 데이터를 만들었다. 오프라인 커밋먼트 단계에는 약 39분이 걸렸다.

검증 단계에서 클라이언트는 약 6.5MB의 커밋먼트를 다운로드하고 GPU 없이 CPU에서 증명을 확인한다. Anthropic은 오프라인 단계의 검사까지 포함해 스레드 24개를 사용했을 때 검증에 17초, 스레드 하나를 사용했을 때 21초가 걸렸다고 측정했다.

이 측정 결과는 CPU만 사용하는 검사 과정과 훨씬 더 많은 연산이 필요한 증명 생성 작업을 구분해 보여준다. vLLM을 실행하는 H100 8대에서 FP8 추론을 수행한 경우와 비교했을 때, Anthropic의 측정에서 증명 생성은 동일한 배치 기준 GPU당 시간이 약 72배 더 필요했고, 테스트한 vLLM 부하 중 가장 높은 부하에서는 약 94배 더 필요했다. 따라서 이러한 처리량에는 증명 없이 모델을 서비스할 때보다 상당한 비용이 따른다.

형식 검증과 현실적인 한계

FlashProve 저장소에는 증명 생성기, 빠른 C++ 검증기, 더 느린 Lean 검증기, 최상위 수학적 명제에 대한 Lean 증명, 대화형 정리 시각화 도구가 Apache 2.0 라이선스로 포함되어 있다. 저장소는 버전 0.16.0을 유지 관리되지 않는 연구용 산출물로 표시하며, 기여도 받지 않는다.

Lean 작업은 랜덤 오라클 모델에서 완전성, 건전성, 영지식성을 다룬다. 형식 명제가 의도한 보장을 실제로 표현하는지 확인하려면 여전히 수동 검토가 필요하다. Lean 검증기는 건전성 정리와 형식적으로 연결되어 있지만, 일상적인 사용을 목적으로 한 C++ 검증기에는 형식적 보장이 없으며 Lean 검증기와 결과가 일치하는지 테스트하는 방식으로 검증했다.

프로젝트의 알려진 한계 문서에 따르면, AI 시스템은 사람의 지시에 따라 소프트웨어와 Lean 증명, 문서 거의 전부를 작성하고 보고된 테스트를 실행했다. 독립적인 보안 감사는 이루어지지 않았으며, 가중치 은닉과 적대적 증명에 대한 테스트도 제한적이다.

증명은 탐욕적 디코딩을 적용한 가중치의 정확한 정수 버전을 대상으로 한다. 부동소수점 추론이나 샘플링 디코딩은 증명 대상 계산과 달라질 수 있으며, 일반적인 오류 테스트는 적대적으로 설계된 프롬프트를 다루지 않는다. 컨텍스트는 1,024토큰으로 제한되고, 타이밍 공격을 비롯한 부채널 공격은 보장 범위에 포함되지 않는다. 추론과 동시에 증명하는 방식과 비교하면 사후 증명은 계산을 반복해야 하고, 보장이 늦어지며, 비결정성이 생긴다.

검증 가능한 추론을 실제 서비스 트래픽에 대한 일상적인 점검 절차로 정착시키려면, 이번 릴리스에서 드러난 과제를 해결하는 데 남은 작업이 집중돼 있다. 증명 비용을 낮추고, 제약이 덜한 디코딩과 더 긴 컨텍스트를 지원하며, 빠른 구현을 정형 프로토콜에 더욱 확실히 연결해야 한다.