2025/09/12 –, Plasma Stage 言語: English
Cryptography can’t tell us what is “good,” but it can provide verifiable ground truth about AI systems. Using tools like formal verification, zero-knowledge proofs, and verifiable computation, we can prove claims about what model ran, what guardrails executed, and how safety checks were enforced. This talk explores how cryptography can’t solve ethics, but can make AI behavior falsifiable, auditable, and accountable.
What does it mean for AI to be “safe”? Philosophy has wrestled with the problem of defining what is good or just for thousands of years, and cryptography cannot resolve that normative debate. But while it cannot decide ought, cryptography can help us establish reliable evidence about what AI systems did.
This talk explores how formal verification and cryptographic proofs can contribute to AI safety and interpretability. Formal verification can encode invariants and check that safety-critical guardrails or filters behave as specified. Zero-knowledge proofs and verifiable computation can ensure that an AI used the approved model version, applied required safety checks, and followed specified constraints—without exposing private data or proprietary model weights. Proof-carrying execution, enabled by recursive proofs, extends these guarantees to multi-step agents, letting us audit entire chains of reasoning or action.
The result is a “cryptographic safety wrapper”: a verifiable layer around AI systems that does not define moral truth, but that can make safety claims falsifiable, enforceable, and auditable. Drawing on Terence Tao’s ideas on machine-assisted proof, the talk argues that while philosophy continues to grapple with values, cryptography offers us a way to build shared ground truth about AI behavior—bridging the gap between ethics and engineering.
Ventali Tan is the founder of Lita, where she leads the development of Valida, a high-performance zero-knowledge virtual machine. She studied physics, philosophy, and computer science at Duke University and previously worked in venture capital and AI in San Francisco. Before Lita, she co-founded Delendum, a cryptography research lab. Her current interests include designing systems with zero-knowledge proofs and exploring how AI may extend our understanding of natural sciences.