形式定理证明的正确对称性是什么？

基于 大语言模型 (LLM) 的形式定理证明者对问题表示的表面变化高度敏感：语义上等价的陈述可以表现出截然不同的证明成功率，揭示出未能尊重形式数学固有的结构对称性。这就提出了一个核心问题：形式定理证明的正确对称性是什么？我们引入了重写类别，这是一个类别理论框架，捕获由证明策略引起的组合的、通常不可逆的变换，并用它来形式化两个对称概念：证明等变性，控制证明分布在重写下如何变换，以及成功不变性（即成功概率的不变性），要求以相同的概率求解等效语句。我们观察到基于状态的下一策略证明者通过对证明状态进行操作自然地满足证明等变性。相比之下，最先进的基于 LLM 的证明器不满足这两个属性，在等效公式中表现出巨大的性能差异。为了缓解这个问题，我们提出了对输入的等效重写进行聚合的测试时方法，从理论上表明它们在采样限制中恢复了成功的不变性，并且从经验上表明它们在固定推理预算下提高了鲁棒性和性能。我们的结果强调对称性是基于 LLM 的定理证明中一个关键缺失的归纳偏差，并建议将测试时间计算作为近似它的实用途径。