形式定理证明的正确对称性是什么？
机器学习
2026-05-22 v1 人工智能
计算机科学中的逻辑
摘要
基于大型语言模型（LLM）的形式定理证明器对问题表示的细微变体极其敏感：语义等价的陈述在证明成功率上可能呈现巨大差异，暴露出其未能尊重形式数学中固有结构对称性。这引出一个核心问题：形式定理证明的正确对称性是什么？我们引入范畴论框架——重写范畴（rewriting categories），以捕捉由证明策略所产生的组合式、通常不可逆的转换，并用其来形式化两种对称性概念：证明等价性（proof equivariance），规定证明分布在重写作用下的变换方式；成功不变性（success invariance，即成功概率的不变性），要求等价陈述的求解概率相同。我们观察到，基于状态的下一个战术证明器天然满足证明等价性，因为其针对证明状态进行操作。相比之下，最先进的LLM-based证明器既不满足证明等价性，也不满足成功不变性，在等价表述之间显示出显著的性能差异。为缓解这一问题，我们提出在测试时聚合等价重写的输入，理论上表明此方法在抽样极限下可恢复成功不变性，实证上则在固定推理预算下提高鲁棒性和性能。我们的结果表明，对称性是LLM-based定理证明中缺失的关键归纳偏置，测试时计算是实现近似对称性的实用途径。
引用
@article{arxiv.2605.22257,
title = {What are the Right Symmetries for Formal Theorem Proving?},
author = {Krzysztof Olejniczak and Radoslav Dimitrov and Xingyue Huang and Bernardo Cuenca Grau and Jinwoo Kim and İsmail İlkan Ceylan},
journal= {arXiv preprint arXiv:2605.22257},
year = {2026}
}