What are the Right Symmetries for Formal Theorem Proving?

• URL: http://arxiv.org/abs/2605.22257v1
• Date: Thu, 21 May 2026 10:00:47 GMT
• Title: What are the Right Symmetries for Formal Theorem Proving?
• Abstract summary: We show that semantically equivalent statements can exhibit drastically different proof success rates.<n>This raises a central question: what are the right symmetries for formal theorem proving?<n>We introduce rewriting categories, a category-theoretic framework capturing the compositional, generally non-invertible transformations induced by proof tactics.
• Score: 23.981613344642152
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
  MathAdv is a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics.<n>We show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures.
  arXiv  Detail & Related papers  (2026-08-26T07:12:54Z)
• TREAT: Evaluating Access to Formal Knowledge across Equivalent Mathematical Representations [0.0]
  Key challenge is recognizing when an unfamiliar formulation denotes a known formal object.<n>Treat is a benchmark for evaluating whether large language models can recover known theorem identities.<n>Treat provides a controlled testbed for evaluating representation-robust access to formal knowledge.
  arXiv  Detail & Related papers  (2026-07-29T23:02:46Z)
• Aligning Network Equivariance with Data Symmetry: A Theoretical Framework and Adaptive Approach for Image Restoration [71.51826063983434]
  Image restoration is an inherently ill posed inverse problem.<n>We use non strict symmetry as a constraint to formulate the restoration inverse problem.<n>We show that the equivariance error of the optimal restoration operator is strictly bounded by the data symmetry error and the discretization mesh size.
  arXiv  Detail & Related papers  (2026-05-13T16:22:19Z)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness [7.694715050727414]
  Large language models (LLMs) have become capable mathematical problem-solvers.<n>We introduce ProofRank, a benchmark curated from challenging mathematical competitions.<n>We find substantial differences in proof quality that are not captured by correctness-only benchmarks.
  arXiv  Detail & Related papers  (2026-05-11T11:23:36Z)
• Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
  Agentic theorem provers are pipelines that couple a mathematical reasoning model with library retrieval, subgoal-decomposition/search planner, and a proof assistant verifier.<n>We propose a distributional viewpoint and introduce provability, defined as the finite-horizon success probability of reaching a verified proof.<n>We provide a principled, component-sensitive explanation of when and why agentic theorem provers succeed on biased real-world problem distributions.
  arXiv  Detail & Related papers  (2026-02-11T05:22:24Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Almost Equivariance via Lie Algebra Convolutions [0.0]
  We provide a definition of almost equivariance and give a practical method for encoding it in models. Specifically, we define Lie algebra convolutions and demonstrate that they offer several benefits over Lie group convolutions. We prove two existence theorems, one showing the existence of almost isometries within bounded distance of isometries of a manifold, and another showing the converse for Hilbert spaces.
  arXiv  Detail & Related papers  (2023-10-19T21:31:11Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  Disentangling the explanatory factors in complex data is a promising approach for data-efficient representation learning. We establish relationships between logical definitions and quantitative metrics to derive theoretically grounded disentanglement metrics. We empirically demonstrate the effectiveness of the proposed metrics by isolating different aspects of disentangled representations.
  arXiv  Detail & Related papers  (2023-05-19T08:22:23Z)
• Evaluating the Robustness of Interpretability Methods through Explanation Invariance and Equivariance [72.50214227616728]
  Interpretability methods are valuable only if their explanations faithfully describe the explained model. We consider neural networks whose predictions are invariant under a specific symmetry group.
  arXiv  Detail & Related papers  (2023-04-13T17:59:03Z)
• Causal Expectation-Maximisation [70.45873402967297]
  We show that causal inference is NP-hard even in models characterised by polytree-shaped graphs. We introduce the causal EM algorithm to reconstruct the uncertainty about the latent variables from data about categorical manifest variables. We argue that there appears to be an unnoticed limitation to the trending idea that counterfactual bounds can often be computed without knowledge of the structural equations.
  arXiv  Detail & Related papers  (2020-11-04T10:25:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.