compute-verification/verity
Developer toolsこのページは AI により自動翻訳されています。技術的な詳細は原文をご確認ください。 原文を見る
verifying compute
概要
Verity is a system for verifying how AI datacenters are being used. It aims for security in extremely adversarial settings: the intended application is enforcing an international agreement to deliberately pace AI development. At a high level, it is a streaming interactive protocol between a developer and an auditor, in which the developer maintains private records of the computations it performs in its datacenters and continuously proves that these records have certain properties, which we have chosen as proxies for the following idealized properties: - the records accurately and comprehensively reflect the developer's actual computations. - the records reflect only having performed inference, not training. The developer represents its computations as Boolean circuits, which capture their numerical semantics down to the silicon level (though the logical circuit need not exactly match the structure of the physical circuit).
README
以下は原文 README の抜粋です。原文を見る。
[quick overview written by Claude…]
Verity
Verity lets an AI developer prove to an auditor what its datacenter’s hardware computed, so that the auditor can bound
how much the developer could have trained in secret. It is for developers who must show what their hardware ran without
revealing their models or data, since every proof is zero-knowledge, and for the auditors who check those proofs. It has
two composite protocols: onsite, for an auditor with devices at the datacenter, and remote, for an auditor with none.
Start with the remote protocol in verity/core/protocols/remote/, then ARCHITECTURE.md.
- ARCHITECTURE.md: what Verity bounds and how, the design’s layers and the Glossary.
- GLOSSARY.md: the notation every guarantee is stated in, and the older names it replaces.
Security/: the guarantees, in Lean.Security/Definitions/states them and their named assumptions,Security/Proofs/proves them, and a guarantee whose proof isn’t there is open.- AGENTS.md: the code’s layout and rules, for contributors and their agents.
Subprotocols
Each subprotocol proves one kind of claim about what the developer’s hardware did. Its Lean is its definition; where a Python verifier still decides, a difftest holds it to the Lean until the Lean replaces it.
| Subprotocol | What an accepted run establishes | Where |
|---|---|---|
| Sampled proofs | The auditor samples proof blocks of a committed circuit with live coins, and C-Flock proves each sampled proof block’s values in the committed trace right. The result bounds how many proof blocks are incorrect. | verity/core/protocols/sampled_proofs, C-Flock in verity/ml/flock |
| Proof of useful work (PoUW) | A credited size S of noised matrix products, at least (1 − ε)·S of their AND gates computed right. Dither is its no-fold design, stated over the ACCEL model of the accelerator. | verity/core/protocols/pouw, Dither |
| Proof of useful space (PoUS) | A lower bound on the bits a device’s memory held, from timed rounds the memory challenger runs and signs. | verity/core/protocols/pous |
| The bandwidth audit | A lower bound on the bits read from PoUS’s store. | verity/core/protocols/bandwidth |
| PoUB | The same, over a node’s registered store. | verity/core/protocols/remote_bandwidth |
| Network certification | An auditor-trusted device on each node’s uplink, the network certifier, certifies that the traffic carried only values in the committed trace, and bounds the bits that left the site. | verity/core/protocols/certifier |
推奨ツール
別のキーワードを試すか、フィルタを外してください。
インストール
npx skillfish add compute-verification/verity