論文の概要: Surface Sensitivity in Lean 4 Autoformalization

• arxiv url: http://arxiv.org/abs/2604.23135v1
• Date: Sat, 25 Apr 2026 04:26:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 17:12:07.174067
• Title: Surface Sensitivity in Lean 4 Autoformalization
• Title（参考訳）: リーン4オートフォーマル化における表面感性
• Authors: William Feng, Ethan Lou, Aryan Sharma,
• Abstract要約: 観察されたパラフレーズの感度は,形式化が成功する間に意味的差異が生じるのではなく,コンパイル境界の障害を反映していることがわかった。 この結果から,今後のトレーニング時間の介入はセマンティック層ではなく,コンパイル境界を目標とすべきであることが示唆された。
• 参考スコア（独自算出の注目度）: 1.7855077077275565
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Natural-language variation poses a key challenge in Lean autoformalization: semantically equivalent paraphrases of the same theorem statements can induce divergent formal outputs, yet it remains unclear whether this variation reflects semantic disagreements or shallower failures. We investigate this question in Lean 4 using 60 deterministic paraphrase rules applied to ProofNet\# and miniF2F. Across four GPT-family models and three open-weight 7B autoformalizers, we find that the observed paraphrase sensitivity reflects compilation-boundary failures rather than semantic divergence among successful formalizations. In particular, when both baseline and perturbed outputs compile, paired predictions are semantically equivalent under BEq+ and structurally near-identical under GTED. By contrast, paraphrasing substantially affects whether outputs compile, with failure modes varying across datasets and perturbation classes. Our results suggest that future training-time interventions should target the compile boundary rather than the semantic layer, and that benchmarks should separate compile-conditional equivalence from surface consistency.
• Abstract（参考訳）: 同じ定理文の意味論的に等価なパラフレーズは、異なる形式的なアウトプットを誘導することができるが、このバリエーションが意味的不一致やより浅い失敗を反映しているかどうかは不明だ。 In this question in Lean 4 using 60 deterministic paraphrase rules applied to ProofNet\# and miniF2F。 4つのGPTファミリーモデルと3つのオープンウェイトな7Bオートフォーマライザで、観察されたパラフレーズ感度は、成功形式間の意味的差異よりも、コンパイル境界障害を反映していることがわかった。 特に、ベースラインと摂動出力の両方がコンパイルされると、ペア化された予測はBEq+の下で意味的に等価であり、GTEDでは構造的にほぼ同一である。 対照的に、パラフレーズ処理は、データセットや摂動クラスによって異なる障害モードで、アウトプットがコンパイルされるかどうかに大きく影響する。 この結果から,将来の訓練時間の介入はセマンティック層ではなくコンパイル境界を目標とすべきであり,ベンチマークはコンパイル条件の等価性を表面の整合性から分離すべきであることが示唆された。

関連論文リスト

• CausalFlip: A Benchmark for LLM Causal Judgment Beyond Semantic Matching [50.65932158912512]
  そこで我々は,新しい大言語モデルの開発を促進するために,因果推論ベンチマークCausalFlipを提案する。 CaulFlipは、イベントトリプル上に構築された因果判断の質問で構成されており、共同創設者、チェーン、コライダーの関係が異なっている。 回答のみのトレーニング,明示的なチェーン・オブ・ソート監視,そして内在型因果推論アプローチなどを含む,複数の訓練パラダイムによるLCMの評価を行った。
  論文  参考訳（メタデータ） (2026-02-23T18:06:15Z)
• Beyond Memorization: Testing LLM Reasoning on Unseen Theory of Computation Tasks [8.210112631285666]
  大規模言語モデル(LLM)は、形式的な言語タスクにおいて強力なパフォーマンスを示している。 正規言語を用いた決定論的有限オートマトン (DFA) 構築のためのベンチマークを導入する。 モデルが実際の質問に対して完璧に精度を達成し、タスクに対して84-90%を達成できることを示すが、その精度は目に見えない問題に対して急激に低下する。
  論文  参考訳（メタデータ） (2026-01-19T21:00:31Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Efficient semantic uncertainty quantification in language models via diversity-steered sampling [46.23327887393273]
  本稿では,デコード中に意味的に冗長な出力を回避できるダイバーシティステアリング・サンプリング手法を提案する。 主要なアイデアは、モデルの提案分布に連続的な意味-類似性ペナルティを注入することである。 モジュラーであり、ベースLSMへの勾配アクセスを必要としないため、このフレームワークは不確実性評価のためのドロップインエンハンスメントとして機能することを約束している。
  論文  参考訳（メタデータ） (2025-10-24T10:06:21Z)
• From Disagreement to Understanding: The Case for Ambiguity Detection in NLI [3.5164356851161984]
  このポジションペーパーでは、自然言語推論(NLI)におけるアノテーションの不一致は単なるノイズではなく、しばしば意味のある変化を反映していると主張している。 まず、あいまいな入力ペアを識別し、それらの型を分類し、次に推論に進む、あいまいさを意識したNLIへのシフトを呼びます。
  論文  参考訳（メタデータ） (2025-07-20T20:27:35Z)
• The Remarkable Robustness of LLMs: Stages of Inference? [5.346230590800585]
  本研究では,Large Language Models (LLM) の構造的介入に対するロバスト性について検討する。 驚くべきことに、モデルは微調整なしでオリジナルのトップ1予測精度の72-95%を維持している。
  論文  参考訳（メタデータ） (2024-06-27T17:57:03Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。 本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-06-05T16:35:30Z)
• Dive into Ambiguity: Latent Distribution Mining and Pairwise Uncertainty Estimation for Facial Expression Recognition [59.52434325897716]
  DMUE(DMUE)という,アノテーションのあいまいさを2つの視点から解決するソリューションを提案する。 前者に対しては,ラベル空間における潜伏分布をよりよく記述するために,補助的マルチブランチ学習フレームワークを導入する。 後者の場合、インスタンス間の意味的特徴のペアワイズ関係を完全に活用して、インスタンス空間のあいまいさの程度を推定する。
  論文  参考訳（メタデータ） (2021-04-01T03:21:57Z)
• Learning Causal Semantic Representation for Out-of-Distribution Prediction [125.38836464226092]
  因果推論に基づく因果意味生成モデル(CSG)を提案し,その2つの要因を別々にモデル化する。 CSGはトレーニングデータに適合させることで意味的因子を識別できることを示し、この意味的識別はOOD一般化誤差の有界性を保証する。
  論文  参考訳（メタデータ） (2020-11-03T13:16:05Z)

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

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