Formal theorem provers based on large language models (LLMs) are highly sensitive to superficial variations in problem representation: semantically equivalent statements can exhibit drastically different proof success rates, revealing a failure to respect structural symmetries inherent in formal mathematics. This raises a central question: what are the right symmetries for formal theorem proving? We introduce rewriting categories, a category-theoretic framework capturing the compositional, generally non-invertible transformations induced by proof tactics, and use it to formalize two symmetry notions: proof equivariance, governing how proof distributions transform under rewrites, and success invariance (i.e., invariance of success probability), requiring equivalent statements to be solved with the same probability. We observe that state-based next-tactic provers naturally satisfy proof equivariance by operating on proof states. In contrast, state-of-the-art LLM-based provers satisfy neither property, exhibiting large performance variation across equivalent formulations. To mitigate this, we propose test-time methods that aggregate over equivalent rewritings of the input, showing theoretically that they recover success invariance in the sampling limit, and empirically, that they improve robustness and performance under fixed inference budgets. Our results highlight symmetry as a key missing inductive bias in LLM-based theorem proving and suggest test-time computation as a practical route to approximate it.

翻译：基于大语言模型的形式定理证明器对问题表示的表面变化高度敏感：语义等价的陈述可能表现出截然不同的证明成功率，这揭示了其未能尊重形式数学中固有的结构对称性。这引发了一个核心问题：形式定理证明的正确对称性是什么？我们引入重写范畴，这是一个范畴论框架，用于捕捉由证明策略引发的组合性、通常不可逆的变换，并以此形式化两种对称性概念：证明等变性，控制重写下证明分布的变换方式；以及成功不变性（即成功概率的不变性），要求等价陈述以相同概率被解决。我们观察到，基于状态的下一步策略证明器通过操作证明状态而自然满足证明等变性。相比之下，最先进的基于大语言模型的证明器既不满足任一性质，在不同等价表述之间表现出巨大的性能差异。为缓解此问题，我们提出测试时方法，对输入的等价重写进行聚合，理论上表明其在采样极限下恢复成功不变性，实证表明其在固定推理预算下提升鲁棒性和性能。我们的结果突显了对称性作为基于大语言模型的定理证明中缺失的关键归纳偏置，并指出测试时计算是近似该偏置的实用途径。