Circuit Claims Depend on What Is Extracted and How It Is Compared

This paper argues that circuit extraction does not uniquely identify a model mechanism. In a synthetic Lean tactic-prediction benchmark with randomized proof surfaces, the authors vary the reported object, pruning criterion, and whether attention-head queries and keys are represented jointly or separately. Exact edge overlap between extracted circuits is low and can reach a random baseline. Two coarser summaries remain more stable: the selected attention-head set and the ranking of circuit sizes across conditions differing in which supervised checkpoint initializes reinforcement learning. The paper proposes explicit reporting requirements for circuit-extraction studies.