論文の概要: The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

• arxiv url: http://arxiv.org/abs/2606.16541v1
• Date: Mon, 15 Jun 2026 10:45:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:34.461938
• Title: The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements
• Title（参考訳）: 信仰のギャップ--自然言語と形式的数学的ステートメントのセマンティック等価性を証明する
• Authors: Noor Islam S. Mohammad, Tamim Sheikh,
• Abstract要約: 形式的なステートメントは、型チェックと証明が可能でありながら、意図した元とは異なる定理を符号化することができる。 emphBidirectional Provability Fingerprinting (bpf) を導入する。 我々は6つのサブフィールドにわたる制御ドリフトラベルを持つ2,183ドルのNL/Lean4ペアのベンチマークであるDreatbenchをリリースした。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization, translating natural-language mathematics into formal proof assistants, is bottlenecked not by translation fluency but by \emph{faithfulness}: a formal statement can typecheck and be provable, yet still encode a different theorem than the source intended. We introduce \emph{Bidirectional Provability Fingerprinting} (\bpf{}), a framework that certifies faithfulness by characterizing each candidate through its forward and backward consequence neighborhoods in the ambient theory and matching these against probes derived from the natural-language statement. We further introduce four novel components: (i) \emph{Counterfactual Probe Generation} (\cpg{}), a contrastive procedure that synthesizes probes targeting specific drift directions; (ii) the \emph{Equivalence Spectrum}, a continuous faithfulness score that replaces brittle binary verdicts; (iii) \emph{Adaptive Probe Budget Allocation} (\apba{}), an information-theoretic budget router; and (iv) \emph{Faithfulness-Guided Decoding} (\fgd{}), which uses \bpf{} signals as a reward during autoformalization. We prove a \emph{drift detection theorem} and a \emph{PAC-faithfulness} result establishing that the equivalence class of a natural language statement is learnable from $\mathcal{O}(\log(1/δ)/\varepsilon)$ probes under mild assumptions. We release \driftbench{}, a benchmark of $2{,}183$ NL/Lean~4 pairs with controlled drift labels across six subfields of mathlib4. \bpf{}\,+\,\cpg{} detects $89.6\%$ of drifted formalizations at a $3.0\%$ false-positive rate-against $41.2\%$ for typecheck and $63.3\%$ for LLM-judge baselines, and \fgd{} reduces the rate at which a state-of-the-art autoformalizer emits drifted statements by $47\%$. https://pmlrbd.github.io/BPF/
• Abstract（参考訳）: 自然言語数学を形式的証明アシスタントに翻訳するオートフォーマル化は、翻訳流布ではなく、'emph{faithfulness} によってボトルネックとなる。 本稿では, 環境理論における各候補の前後の帰結近傍を特徴付けることによって, 自然言語文から導出したプローブに適合させることにより, 忠実性を証明したフレームワークである \emph{Bidirectional Provability Fingerprinting} (\bpf{}) を紹介する。 さらに4つの新しい要素を紹介します。 (i)特定のドリフト方向をターゲットとしたプローブを合成する対照的な手順であるemph{Counterfactual Probe Generation} (\cpg{}) (ii) 不安定な二項評定を置き換える連続忠実度スコアである「emph{Equivalence Spectrum}」 (iii)情報理論予算ルータであるemph{Adaptive Probe Budget Allocation} (\apba{}) (iv) \emph{Faithfulness-Guided Decoding} (\fgd{})。 自然言語文の同値類が、穏やかな仮定の下で$\mathcal{O}(\log(1/δ)/\varepsilon)$ probesから学習可能であることを示す。 6つのサブフィールドにまたがるドリフトラベルを持つ2,183$ NL/Lean~4ペアのベンチマークである \driftbench{} をリリースする。 bpf{}\,+\,\cpg{} は 89.6\% のドリフト形式を$3.0\% で検出し、型チェックは 41.2\% 、LCM-judge ベースラインは 63.3\% で、そして \fgd{} は、最先端のオートフォーマライザがドリフト式を出力するレートを 47\% で削減する。 https://pmlrbd.github.io/BPF/

関連論文リスト

• Subtle Injection for Ground-truth Inference of LLM Training Data [0.2538209532048867]
  SIGILは、認識不能なEmphcanary Sequenceを保護されたテキストとコードに埋め込むフレームワークである。 SIGILは、語彙規則、語彙句、構文、意味、コードパターンの5つのカナリア戦略を定義している。
  論文  参考訳（メタデータ） (2026-05-18T14:48:44Z)
• The Geometry of Forgetting: Temporal Knowledge Drift as an Independent Axis in LLM Representations [50.43168858368539]
  大規模言語モデルは自信を持って時代遅れの回答を生成し、既存の方法では検出できない。 これは工学的な失敗ではなく構造的な失敗であり、時間的ドリフトは、幾何的に残留流の方向として、正確性と不確実性の両方に符号化される。
  論文  参考訳（メタデータ） (2026-05-09T22:27:31Z)
• Structural Analysis of Directional qLDPC Codes [5.685589351789461]
  Gehér--Byfield--Ruban citeGeher2025Directional は量子低密度パリティチェック (qLDPC) 符号のハードウェア駆動型ファミリである。 これらの符号は、正方形またはヘックスグリッド接続上で固定エンフダイレクトワード(ルート)を実行するアンシラキュービットによって測定される安定化器によって定義される。
  論文  参考訳（メタデータ） (2026-02-22T05:59:57Z)
• Logical GANs: Adversarial Learning through Ehrenfeucht Fraisse Games [0.0]
  GANは区別不能を約束する、とロジックは説明する。 textbfLOGAN (LOGical GANs)は、識別器をdeep-k$Ehrenfeucht--Fra"iss'e (EF) emphOpponentとしてキャストする EFプローブシミュレータとMSOスタイルのグラフチェッカーである最小限のツールキットと、PyTorchによる実際の神経GANトレーニングを含む4つの実験を出荷しています。
  論文  参考訳（メタデータ） (2025-10-26T20:34:00Z)
• Reinforcement Learning with Verifiable yet Noisy Rewards under Imperfect Verifiers [90.50039419576807]
  RLVR(Reinforcement Learning with Verifiable Rewards)は、人為的なラベル付けを避けるために、自動検証に対するポリシーを訓練する。 認証ハッキングの脆弱性を軽減するため、多くのRLVRシステムはトレーニング中にバイナリ$0,1$の報酬を破棄する。 この選択にはコストがかかる:textitfalse negatives(正しい回答、FNを拒絶)とtextitfalse positives(間違った回答、FPを受け入れる)を導入する。
  論文  参考訳（メタデータ） (2025-10-01T13:56:44Z)
• 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)
• Sign Operator for Coping with Heavy-Tailed Noise in Non-Convex Optimization: High Probability Bounds Under $(L_0, L_1)$-Smoothness [74.18546828528298]
  SignSGD with Majority Votingは,Kappakappakappa-1right,Kappakappakappa-1right,Kappakappakappa-1right,Kappakappakappa-1right,Kappaka ppakappa-1right,Kappakappakappa-1right,Kappakappakappa-1right,Kappakappakappa-1right,Kappakappakappa -1right,Kappakappakappa-1right,Kappakappakappa-1right,Kappakappappapa-1right,Kappaを用いて,複雑性の全範囲で堅牢に動作することを示す。
  論文  参考訳（メタデータ） (2025-02-11T19:54:11Z)
• Efficiently stable presentations from error-correcting codes [5.69361786082969]
  線形誤り訂正符号から$mathbbZk$のプレゼンテーションを構築するための一般的な方法を提案する。 結果のプレゼンテーションは、コードがエフェクト可能なときの安定性が弱いことを観察する。 このことは一般には証明できないが、量子情報理論における非局所ゲームの研究において最近の結果を活用する。
  論文  参考訳（メタデータ） (2023-11-08T13:40:13Z)
• Provable Robustness of Adversarial Training for Learning Halfspaces with Noise [95.84614821570283]
  ラベル雑音の存在下での敵対的ロバストなハーフスペースの特性を分析する。 我々の知る限りでは、これは敵の訓練がノイズの分類子を与えることを示す最初の研究である。
  論文  参考訳（メタデータ） (2021-04-19T16:35:38Z)
• Proving Non-Inclusion of B\"uchi Automata based on Monte Carlo Sampling [19.09848789158933]
  B"uchiautoa non-inclusion $mathcalL(mathcalA) notsubseteq mathcalL(mathcalB)$を証明するための具体的なアルゴリズムを提案する。 $mathsfIMC2$は、B"uchiautoaのインクルージョンに対する反例を見つける高速で信頼性の高い方法である。
  論文  参考訳（メタデータ） (2020-07-05T10:17:02Z)

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

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