Anthropic FlashProve: 초당 110 토큰의 zkSNARK 증명 가능 추론

Anthropic은 특정 커밋된 모델이 주어진 출력을 생성했음을 증명하기 위해 zkSNARK를 사용하는 증명 가능 추론(provable inference)을 위한 오픈 소스 연구 프로토타입인 FlashProve를 공개했습니다. 400B 파라미터의 전문가 혼합(mixture-of-experts) 모델인 Llama 4 Maverick에서, Anthropic은 단일 H100 GPU에서 초당 약 110 토큰의 증명 생성 속도를 보고했으며, 약 19MB 크기의 증명은 CPU에서 수 초 내에 검증됩니다. 이 결과는 모델 식별 및 출력 출처에 대한 암호학적 증명을 라우팅 무결성, 변조 탐지, 감사 도구 및 AI 속도 조절을 연구하기에 충분히 실용적인 수준으로 만들었기 때문에 중요합니다. 다만 Anthropic은 이를 완성된 시스템이 아닌 중간 연구 단계로 명시하고 있습니다.

Anthropic이 공개한 것

Anthropic은 연구 게시물과 함께 5가지 아티팩트를 발표했습니다. 블로그 게시물 본문, 기술 보고서, 프로토콜 설명, 실행 가능한 코드, 그리고 Lean 증명이 그것입니다. 코드에는 증명자(prover), 빠른 C++ 검증자(verifier), 그리고 증명 가능하게 올바른 Lean 검증자가 포함되어 있습니다. Lean 자료에는 최상위 수학적 문장에 대한 증명과 감사를 돕기 위한 Lean 정리의 대화형 시각화 도구가 포함되어 있습니다. Anthropic은 코드, Lean 증명 및 문서를 Apache 2.0 라이선스 하에 공개했습니다.

이 게시물은 FlashProve를 증명 가능 추론을 위한 오픈 소스 고성능 프로토타입으로 설명합니다. Anthropic은 그 목표가 증명 가능 추론의 개발을 가속화 및 촉진하고, 영지식 간결한 논증(zero-knowledge succinct arguments)이 이 문제에 실용적임을 입증하는 두 가지라고 밝힙니다. 또한 Anthropic은 이 게시물이 완성된 연구 의제가 아닌 중간 진행 상황을 공유하는 것이며, 다른 이들이 이 작업을 가져가 개선해 줄 것을 요청하고 있습니다.

증명 가능 추론이 중요한 이유

증명 가능 추론은 간단한 신뢰 격차를 해결합니다. 오늘날 모델에 질의하는 사용자는 응답이 개발자가 주장하는 특정 모델에서 나왔는지 확인할 수 없습니다. 응답은 라우팅 서비스에 의해 몰래 대체된 더 저렴한 모델에서 나왔거나, 토큰 스트림을 변조한 공격자로부터 나왔을 수 있습니다. 출력 품질만으로 판단하는 것은 신뢰할 수 없습니다.

zkSNARK(영지식 간결한 지식 논증)를 사용하면 증명자는 짧은 인증서를 사용하여 계산이 올바르게 실행되었음을 검증자에게 확신시킬 수 있습니다. 이 인증서는 계산의 정확성 외에 어떠한 정보도 드러내지 않기 때문에 영지식이며, 증명보다 검증이 기하급수적으로 빠르기 때문에 간결합니다. 증명 가능 추론의 경우, 모델 제공자는 가중치 세트에 커밋하고 각 응답이 해당 커밋된 모델에 의해 생성되었음을 증명합니다. 증명은 가중치에 대해 아무것도 드러내지 않으며, 검증자는 가중치나 제공자의 하드웨어가 필요하지 않습니다.

Anthropic은 이 동기를 네 가지 신뢰 과제로 정리합니다.

과제 1: AI 개발 속도 조절

AI 개발을 규제하고 속도를 조절하려는 일부 제안은 하드웨어와 그 사용 방식 모니터링에 의존합니다. 제공자는 강력한 새 모델을 훈련하는 대신 추론에 하드웨어를 할당해야 할 수 있습니다. 제공자는 더 저렴한 모델을 서비스하거나 컴퓨팅 자원을 예상치 못하게 사용하여 훈련을 위한 자원을 확보하는 방식으로 속임수를 쓸 수 있습니다.

zkSNARK를 사용하면 규제 기관은 특정 기간 동안 서비스된 추론 요청을 포괄하는 인증서를 요청할 수 있습니다. 인증서는 요청이 주장된 모델에 의해 생성되었음을 보여야 합니다. 악의적인 제공자는 하드웨어가 실제로 올바른 모델을 서비스하지 않는 한 해당 요청을 충족할 수 없습니다. 규제 기관은 제공자의 하드웨어 설정 없이도 주장을 확인할 수 있으며, 제공자는 규제 기관이 독점적인 모델 정보를 알 수 없다는 보장을 받습니다. Anthropic은 중요한 한계를 지적합니다. 이는 하드웨어가 추론을 서비스하고 있음을 검증하지만, 해당 하드웨어가 뒤에서 훈련을 수행하고 있지 않음을 확립하지는 못합니다.

과제 2: 변조 탐지

모델의 가치가 높아짐에 따라 추론 서버는 표적이 됩니다. 공격자나 악의적인 에이전트가 서버를 손상시켜 가중치를 유출하거나, 악의적인 응답을 제공하거나, 실제 응답 사이에 숨을 수 있습니다. 적대자가 외부인일 필요는 없습니다. 더 발전된 모델이 승인된 약한 모델 대신 실행되어 분류기나 모니터링을 피하기 위해 약한 모델인 척할 수 있습니다.

zkSNARK를 사용하면 제공자는 모든 응답에 대해 유효한 증명을 요구할 수 있습니다. 증명은 가중치에 대한 특정 커밋에 묶여 있으므로, 단순히 어떤 모델이 생성했다는 것이 아니라 커밋된 모델이 응답을 생성했음을 인증합니다. 서버를 손상시킨 공격자나 다른 모델로 대체된 모델은 탐지를 피하기 위해 예상되는 가중치에 대한 유효한 증명을 생성해야 하는데, 이는 불가능합니다. 사용자 또한 내부 정보를 유출하지 않고 확인 비용이 저렴하기 때문에 증명을 받을 수 있습니다.

Anthropic은 이를 Frontier Safety Roadmap과 연결합니다. 이 로드맵에서 Anthropic은 2026년 9월 30일까지 AI 모델 출력을 안정적으로 서명하여 특정 모델 가중치 세트에 귀속시킬 수 있는 증명 가능 추론 프로토타입을 개발하겠다는 공개 목표를 세웠습니다. Anthropic은 추론 트래픽에 서명하고 신뢰할 수 있는 서버에서 추론을 재계산하는 별도의 관련 프로젝트를 통해 해당 목표를 달성했다고 밝혔으며, FlashProve는 다른 방법으로 동일한 목표를 추구합니다.

과제 3: 텍스트 출처

개발자는 소프트웨어 라이브러리가 프론티어 사이버 보안 모델에 의해 취약점 스캔을 받았다고 주장할 수 있으며, 기업은 사업 계획이 적절한 모델에 의해 승인되었다고 주장할 수 있습니다. 사용자는 모델을 실행할 자원이나 권한이 없을 수 있으며, 채팅 로그를 게시하는 것은 로그가 더 저렴하거나 성능이 낮은 모델로 위조될 수 있기 때문에 절대적인 보장을 제공하지 않습니다.

zkSNARK를 사용하면 제공자는 주어진 입력에 대해 주장된 모델이 출력을 생성했다는 증명을 첨부할 수 있습니다. 간결성 덕분에 사용자는 특수 하드웨어 없이도 인증서를 빠르게 확인할 수 있으며, 영지식은 제공자에게 사용자가 독점적인 가중치에 대해 아무것도 알 수 없음을 보장합니다. Anthropic은 '실패 증명(Proof-of-Failure)'의 예를 듭니다. 코드를 릴리스하기 전에 모델 제공자는 개발자에게 제공자가 특정 모델에 최소한 일정 수의 토큰을 소비했으며, 최소 100만 토큰 이상 시도한 후에도 패치에서 버그를 찾지 못하는 등 특정 결과를 달성하지 못했다는 증명을 제공할 수 있습니다.

과제 4: 모델 승인

규제는 제공자가 안전하다고 승인된 모델만 서비스하도록 요구할 수 있습니다. 위험한 모델이 경쟁사보다 우수한 성능을 보이거나 서비스 비용이 더 저렴할 수 있기 때문에 제공자는 이를 우회하려는 유인이 있을 수 있습니다. 규제 기관은 승인된 모델만 서비스되도록 보장할 방법이 필요합니다.

zkSNARK를 사용하면 규제 기관은 제공자가 승인된 모델의 사용을 강제하는 증명을 응답에 첨부하도록 요구할 수 있습니다. 증명은 각 요청을 사용된 모델에 묶으므로, 제공자가 승인되지 않은 모델을 사용하면 검증되지 않습니다. 규제 기관은 각 요청을 재실행하지 않고도 가벼운 방식으로 이를 확인할 수 있습니다.

Anthropic은 이 소프트웨어 전용 암호학적 접근 방식을 제조업체가 변조 방지 하드웨어를 생산하는 것에 의존하는 하드웨어 기반 솔루션인 신뢰 실행 환경(trusted execution environments)과 대조합니다. Anthropic은 신뢰할 수 있는 하드웨어와 암호학이 서로 다른 보장과 트레이드오프를 가진 상호 보완적인 접근 방식이며, 둘 다 역할을 할 것이라고 말합니다.

FlashProve의 작동 방식

FlashProve는 대규모 전문가 혼합 언어 모델의 증명 가능 추론을 위한 시스템입니다. 여기에는 증명자로서의 모델 제공자와 검증자로서의 사용자가 참여합니다. 프로토콜은 두 단계로 구성됩니다.

오프라인 단계에서 증명자는 모델 가중치에 대한 커밋을 게시합니다. 커밋은 가중치가 숨겨진 상태에서 정확한 가중치 선택을 고정하는 짧은 지문입니다. 이후의 추론 주장은 해당 커밋에 대해 확인됩니다.

온라인 단계에서 증명자는 요청(프롬프트 및 해당 출력 토큰)을 수신하고, '커밋된 모델이 평가될 때 이 출력 토큰을 생성한다'는 문장을 증명하는 증명 파일을 생성합니다. 커밋, 프롬프트 및 응답을 가진 사람은 누구나 가중치 없이 제한된 컴퓨팅 자원으로 증명을 확인할 수 있습니다.

증명 시스템은 네 가지 관련 속성을 가집니다. 완전성(Completeness)은 정직한 증명자의 증명이 검증자에 의해 수락됨을 의미합니다. 건전성(Soundness)은 거짓 문장에 대한 유효한 증명을 생성하는 것이 사실상 불가능하여 검증자가 증명자를 신뢰할 필요가 없음을 의미합니다. 영지식(Zero-knowledge)은 검증자가 가중치, 중간 계산 값 또는 각 레이어에서 어떤 전문가가 실행되었는지에 대해 아무것도 알 수 없음을 의미합니다(가중치를 제외한 모델 아키텍처는 숨겨지지 않음). 간결성(Succinctness)은 증명이 작고 확인하기 저렴함을 의미합니다. 증명된 계산은 H100 GPU에서 400B 파라미터 모델(양자화 버전의 경우 약 232GB)을 실행하는 것이지만, 검증자는 24코어 CPU에서 수 초 내에 확인 가능한 약 19MB의 증명 파일을 수신합니다.

Llama 4 Maverick에서의 성능

Anthropic은 공개적으로 사용 가능한 4비트 가중치를 사용하여 토큰당 약 17B 파라미터가 사용되는 400B 파라미터 전문가 혼합 모델인 Llama 4 Maverick에서 구현을 평가했습니다. 각 검증자 요청은 1,024 토큰의 윈도우이며, 각 증명은 하나의 토큰을 확인합니다. 증명자는 단일 H100과 24개의 CPU 코어가 있는 서버에서 실행되며, 검증자는 CPU에서 실행됩니다.

오프라인 단계는 모델당 한 번 실행되며 약 39분이 소요됩니다. 기술 보고서에서 논의된 기술적 이유로 인해 결과 커밋은 약 1,600만 건의 요청에 유효하며, 그 이후에는 제공자가 다시 커밋해야 합니다. 24개 요청 배치에 대한 온라인 단계는 증명자에게 약 223초가 소요되며, 이는 초당 110 토큰에 해당하고 각 증명은 18.78MB입니다.

검증자는 GPU가 필요 없으며 가중치에 대한 커밋에만 액세스할 수 있습니다. 클라이언트는 총 약 6.5MB의 커밋을 다운로드한 다음 요청당 하나의 증명을 다운로드합니다. 증명을 확인하는 데는 오프라인 단계의 확인을 포함하여 24개 스레드에서 17초, 단일 스레드에서 21초가 소요됩니다.

Anthropic은 이를 8개의 H100에서 동일 모델의 FP8 릴리스를 사용하는 널리 사용되는 추론 엔진인 vLLM을 사용한 일반 추론과 비교합니다. GPU당 24개 요청 배치를 증명하는 것은 vLLM이 동일한 24개 요청을 한 번에 처리하는 데 걸리는 시간보다 약 72배 더 오래 걸리며(실행 전반에 걸쳐 66~77배 범위), Anthropic이 시도한 가장 높은 부하에서 vLLM이 실행될 때보다 약 94배 더 오래 걸립니다.

FlashProve를 실용적으로 만드는 엔지니어링 선택

FlashProve는 증명 비용을 관리 가능한 수준으로 유지하기 위해 여러 아키텍처 결정을 사용합니다. 증명자의 작업은 실제로 실행된 전문가에 비례합니다. 전문가 혼합 모델에서 토큰은 400B 파라미터 중 약 17B를 사용하므로, 토큰당 증명자의 작업은 모든 파라미터가 아닌 해당 17B에 비례하며, 증명은 여전히 어떤 전문가가 선택되었는지 숨깁니다.

요청은 사후에 배치로 증명됩니다. 증명자는 프리필(prefill)에서와 같이 한 번의 병렬 패스로 완료된 텍스트를 읽고, 요청당 한 번이 아니라 배치당 한 번 가중치 커밋을 엽니다.

이 시스템은 단일 GPU에 맞도록 설계되었습니다. 각 레이어의 모델 가중치는 세그먼트로 분할되어 한 번에 한 레이어 세그먼트씩 증명됩니다. 가중치는 일반 메모리에 보관되고 스트리밍되므로, 옆에 약 290GB의 호스트 메모리가 있는 단일 80GB GPU면 충분합니다.

Anthropic은 또한 인라인 증명(in-line proving)과 사후 증명(post-hoc proving)을 구분합니다. 인라인 증명은 추론과 함께 발생하며 매우 빠를 것으로 예상되지만 효율성을 위해 보안을 희생할 수 있습니다. 사후 증명은 사후에 토큰의 하위 집합에 대해 발생하며 해당 트레이드오프 없이 더 느릴 수 있습니다. FlashProve는 사후 접근 방식을 따릅니다. Anthropic은 재계산의 복잡성 추가, 트래픽에 대한 보장을 얻는 데 지연, 고유한 비결정론과 같은 사후 증명의 한계를 지적합니다.

암호학적 구성

FlashProve는 이더리움의 레이어-2 네트워크와 같은 피어 투 피어 시스템에 배포된 종류의 zkSNARK를 사용합니다. Anthropic은 zkSNARK가 잘 확립된 레시피를 따른다고 말합니다. 대화형 오라클 증명(IOP)이라는 기본 정보 이론 객체가 해시 함수를 사용하여 암호학적 증명으로 컴파일되며, 이는 양자 내성 보안까지 제공합니다. IOP는 선형 제약 조건이 있는 코드 근접성 테스트와 룩업 논증을 포함한 최첨단 빌딩 블록으로 조립되며, 이는 코딩 이론과 복잡도 이론의 기술을 기반으로 합니다. Anthropic은 이러한 조각들을 추론을 위한 맞춤형 IOP로 결합하는 것을 섬세한 작업으로 설명하며 자세한 내용은 기술 보고서를 참조하라고 안내합니다.

Lean을 사용한 형식 검증

Anthropic은 형식 검증을 통해 암호학적 코드에 대한 신뢰 문제를 해결합니다. 팀은 Lean 증명 보조 도구를 사용하여 프로토콜과 원하는 보안 속성을 지정하고, 기계 검증 가능한 형태로 속성을 증명합니다. 세 가지 최상위 속성은 완전성, 건전성, 영지식입니다. 이러한 속성은 해시 함수에 의존하는 암호학적 프로토콜을 분석하는 정보 이론적 방법인 랜덤 오라클 모델에서 명시됩니다.

Anthropic은 두 가지 남은 신뢰 격차를 식별합니다. 첫째, 형식 문장이 의도와 일치하는지 확인하기 위해 감사를 받아야 합니다. 이는 수동으로 수행해야 하지만, Anthropic은 증명을 감사하는 것보다 훨씬 덜 번거롭다고 말하며 이를 돕기 위한 대화형 시각화 도구를 제공합니다. 둘째, 실행 가능한 코드가 보안 속성이 증명된 형식적으로 정의된 프로토콜과 일치하는지 확인하기 위해 감사를 받아야 합니다.

감사 접근 방식은 속성에 따라 다릅니다. 건전성은 검증자에만 의존하므로 Anthropic은 C++ 검증자와 함께 실행 가능한 Lean 검증자를 제공합니다. Lean 검증자는 더 느리게 실행되지만, Lean은 건전성 정리의 검증자가 수락하는 것만 수락함을 증명합니다. C++ 검증자는 일상적인 도구입니다. 형식적인 보장은 없지만 Anthropic의 테스트에서 모든 증명에 대해 Lean 검증자와 일치합니다. 완전성은 정직한 증명자와 검증자를 가정하므로, Lean 검증자를 통해 팀은 표준 소프트웨어 테스트를 통해 정직한 증명자가 수락하는 증명을 생성한다는 확신을 얻을 수 있습니다. 영지식은 증명자에만 의존하지만, 증명자는 비용이 많이 들고 Lean 증명자를 실행하는 것은 비실용적입니다. Anthropic은 그 부분에 대한 시설을 제공하지 않으며 가중치를 숨기려는 모든 증명자가 Lean 증명자와의 동등성을 보장하기 위해 신중한 에이전트 또는 인간 보안 감사를 위한 충분한 자원을 가질 것으로 예상합니다.

Anthropic은 또한 Claude가 추론을 위한 zkSNARK 개선 사항을 생성했으며 기존 오픈 소스 시스템보다 훨씬 빠른 시스템을 구축했다고 말합니다. 게시물은 Claude가 최적화에는 능숙하지만 특히 크고 복잡한 시스템에서 평가하기 어려운 결정을 내리는 경우가 많으며, Anthropic은 주장된 보안 보장에 대해 Lean으로 감사 가능한 최상위 문장을 제공함으로써 이에 대응한다고 언급합니다.

FlashProve와 이전 작업 비교

Anthropic은 FlashProve를 구어체로 zkML이라고 불리는 작업 라인에 배치합니다. 초기 시스템은 작았습니다. 2017년 SafetyNets는 2개의 컨볼루션 레이어 MNIST CNN과 작은 완전 연결 음성 모델을 검증했습니다. 2021년 zkCNN은 1,500만 파라미터의 VGG-16에 도달하여 증명당 88.3초를 기록했습니다. 2022년 Kang 등은 전체 해상도 ImageNet에서 MobileNet v2를 증명했습니다.

트랜스포머 증명이 뒤를 이었습니다. ZKML의 GPT-2는 1억 1,700만 파라미터에 대해 토큰당 약 159초(초당 약 0.006 토큰)가 소요되었습니다. Modulus Labs의 15억 파라미터 GPT-2 XL은 90시간 이상이 필요했습니다. 2024년 zkLLM은 GPU에서 약 15분 만에 2,048 토큰 입력에 대해 LLaMA-2-13B를 증명했는데, Anthropic은 이를 새로운 토큰당 약 0.001 토큰/초 또는 배치에서 약 2.5 토큰/초로 설명합니다. 2025년 zkGPT는 GPT-2를 21.8초(초당 약 0.05 토큰)로 줄였습니다. zkPyTorch는 단일 CPU 코어에서 토큰당 약 150초(초당 약 0.007 토큰)로 Llama-3 8B를 증명했습니다. ZKTorch는 약 20분(초당 약 0.001 토큰) 만에 GPT-J 6B를 증명했습니다. VerInf는 FlashProve가 타겟팅하는 동일한 400B 파라미터 전문가 혼합 모델인 Llama 4 Maverick을 초당 약 0.02 토큰으로 증명했습니다. Anthropic이 현재 동료 검토를 거친 최첨단 기술이라고 부르는 DeepProve는 단일 포워드 패스로 전체 생성 시퀀스를 인증하며 한 대의 머신에서 GPT-2의 경우 초당 약 2.9 토큰, Gemma 3의 경우 초당 1.4 토큰에 도달하고 분산 환경에서는 초당 31 토큰에 도달합니다.

Anthropic은 상업적 노력도 언급합니다. Attestable는 단일 H100에서 초당 53~77 토큰으로 Gemma 4 31B를 증명했다고 보고했습니다. 이 글을 쓰는 시점에서 Attestable는 해당 오픈 소스 라이브러리를 릴리스하지 않았습니다.

Anthropic은 발전의 규모를 강조합니다. 2024년 zkLLM은 단일 A100에서 초당 약 2.5 토큰으로 13B 모델을 증명했습니다. Anthropic이 알고 있는 Llama 4 Maverick의 유일한 이전 증명인 VerInf는 DGX Spark에서 1,000 토큰에 14.3시간이 소요되었으며, 검증하는 데 거의 하루가 걸리는 93.6GB 증명을 보고했습니다. FlashProve는 단일 H100에서 초당 110 토큰으로 동일한 모델을 증명하며, 수 초 내에 검증 가능한 19MB 증명을 사용합니다. Anthropic은 이러한 발전이 더 많은 모델과 아키텍처로 이전되어 네이티브 계산 대비 약 2자리수(측정 결과 약 70~95배)의 오버헤드를 산출할 것이며, 이는 이전에 예상했던 것보다 훨씬 적다고 믿습니다.

Anthropic이 문서화한 한계

Anthropic은 몇 가지 기술적 한계를 나열합니다. 첫째, 빠른 실행 코드에 대한 형식적인 보장이 없습니다. Anthropic은 실행 가능한 느린 Lean 검증자를 포함하여 프로토콜의 Lean 구현을 제공하며, Lean에서 증명된 보안 속성을 함께 제공합니다. 논문과 빠른 실행 코드는 Lean 프로토콜에서 파생되었지만, Anthropic은 Lean, 논문, 코드 세 가지가 모두 일치한다고 보장하지 않습니다.

둘째, 증명은 탐욕적 디코딩(greedy decoding) 하의 정수 모델에 대한 것입니다. Anthropic은 게시된 가중치의 정확한 정수 버전을 증명하며, 증명은 확인된 각 토큰이 해당 모델의 탐욕적 선택임을 주장합니다. 부동 소수점 구현이나 샘플링 디코딩의 응답은 특정 위치에서 벗어나 증명된 계산과 더 이상 정확히 일치하지 않을 수 있습니다. 정수 버전은 일반적으로 부동 소수점 계산의 비결정론을 고려하더라도 실제 부동 소수점 추론의 작은 오차 범위 내에 있을 것으로 예상되고 경험적으로 테스트되었지만, 이는 적대적으로 설계된 프롬프트까지 다루지는 않습니다.

셋째, 아키텍처 숨기기는 목표가 아닙니다. 이 시스템은 서비스되는 모델이 전문가 혼합 아키텍처를 사용한다고 가정합니다. 여기서 각 트랜스포머 레이어의 피드 포워드 블록은 여러 전문가 서브 네트워크로 대체되고 라우터는 토큰당 소수의 전문가만 활성화합니다. FlashProve는 효율성 향상을 위해 MoE 구조를 사용합니다. 밀집 모델(dense models)과 같은 다른 아키텍처도 널리 사용되며, 그 설명에는 제공자가 비밀로 유지하려는 지적 재산이 포함될 수 있습니다. Anthropic은 검증자가 커밋된 모델에서 커밋된 실행 파일의 실행을 확인하는 숨김 커밋(hiding commitment)을 통해 가중치와 아키텍처를 모두 커밋함으로써 아키텍처도 숨기는 시스템을 상상할 수 있다고 언급합니다.

넷째, 사이드 채널 공격은 범위 밖입니다. 프로토콜은 증명 자체가 커밋된 모델의 가중치에 대해 아무것도 드러내지 않음을 보장하지만, 증명 생성 시간 측정과 같은 사이드 채널은 잠재적으로 가중치에 대한 정보를 드러낼 수 있습니다. Anthropic은 이를 이번 릴리스의 범위 밖으로 간주합니다.

다섯째, 이 시스템은 현재 최대 1,024 토큰의 컨텍스트에 대해 추론을 증명합니다. Anthropic은 이것이 채팅 설정에서 누적된 컨텍스트에 비해 짧다고 지적하며, 이상적인 것은 컨텍스트 길이를 수십만에서 수백만 토큰의 컨텍스트 윈도우를 정기적으로 가지는 프론티어 모델의 전체 컨텍스트 윈도우로 늘리는 것이라고 말합니다.

릴리스가 시사하는 바

FlashProve는 프로덕션 증명 가능 추론 서비스가 아닌 연구 프로토타입입니다. 그 중요성은 이전에는 오픈 시스템에서 도달할 수 없었던 규모와 속도로 소프트웨어 전용 암호학적 접근 방식을 입증했다는 점에 있습니다. Anthropic은 400B 파라미터 전문가 혼합 모델에서 19MB 증명과 초 단위 검증으로 초당 110 토큰을 보고했으며, 이는 수십 배 더 느리거나 훨씬 작은 모델로 제한되었던 이전 오픈 결과와 비교됩니다.

이 릴리스는 또한 AI 생성 암호학적 시스템을 더 감사 가능하게 만드는 패턴을 보여줍니다. 최상위 보안 문장에 대해 Lean에서 형식 검증을 사용하고, 빠른 검증자와 증명 가능하게 올바른 검증자를 모두 제공하며, 형식 문장, 논문 및 실행 코드 간의 남은 격차를 문서화하는 것입니다. Anthropic은 빠른 C++ 검증자가 형식적인 보장이 없으며 Lean, 논문 및 코드가 완전히 일치하지 않을 수 있다고 명시하므로, 형식 검증은 신뢰 가정을 줄이지만 제거하지는 않습니다.

AI 거버넌스의 경우, 게시물은 증명 가능 추론이 속도 조절 요구 사항, 변조 탐지, 텍스트 출처 및 모델 승인을 지원할 수 있다고 주장합니다. 또한 한계를 명확히 밝힙니다. 증명은 하드웨어가 주장된 모델을 서비스했음을 보여줄 수 있지만, 동일한 하드웨어가 뒤에서 훈련을 수행하지 않았음을 보여줄 수는 없습니다. 증명은 가중치를 숨기지만 아키텍처는 숨기지 않으며, 현재 시스템은 최대 1,024 토큰의 컨텍스트를 처리합니다. 이러한 한계는 유망한 프로토타입과 배포 가능한 규정 준수 또는 보안 메커니즘 사이의 격차를 정의합니다.