In this work, 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 lower bounding the accuracy of 151 small transformers
trained on a Max-of-$k$ task. 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 show that shorter proofs seem to require
and provide more mechanistic understanding, and that more faithful mechanistic
understanding leads to tighter performance bounds. We confirm these connections
by qualitatively examining a subset of our proofs. Finally, we identify
compounding structureless noise as a key challenge for using mechanistic
interpretability to generate compact proofs on model performance.

使用机制性可解释性推导和简明证明模型性能的形式保障，通过形式下界评估小型 Transformer 模型在 Max-of-k 任务上的准确率，并通过多种证明策略量化地展示了机制性理解与性能保障的紧密联系，最终确定了结构缺失噪声的叠加作为使用机制性可解释性生成简明证明的关键挑战。