論文の概要: SemantEq: Faithful Bidirectional Equivalence of Formal Statements

• arxiv url: http://arxiv.org/abs/2610.32919v1
• Date: Fri, 23 Oct 2026 17:20:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 01:38:06.619069
• Title: SemantEq: Faithful Bidirectional Equivalence of Formal Statements
• Title（参考訳）: SemantEq: 形式的ステートメントの忠実な双方向等価性
• Abstract要約: ステートメントの自動形式化は、自然言語からLean 4のような証明アシスタントに数学を翻訳する。 プローバーが強くなるにつれて、正当性の重荷は証明からステートメント、すなわち形式的ステートメントがそのソースを忠実に翻訳するかどうかへと移行する。 より原則化された関係であるSemantEqを紹介します。
• 参考スコア（独自算出の注目度）: 13.298690488679421
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Statement autoformalization translates mathematics from natural language into a proof assistant such as Lean 4, and models now do it at scale. As provers get stronger, the burden of correctness shifts from the proof to the statement, that is, to whether the formal statement faithfully translates its source. Given a trusted reference formalization, the natural test is logical equivalence, and it proves too much. $P \leftrightarrow Q$ holds trivially for any two statements $P$ and $Q$ that the library proves, because a prover can prove each separately and pass through $P \leftrightarrow \mathrm{True} \leftrightarrow Q$. The stronger the prover, the more unrelated pairs pass. Earlier methods restrict the prover and check that each proof names the other statement. We introduce SemantEq, a more principled relation that instead requires each statement to turn into the other only through a chain of allowed steps, such as logical rearrangement and rewriting with the library's own equations. Our programs judge a proof by the proof term Lean checks, not by its tactic script. SemantEq-Eval, a search without a model, reaches 100% precision and 65.6% recall on the ProofNetVerif test split under our adjudicated labels, against 95.8% and 61.8% for BEq+, and an 8.9-fold increase in its CPU time adds at most three pairs. A language model finds more proofs, but under two of four prompts it proves both directions of about two in five of the non-equivalent pairs. SemantEq-ProofAudit audits each model-written proof under a policy derived from the relation and accepts none of the 104 non-equivalent pairs, and it raises recall on 407 equivalent pairs from 65.4% to 81.1% under the best prompt. Separating the generation of equivalence proofs from their acceptance lets a stronger prover raise recall without changing what an acceptance means. We release code and data at: https://github.com/hlxr89/SemantEq
• Abstract（参考訳）: ステートメントの自動形式化は、自然言語からLean 4のような証明アシスタントに数学を変換します。 プローバーが強くなるにつれて、正当性の重荷は証明からステートメント、すなわち形式的ステートメントがそのソースを忠実に翻訳するかどうかへと移行する。 信頼された参照形式化が与えられたとき、自然検定は論理的同値であり、それが過剰に証明される。 証明者がそれぞれを別々に証明し、$P \leftrightarrow \mathrm{True} \leftrightarrow Q$を通すことができるからである。 証明者が強いほど、より関係のないペアが通過する。 以前のメソッドでは、証明者が制限され、各証明が他のステートメントを名付けることをチェックする。 より原則化された関係であるSemantEqを導入し、それぞれの文は論理的な再配置やライブラリ自身の方程式による書き換えなど、許容されるステップの連鎖を通じてのみ、もう一方に変換されるように要求する。 私たちのプログラムは、その戦術スクリプトではなく、リーンチェックという証明用語による証明を判断します。 SemantEq-Evalは100%精度に達し、ProofNetVerifテストは65.6%リコールされ、95.8%と61.8%がBEq+で、CPU時間は8.9倍に向上した。 言語モデルはより多くの証明を見つけ出すが、4つのプロンプトのうち2つでは、等価でないペアのうち5つに約2つの方向が示される。 SemantEq-ProofAuditは、関係から派生したポリシーの下で各モデルによる証明を監査し、104の非等価なペアのどれも受け入れず、最高のプロンプトで407の等価なペアを65.4%から81.1%にリコールする。 等価証明の生成を受容から切り離すことで、より強い証明者が受け入れの意味を変えることなくリコールを行うことができる。 https://github.com/hlxr89/SemantEq

関連論文リスト

• LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification [12.305232086450287]
  LeanPRMは、Leanの証明アシスタントを使用して、自然言語の証明のためのステップレベルのラベルを作成するフレームワークです。 LeanPRMでトレーニングされたQwen3-4B検証器は、同じベースモデルがRM800Kでトレーニングされた場合の60.3とは対照的に、48.2から74.7までの200の証明の保持されたセットに対して正確なステップラベルの精度を上げる。
  論文  参考訳（メタデータ） (2026-10-13T04:23:36Z)
• Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs [16.584143060150165]
  我々は,5つの条件を満たす形式的なリーン証明を生成する,エージェント的・オラクル誘導型証明探索であるPristisを紹介した。 その中核は、新しい忠実に保存される分割とコンカレント検索であり、これは orderDecompose という名前で呼ばれる。 ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。
  論文  参考訳（メタデータ） (2026-08-15T22:20:08Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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