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 proving lower bounds on 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 find that shorter proofs seem to require and provide more mechanistic understanding. Moreover, we find 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.

翻译：在本工作中，我们提出利用机制可解释性——将模型权重逆向工程为人类可解释算法的技术——来推导并简洁地证明模型性能的形式化保证。我们通过在Max-of-$K$任务上训练的151个小型Transformer模型上形式化证明其准确率下界，对该方法进行了原型验证。我们创建了102种不同的计算机辅助证明策略，并评估了它们在每个模型上的证明长度与边界紧致度。通过量化指标分析，我们发现较短的证明似乎需要且能提供更深入的机制理解。此外，我们发现更忠实的机制理解能产生更紧致的性能边界。我们通过定性分析部分证明验证了这些关联。最后，我们指出叠加的无结构噪声是利用机制可解释性生成简洁模型性能证明时面临的关键挑战。