Anthropic FlashProve: 증명 가능한 추론이 증명하는 것과 증명하지 못하는 것

2026년 11월 2일, Anthropic의 Frontier Red Team은 이 팀이 '증명 가능한 추론(provable inference)'이라고 부르는 것을 위한 오픈소스 시제품 FlashProve를 공개했습니다. AI 제공사가 모델 가중치를 보여 주지 않고도, 응답이 특정한 모델 가중치 한 세트에서 나왔음을 증명하는 방법입니다.¹ 제공사의 커밋먼트(commitment), 프롬프트, 응답을 가진 사람은 누구나 GPU 없이 일반 컴퓨터에서 몇 초 만에 증명을 확인할 수 있습니다.

시연은 매개변수 4,000억 개 규모의 Meta 오픈 웨이트 모델 Llama 4 Maverick에서 돌아갑니다. H100 GPU 한 대가 초당 약 110토큰의 속도로 증명을 만들고, 1,024토큰 요청 하나에 대한 증명은 약 19MB이며, 확인에는 약 17초가 걸립니다. Anthropic은 이번 공개를 "중간 진전이며 완성된 연구 과제가 아니다"라고 소개하고, 코드 저장소는 스스로를 유지 관리되지 않는 연구 산출물이라고 밝힙니다.³

아래에서는 증명 가능한 추론이 다루는 문제, FlashProve의 커밋·증명·검증 단계가 작동하는 방식, 드는 비용, 이전 시스템과의 비교, 증명이 정확히 무엇을 말하고 무엇을 말하지 않는지, 지금 실행해 볼 수 있는 것, 그리고 결과 뒤에 있는 AI 모델을 밝히는 연구 기록에 무엇이 달라질지를 정리합니다. 모든 출처는 2026년 11월 3일에 확인했습니다.

증명 가능한 추론은 어떤 문제를 푸나요?#

AI 모델에 프롬프트를 보내면 응답과, 서비스가 보여 주는 모델 이름을 보게 됩니다. 둘이 짝이 맞는지는 확인할 수 없습니다. Anthropic의 글은 이렇게 말합니다. "오늘날 모델에 질의하는 사용자는, 응답이 개발자가 응답하고 있다고 주장하는 바로 그 모델에서 나왔는지, 아니면 라우팅 서비스가 비용 때문에 몰래 바꿔 넣은 모델이나 심지어 토큰 스트림을 조작한 공격자가 바꿔 넣은 모델에서 나왔는지 확인할 수 없다."¹ 또 "모델이 고품질 응답을 내더라도 모델의 출력만으로 판단하는 것은 신뢰할 수 없다"고 합니다.

뻔한 확인 방법도 통하지 않습니다. 대부분의 프런티어 모델은 가중치가 비공개이고, 가중치가 있더라도 큰 모델을 다시 돌려 출력을 비교하려면 사용자는 물론 평가자도 거의 갖추지 못한 하드웨어가 필요합니다. 글의 표현으로 증명 가능한 추론의 목표는 "계산 자원이 제한되고 가중치에 대한 정보가 전혀 없는 사용자가, 응답이 요청한 모델에서 나왔음을 검증할 수 있게 하는 것"입니다.

글은 이것이 중요해질 상황 네 가지를 듭니다.

• 속도 조절(pacing). 제공사의 칩이 새 모델 학습이 아니라 모델 서비스에 쓰이기를 바라는 규제 기관은, 일정 기간에 처리한 요청을 포괄하는 증명을 요구할 수 있습니다. Anthropic은 그 한계를 직접 밝힙니다. 이것은 "하드웨어가 이를테면 옆에서 학습을 하고 있지 않다는 것까지 입증하지는 않는다".
• 변조 탐지. 추론 서버를 장악한 공격자나, 더 약한 모델인 척하는 더 강한 모델은 들키지 않으려면 예상되는 가중치에 대한 유효한 증명을 만들어 내야 하는데, 그럴 수 없습니다.
• 텍스트의 출처. 개발자가 소프트웨어 라이브러리를 프런티어 보안 모델로 검사했다고 말하거나, 회사가 어떤 계획을 특정 모델이 승인했다고 말하는 경우입니다. 글은 "채팅 로그를 공개하더라도 절대적인 보장은 되지 않는다"고 말합니다. 로그는 더 싸거나 성능이 떨어진 모델로 만들어졌을 수 있기 때문입니다.
• 모델 승인. 안전하다고 승인된 모델만 서비스할 수 있다는 규칙이 있다면, 응답마다 붙은 증명이 어느 모델이 답했는지 보여 줄 것입니다.

세 번째 경우가 연구에 가장 가깝습니다. 어떤 분석을 특정 모델로 했다고 적은 논문, 공개 진술, 기록은 지금으로서는 저자의 말일 뿐입니다.

이 작업은 공개된 목표에 대한 응답이기도 합니다. Anthropic의 Frontier Safety Roadmap은 2026년 9월 30일까지 "AI 모델 출력을 특정 모델 가중치 세트에 귀속시킬 수 있는 방식으로 신뢰성 있게, 증명 가능하게 '서명'하는 기법"의 시제품을 내놓겠다고 약속했습니다. 글에 따르면 Anthropic은 "우리의 추론 트래픽에 서명하고 신뢰할 수 있는 서버에서 추론을 다시 계산하는" 별도 프로젝트로 그 목표를 달성했고, FlashProve는 다른 방법으로 같은 목표를 추구합니다. 2026년 10월 19일 업데이트에서 이 목표는 '추론 검증(inference verification)'으로 이름이 바뀌었는데, 토큰 스트림에 대한 높은 보증은 "여러 방법으로 달성할 수 있기" 때문입니다.

FlashProve는 어떻게 작동하나요?#

FlashProve에는 제공사(증명자)와 사용자(검증자)라는 두 당사자가 있고, 두 단계에 확인을 더해 진행됩니다.¹

증명은 zkSNARK, 즉 영지식 간결 지식 논증(zero-knowledge succinct argument of knowledge)입니다. Anthropic은 네 가지 성질을 듭니다.

• 완전성. 정직한 증명자의 증명은 받아들여집니다.
• 건전성. "거짓 명제에 대한 유효한 증명을 만드는 것은 사실상 불가능하며(즉, 널리 믿어지는 암호학적 가정을 깨는 것과 맞먹는다), 따라서 검증자는 증명자를 믿을 필요가 없다."
• 영지식. 검증자는 "가중치, 계산의 중간값, 각 층에서 어느 전문가가 실행됐는지에 대해 아무것도 알지 못한다". 모델의 아키텍처는 숨겨지지 않습니다.
• 간결성. 양자화된 형태로 약 232GB인 모델의 실행을 약 19MB의 증명으로 몇 초 만에 확인합니다.

구성은 잘 알려진 방법을 따릅니다. 대화형 오라클 증명(interactive oracle proof)을 해시 함수로 하나의 증명 파일로 바꾸는 방식으로, Starknet 같은 이더리움 레이어 2 네트워크가 쓰는 증명 시스템과 같은 계열입니다. 기술 보고서는 이 방식이 해시 함수의 보안에 기대며, 그 덕분에 양자 컴퓨터에 대해서도 그럴듯한 보안을 갖춘다고 덧붙입니다.² 신뢰할 수 있는 하드웨어는 쓰지 않습니다. Anthropic은 자기가 실행한 것을 보증(attest)하는 칩인 신뢰 실행 환경(trusted execution environment)을 보완적인 접근으로 봅니다. 신뢰 실행 환경의 보장은 제조사에 기대지만, zkSNARK의 보장은 풀기가 사실상 불가능하다고 믿어지는 문제에 기댑니다.

속도의 일부는 모델 설계에서 나옵니다. Maverick은 전문가 혼합(mixture-of-experts) 모델입니다. 각 토큰은 몇 개의 전문가 하위 네트워크, 즉 매개변수 4,000억 개 가운데 약 170억 개만 거치며, 토큰당 FlashProve의 작업도 그것을 따라갑니다. 그러면서도 증명은 어느 전문가가 실행됐는지 숨깁니다. 증명기는 또 가중치를 일반 메모리에서 스트리밍하므로, 80GB GPU 한 대와 그 옆의 약 290GB 호스트 메모리면 충분합니다.

FlashProve는 얼마나 빠르고, 비용은 얼마나 드나요?#

Anthropic은 공개된 4비트 버전 가중치를 쓴 Llama 4 Maverick에서, 요청당 1,024토큰 창 하나로 FlashProve를 측정했습니다.¹

증명에는 응답을 서비스할 때보다 GPU 시간이 약 두 자릿수 크기(100배 규모) 더 듭니다. 이전 시스템에 필요했던 것보다 훨씬 적지만(다음 절), 여전히 서비스보다 훨씬 많습니다. Anthropic은 자신의 접근을, 서비스하는 모든 토큰을 그때그때 증명하는 것이 아니라 "토큰의 일부를 사후에 증명하는" 사후 증명(post-hoc proving)이라고 설명합니다. 기술 보고서는 그것이 무엇을 뜻하는지 분명히 말합니다. 사후 증명은 "사용자가 잘못된 응답을 받는 것을 막지 못하며, 변조가 탐지되도록 보장할 뿐이다".²

이전의 추론 증명과 비교하면 어떤가요?#

신경망이 올바르게 실행됐음을 증명하는 일에는 암호학에서 zkML이라는 이름이 있고, 아주 느린 결과들로 이루어진 짧은 역사가 있습니다. Anthropic의 글은 이를 다음과 같이 정리합니다.¹

가장 분명한 비교는 같은 모델에서 나옵니다. VerInf는 Maverick을 초당 약 0.02토큰으로 증명했고 증명은 93.6GB였습니다. FlashProve는 초당 약 110토큰으로 증명하며 증명은 19MB입니다. Anthropic의 결론은 "대략 두 자릿수 크기"인 증명 오버헤드가 "이전에 예상한 것보다 훨씬 작다"는 것, 그리고 이 진전이 "더 많은 모델과 아키텍처로 이어질 것"이라는 것입니다. 마지막 부분은 기대입니다. FlashProve는 모델 하나에서만 시연됐습니다.

FlashProve 증명은 무엇을 말하고, 무엇을 말하지 않나요?#

증명이 내세우는 명제는 일부러 좁습니다. "커밋된 모델을 실행하면 이 출력 토큰이 나온다."¹ 증명에 기대려는 사람에게는 속도만큼이나 한계가 중요합니다.

보여 주는 것. 커밋먼트 뒤의 가중치를 이 프롬프트로 실행하면 정확히 이 토큰들이 나온다는 것입니다. 엄밀히 말하면 증명은 공개된 가중치의 정확한 정수 버전에 관한 것이며, 확인된 각 토큰은 그 모델에서 가능성이 가장 높은 다음 토큰입니다. "증명은 탐욕적 디코딩(greedy decoding) 아래의 정수 모델에 관한 것이다." 저장소의 건전성 정리에 따르면 해시 질의를 q번 한 뒤 거짓 주장에 대한 증명이 받아들여질 확률은 최대 약 q/2^124 + 2^-101이며, Lean으로 작성된 검증기에 대해서는 Lean이 이 정리를 기계로 확인합니다.⁴

보여 주지 않는 것.

• 응답이 옳다는 것. 증명은 어떤 계산이 텍스트를 만들었는지에 관한 것이지, 텍스트가 참인지, 합리적인지, 안전한지에 관한 것이 아닙니다.
• 모델의 이름. 증명은 응답을 커밋먼트에, 커밋먼트를 가중치 한 세트에 묶습니다. 그 가중치가 어느 모델인지는 커밋먼트를 공개한 쪽이 말하는 것이고, 비공개 가중치라면 다른 누구도 들여다볼 수 없습니다.
• 샘플링이나 부동소수점으로 만든 응답. 모델은 보통 부동소수점으로, 샘플링을 써서 서비스됩니다. 그런 응답은 "어느 위치에서 갈라져 증명된 계산과 더는 정확히 일치하지 않을 수 있다". 정수 모델은 부동소수점 추론과 "작은 오류율 안에 있음을 경험적으로 시험했지만", "적대적으로 설계된 프롬프트까지 포괄하지는 않는다". 기술 보고서는 무해한 수치 잡음과 변조를 구별하는 통계적 방법을 제시합니다.²
• 긴 대화. 컨텍스트는 1,024토큰으로 제한되며, 이는 "채팅 환경에서 쌓이는 컨텍스트에 비하면 꽤 짧다".
• 하드웨어가 한 다른 모든 일. 앞서 짚었듯, 서비스에 대한 증명은 같은 칩이 학습도 하고 있지 않았다는 것을 보여 주지 않습니다.
• 아키텍처. 숨겨지는 것은 가중치뿐입니다.
• 시간 정보. "증명을 만드는 데 걸리는 시간을 재는 것 같은" 부채널 공격은 "이번 공개의 범위 밖"입니다.
• 빠른 코드가 곧 증명된 코드라는 것. Lean은 Lean 검증기의 건전성을 증명합니다. 사용자가 실행하는 C++ 검증기와 CUDA 증명기는 "같은 프로토콜을 따르도록 작성되었고 그 프로토콜에 맞춰 시험되었지만, 그 자체가 증명된 것은 아니다". 가중치를 숨기는 문제에 대해 저장소는 솔직합니다. "프로그램이 가중치를 숨긴다는 것은 우리가 아는 것이 아니라 기대하는 것이다."⁴

Anthropic은 FlashProve를 만드는 데 AI를 어떻게 썼나요?#

이번 공개는 AI가 어느 부분을 했는지 밝히는 AI 활용 연구의 사례이기도 합니다. 글은 "Claude가 추론용 zkSNARK의 개선을 만들어 냈다"고 말하고, 안전장치를 설명합니다. "Claude는 최적화에 능하지만, 특히 크고 복잡한 시스템에서 평가하기 어려운 결정을 자주 내린다. 우리는 주장하는 보안 보장에 대해 Lean(형식 검증 언어)으로 감사 가능한 최상위 명제를 제공하는 방식으로 이에 대응한다."¹

기술 보고서는 더 나아갑니다.²

• C++ 증명기와 검증기는 "AI 에이전트가 Lean 표현으로부터 얻어 낸 것"이며, "C++ 코드와 Lean 명세의 형식적 동등성은 증명되지 않았다".
• 저장소의 긴 프로토콜 설명은 "AI가 생성했으며, 우리는 이를 자세히 검토하지 않았다. 꼼꼼히 검토한 논문은 나중에 나올 것이다. 반면 이 보고서는 저자들이 직접 썼다".
• 형식 명제는 "사람이 직접, 그리고 AI 에이전트가 정확성을 확인했다. 전문가가 이를 독립적으로 감사하는 데 몇 시간 넘게 걸리지는 않을 것으로 예상한다".

저장소의 README에는 "Built to be run by an agent"(에이전트가 실행하도록 만들었다)라는 제목의 절이 있고, 코딩 에이전트에 줄 프롬프트가 들어 있습니다. 검증기를 빌드하고, 저장된 증명을 확인하고, 결과를 보고하고, 더 무거운 작업을 시작하기 전에는 먼저 물어보라는 내용입니다.³ 하버드 CMSA 보고서가 AI 활용 수학에 요구하는 종류의 '누가 무엇을 했는지' 진술입니다(하버드 CMSA 보고서의 권고 참고). AI의 몫, 사람의 몫, 그리고 독자가 여전히 확인해야 할 것입니다.

지금 FlashProve를 쓸 수 있나요?#

서비스로는 쓸 수 없습니다. 이번 공개에는 API가 없고, 증명기를 돌리는 사람이 직접 실행한 Llama 4 Maverick만 증명하며, Claude, ChatGPT, Gemini의 응답에 대한 증명은 만들지 않습니다. FlashProve는 Apache 2.0 라이선스의 코드로 버전은 0.16.0이며, "연구 산출물: 유지 관리하지 않으며 기여를 받지 않음"이라고 소개되어 있습니다.³ 모델 가중치는 공개물에 들어 있지 않습니다. 읽는 사람이 Meta의 라이선스에 따라 Hugging Face에서 Maverick을 직접 내려받아야 합니다.¹

저장소는 네 가지 경로를 설명합니다.

경로 1은 비용이 적게 들지만, 예시는 합성 가중치를 쓴 작은 모델입니다. 이 경로는 "검증기가 작동한다는 것만 보여 줄 뿐, 서비스되는 모델에 대해서는 아무것도 보여 주지 않는다". 실제 모델에 대해 무언가를 증명하려면 전용 H100과 수백 기가바이트의 메모리가 필요합니다. 자체 모델을 커밋하고 서비스하려는 제공사에게는 저장소의 서비스 안내와 운영자 의무 목록을 보라고 안내하는데, 이 목록은 "비밀로 유지해야 하는 가중치를 쓰기 전에 반드시 읽어야 할 문서"입니다.

연구 기록에는 무엇이 달라질까요?#

학술지와 연구비 지원 기관의 AI 정책은 저자에게 사용한 도구와 모델의 이름을 밝히라고 요구합니다(논문에 AI 사용을 표기하는 방법 참고). 그 이름은 진술일 뿐, 논문 안의 어떤 것도 독자가 그것을 확인하게 해 주지 않습니다. 현재 Papex의 연구 기록도 마찬가지입니다. 기록은 연구자나 연구자의 AI 앱이 보고한 AI 앱과 모델을 나열하며, Papex는 그 이름을 확인할 방법이 없으므로 자기 보고로 취급합니다.

추론 증명은 자신이 다루는 단계에 한해 이를 바꿀 수 있는 종류의 증거입니다. 제공사의 커밋먼트, 프롬프트, 응답, 증명은 모두 파일입니다. 기록과 함께 보관하면 누구든 몇 년 뒤에도 제공사나 기록 작성자를 믿지 않고 검증기를 다시 돌려 볼 수 있을 것입니다. 서명과 독립적인 타임스탬프는 누가 어떤 버전을 책임졌고 그 버전이 언제 존재했는지를 말해 줍니다. 추론 증명은 어떤 가중치가 특정 텍스트를 만들었는지를 말해 줄 것입니다.

그래도 범위는 좁을 것입니다. 증명은 어떤 가중치가 어떤 텍스트를 만들었는지를 보여 줄 뿐, 분석이 타당했는지, 사람이 확인했는지, 결과가 성립하는지는 보여 주지 않습니다. 그것은 여전히 사람의 몫입니다. 심사, 재현, 그리고 수학에서는 형식 증명입니다. 또 지금은 세 가지가 걸림돌입니다. AI 앱과 함께하는 연구 세션은 1,024토큰을 훨씬 넘고 샘플링을 씁니다. 대부분의 연구자가 쓰는 모델은 비공개이며, 아는 한 응답과 함께 이런 증명을 제공하는 비공개 모델 제공사는 없습니다. 그리고 증명에는 응답의 약 70~95배에 이르는 GPU 시간이 듭니다.

Anthropic 글의 한 아이디어는 과학의 관점에서 다시 볼 만합니다. 제공사가 개발자에게 "모델 제공사가 특정 모델에 적어도 X토큰을 썼으나 특정 결과에 이르지 못했다는 실패 증명(Proof-of-Failure)"을 줄 수 있다는 것입니다. 예를 들면 모델이 적어도 100만 토큰을 쓰고도 패치에서 버그를 찾지 못했다는 증명입니다.¹ 실패한 시도는 AI 에이전트가 보고에서 빼기 쉬운 것입니다(AI 연구 에이전트는 부정적 결과를 숨길까 참고). 효과가 없었던 시도를 확인할 수 있게 남긴 기록이 있다면 새로운 일일 것입니다.

주요 용어#

출처#

1. Anthropic (Frontier Red Team), Progress on provable inference for large language models (2026년 11월 2일), 2026년 11월 3일 확인 ↩ a b c d e f g h i
2. Roy Rinberg, Alex Allain, Alessandro Chiesa, Miranda Christ, Rahul Dalal, Giacomo Fenzi, Ben Mayer, Guy Weissenberg, FlashProve: an open-source library for provable inference, 기술 보고서 (2026년 11월), 23쪽, 2026년 11월 3일 확인 ↩ a b c d
3. GitHub의 anthropics/FlashProve, README (버전 0.16.0), 2026년 11월 3일 확인 ↩ a b c
4. FlashProve 안내서, What is proved, and of what, 2026년 11월 3일 확인 ↩ a b