Compact Proofs of Model Performance via Mechanistic Interpretability

Understand

We propose using mechanistic interpretability -- techniques for reverse engineering model weights into human-interpretable algorithms -- to derive and compactly prove formal guarantees on model performance.

• We prototype this approach by formally proving accuracy lower bounds for a small transformer trained on Max-of-K, validating proof transferability across 151 random seeds and four values of K.
• We create 102 different computer-assisted proof strategies and assess their length and tightness of bound on each of our models.
• Using quantitative metrics, we find that shorter proofs seem to require and provide more mechanistic understanding.