Safety Guarantees

Planned topics include formal verification, robustness certificates, provable guarantees for neural networks, runtime monitoring, and statistical versus worst-case guarantees.

Add lecture notes, readings, and transcripts here as the course progresses.

TorchLean — a Lean 4 framework for specifying, executing, and verifying neural networks. Its verification workflows include robustness bounds and checked certificates; the result applies to the model, input region, property, and trust assumptions that are explicitly represented.
TorchLean: Formalizing Neural Networks in Lean — the project paper, with examples in certified robustness, PINN residual bounds, and neural-controller verification.
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks — an early example of formal verification for neural networks.
AI Safety for Mathematicians — mathematical background and research context.
Fields–PrincInt postdoctoral research directions — includes formal verification methods for AI safety.
Chapter 3.3: Robustness and Chapter 4: Safety Engineering — supplementary context on robustness, risk analysis, and safety engineering.

Golden Gate Claude is a useful comparison with formal verification: Anthropic amplified an interpretable feature and observed a strong change in Claude's outputs. This demonstrates an intervention, but does not prove that a model satisfies a safety property across inputs or contexts. It was a 24-hour research demo and is no longer available.
Evaluating feature steering: A case study in mitigating social biases examines potential benefits and limitations of feature steering.