What was already known
Earlier verifiable-inference systems covered smaller networks or incurred much larger proving and verification costs. The authors compare with zkLLM and VerInf, but those experiments use different models, hardware and proof scopes, so their figures do not establish a controlled speedup factor.
AI involvement
The named research team credits Claude with novel applications of cryptographic tools and with building the improved inference-proof system. AI agents produced the protocol paper and translated Lean representations into executable prover and verifier code. Humans led the project, chose the evaluation and reviewed the top-level statements; the release does not establish task-only autonomy.
- Rinberg and colleagues: FlashProve technical report — Executive summary; formalization and limitations
- Anthropic: Progress on provable inference — Executive summary; formalization and limitations
Importance
A new open protocol and implementation make cryptographic checking of a full-size mixture-of-experts model substantially more practical in the reported setting. The result concerns proof generation for a specified computation; it does not certify the truth of a model’s answers.
Technical verification
The authors report Lean proofs of protocol security and a sound executable Lean verifier, plus implementation tests and benchmarks. Those checks cover a narrower formal protocol: batched zero knowledge and equivalence of the fast C++ verifier and GPU prover to that protocol remain unproved. The complete implemented performance and security claim therefore has Partial verification.
Formal checking
The authors report Lean proofs of protocol security and a sound executable Lean verifier, plus implementation tests and benchmarks. Those checks cover a narrower formal protocol: batched zero knowledge and equivalence of the fast C++ verifier and GPU prover to that protocol remain unproved. The complete implemented performance and security claim therefore has Partial verification.
- Checker
- FlashProve team using Lean 4
- Scope
- Formal protocol and executable Lean verifier under the stated random-oracle, setup and request conditions
- Basis
- Reported by the linked checker
Human understanding
Few is the default when evidence for a higher level is insufficient. The authors explain the system and its cryptographic building blocks, but say the AI-generated protocol paper has not been reviewed in detail. A named human explanation of the full central protocol is not established, so Few is the evidence default.
Correction and publication history
New source-reviewed AI-centered cryptographic inference protocol and benchmark, with partial checking and explicit formal-model limits.
Read this published revision