論文の概要: What are the Right Symmetries for Formal Theorem Proving?

• arxiv url: http://arxiv.org/abs/2605.22257v1
• Date: Thu, 21 May 2026 10:00:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-22 16:35:42.199655
• Title: What are the Right Symmetries for Formal Theorem Proving?
• Title（参考訳）: 形式理論の正しい対称性は何か?
• Authors: Krzysztof Olejniczak, Radoslav Dimitrov, Xingyue Huang, Bernardo Cuenca Grau, Jinwoo Kim, İsmail İlkan Ceylan,
• Abstract要約: 意味論的に等価な文は、非常に異なる証明成功率を示すことを示す。 これは中心的な疑問を提起する: 形式的定理証明の適切な対称性は何か? 証明戦術によって誘導される構成的、一般的には非可逆な変換をキャプチャーするカテゴリ理論フレームワークである書字カテゴリを導入する。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 大言語モデル(LLM)に基づく形式的定理証明は、問題表現における表面的変動に非常に敏感である:意味論的に等価なステートメントは、形式数学に固有の構造的対称性を尊重するのに失敗することを明らかにする、劇的に異なる証明成功率を示す。 これは中心的な疑問を提起する: 形式的定理証明の適切な対称性は何か? 我々は、証明戦術によって引き起こされる構成的、一般的には非可逆変換をキャプチャするカテゴリ理論のフレームワークである書き換え圏を導入し、証明の同値性、証明分布が書き換えの下でどのように変換されるかの制御、成功確率の不変性、同じ確率で解決される同等の文を必要とする2つの対称性の概念を定式化する。 状態ベースの次戦術プローバーは証明状態の操作により自然に証明等価性を満足する。 対照的に、最先端のLLMベースのプローサはどちらの特性も満足せず、等価な定式化にまたがって大きな性能変化を示す。 そこで本研究では,入力の等価な書き直しを集約し,サンプリング限界のばらつきを再現し,固定された推論予算下での堅牢性と性能を向上する試験時間法を提案する。 本研究では, LLMに基づく定理の証明において, 対称性を欠落した帰納的バイアスとして強調し, 実測経路としてテスト時間計算を提案する。

関連論文リスト

• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness [7.694715050727414]
  大規模言語モデル(LLM)は数学的な問題解決に有効である。 ProofRankは、挑戦的な数学的競争から得られたベンチマークである。 正当性のみのベンチマークでは得られない証明品質にはかなりの違いがある。
  論文  参考訳（メタデータ） (2026-05-11T11:23:36Z)
• Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
  エージェント定理プロバーは、数学的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証とを結合したパイプラインである。 本稿では, 検証された証明に到達する有限水平成功確率として定義される分布的視点を提案し, 証明可能性を導入する。 本稿では,エージェント定理の証明者が実世界の偏りのある問題分布にいつ,なぜ成功するのかを,原理的かつコンポーネントに敏感に説明する。
  論文  参考訳（メタデータ） (2026-02-11T05:22:24Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Almost Equivariance via Lie Algebra Convolutions [0.0]
  ほぼ同値の定義を提供し、それをモデルで符号化する実践的な方法を与える。 具体的には、リー代数の畳み込みを定義し、それらがリー群畳み込みに対していくつかの利点を提供することを示す。 2つの存在定理を証明し、1つは多様体の等距離の有界距離におけるほぼ等距離の存在を示し、もう1つはヒルベルト空間の逆を示す。
  論文  参考訳（メタデータ） (2023-10-19T21:31:11Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  複雑なデータにおける説明的要素を遠ざけることは、データ効率の表現学習にとって有望なアプローチである。 論理的定義と量的指標の関連性を確立し, 理論的に根ざした絡み合いの指標を導出する。 本研究では,非交叉表現の異なる側面を分離することにより,提案手法の有効性を実証的に実証する。
  論文  参考訳（メタデータ） (2023-05-19T08:22:23Z)
• Evaluating the Robustness of Interpretability Methods through Explanation Invariance and Equivariance [72.50214227616728]
  解釈可能性法は、それらの説明が説明されたモデルを忠実に記述した場合にのみ有用である。 特定の対称性群の下で予測が不変であるニューラルネットワークを考える。
  論文  参考訳（メタデータ） (2023-04-13T17:59:03Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。