What are the Right Symmetries for Formal Theorem Proving?
作者: Krzysztof Olejniczak, Radoslav Dimitrov, Xingyue Huang, Bernardo Cuenca Grau, Jinwoo Kim, İsmail İlkan Ceylan
分类: cs.LG, cs.AI, cs.LO
发布日期: 2026-05-21
💡 一句话要点
提出重写范畴框架，提升LLM在形式化定理证明中的对称性与鲁棒性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化定理证明 大型语言模型 对称性 重写范畴 测试时聚合
📋 核心要点
- 现有基于LLM的定理证明器对问题表示的微小变化过于敏感，缺乏对数学结构对称性的有效利用。
- 论文提出重写范畴框架，形式化证明等变性和成功不变性，并设计测试时聚合方法来提升对称性。
- 实验表明，所提出的测试时聚合方法能够提高LLM定理证明器的鲁棒性和性能，验证了对称性的重要性。
📝 摘要（中文）
基于大型语言模型（LLM）的形式化定理证明器对问题表示中的表面变化高度敏感，语义等价的陈述可能表现出截然不同的证明成功率，这揭示了其未能尊重形式数学中固有的结构对称性。本文旨在回答一个核心问题：形式化定理证明的正确对称性是什么？我们引入了重写范畴，这是一个范畴论框架，用于捕获由证明策略引起的组合的、通常是非可逆的变换，并用它来形式化两个对称性概念：证明等变性（governing how proof distributions transform under rewrites）和成功不变性（即，成功概率的不变性），要求等价的陈述以相同的概率被解决。我们观察到，基于状态的next-tactic证明器通过对证明状态进行操作，自然地满足证明等变性。相比之下，最先进的基于LLM的证明器既不满足证明等变性也不满足成功不变性，在等价公式中表现出很大的性能变化。为了缓解这种情况，我们提出了测试时方法，该方法聚合输入的等价重写，从理论上表明它们在采样极限中恢复成功不变性，并且在经验上表明它们在固定的推理预算下提高了鲁棒性和性能。我们的结果强调了对称性是基于LLM的定理证明中一个关键的缺失归纳偏差，并表明测试时计算是近似它的一个实用途径。
🔬 方法详解
问题定义：现有基于大型语言模型的定理证明器在面对语义等价但表达形式不同的问题时，表现出显著的性能差异。这种现象表明，这些模型未能充分利用形式数学中固有的对称性，导致其鲁棒性较差。因此，论文旨在解决如何使LLM更好地利用对称性，从而提高定理证明的性能和鲁棒性的问题。
核心思路：论文的核心思路是形式化定理证明中的对称性概念，并设计方法使LLM能够更好地利用这些对称性。具体来说，论文引入了“重写范畴”的概念，用于描述证明过程中各种策略所产生的变换。基于此，论文定义了“证明等变性”和“成功不变性”两种对称性，并提出通过测试时聚合等价重写来近似满足这些对称性。
技术框架：论文的技术框架主要包括以下几个部分：1) 引入重写范畴，用于形式化证明策略的变换；2) 定义证明等变性和成功不变性两种对称性；3) 提出测试时聚合方法，通过对输入的等价重写进行聚合，来近似满足成功不变性。整体流程是，首先分析现有LLM证明器不满足对称性的原因，然后设计方法来缓解这个问题，最后通过实验验证方法的有效性。
关键创新：论文最重要的技术创新点在于形式化了定理证明中的对称性概念，并提出了相应的测试时聚合方法。与现有方法相比，该方法不是直接训练模型来学习对称性，而是通过在测试时对等价重写进行聚合，来近似满足对称性。这种方法更加灵活，并且可以应用于各种不同的LLM证明器。
关键设计：测试时聚合方法的关键在于如何生成输入的等价重写。论文中并没有详细说明如何生成这些重写，这部分可能依赖于具体的定理证明环境和可用的策略。此外，如何有效地聚合这些重写的结果也是一个关键问题，论文中可能使用了简单的平均或者投票等方法。
🖼️ 关键图片
📊 实验亮点
实验结果表明，所提出的测试时聚合方法能够显著提高LLM定理证明器的性能。具体来说，该方法在固定推理预算下提高了证明成功率，并增强了模型对问题表示变化的鲁棒性。这些结果验证了对称性在LLM定理证明中的重要性，并表明测试时计算是近似对称性的有效途径。
🎯 应用场景
该研究成果可应用于提升形式化验证、程序验证、数学推理等领域中基于LLM的自动化工具的性能和可靠性。通过提高LLM对问题表示的鲁棒性，可以减少人工干预，加速定理证明过程，并有望在软件安全、人工智能安全等关键领域发挥重要作用。
📄 摘要（原文）
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.