論文の概要: Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing
- arxiv url: http://arxiv.org/abs/2511.12784v1
- Date: Sun, 16 Nov 2025 21:25:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-18 14:36:24.539496
- Title: Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing
- Title（参考訳）: 意味的類似パラフレーズによる自己形式化ロバスト性の評価
- Authors: Hayden Moore, Asfahan Shah,
- Abstract要約: 大規模言語モデル(LLM)は、自動形式化のための強力なツールとして登場した。
最近の研究により、LLMはパラフレーズ自然言語(NL)入力に敏感であることが判明した。
意味論的に類似したNL文を持つ形式的証明を生成するLLMのロバスト性を評価する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large Language Models (LLMs) have recently emerged as powerful tools for autoformalization. Despite their impressive performance, these models can still struggle to produce grounded and verifiable formalizations. Recent work in text-to-SQL, has revealed that LLMs can be sensitive to paraphrased natural language (NL) inputs, even when high degrees of semantic fidelity are preserved (Safarzadeh, Oroojlooyjadid, and Roth 2025). In this paper, we investigate this claim in the autoformalization domain. Specifically, we evaluate the robustness of LLMs generating formal proofs with semantically similar paraphrased NL statements by measuring semantic and compilation validity. Using the formal benchmarks MiniF2F (Zheng, Han, and Polu 2021) and Lean 4 version of ProofNet (Xin et al. 2024), and two modern LLMs, we generate paraphrased natural language statements and cross-evaluate these statements across both models. The results of this paper reveal performance variability across paraphrased inputs, demonstrating that minor shifts in NL statements can significantly impact model outputs.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、最近、自動形式化のための強力なツールとして登場した。
印象的な性能にもかかわらず、これらのモデルは根底的で検証可能な形式を作るのに苦戦する可能性がある。
テキストからSQLへの最近の研究により、LLMは高い意味的忠実度が保存されている(Safarzadeh, Oroojlooyjadid, Roth 2025)場合でも、パラフレーズ自然言語(NL)入力に敏感であることが判明した。
本稿では, 自己形式化領域におけるこの主張について検討する。
具体的には、意味論的に類似したNL文を含む形式的証明を生成するLLMのロバスト性を評価する。
The formal benchmarks MiniF2F (Zheng, Han, and Polu 2021) and Lean 4 version of ProofNet (Xin et al 2024) and two modern LLMs, we generated paraphrased natural language statement and cross-evaluating these statement across both model。
本稿では,NL文の小さな変化がモデル出力に大きな影響を及ぼすことを示す。
関連論文リスト
- Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
非公式な文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデルの出現により、新たな関心を集めている。
本稿では,LLMをベースとした簡易なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証する。
この結果から, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が有意な可能性を示唆した。
論文 参考訳（メタデータ） (2025-11-14T19:45:17Z) - Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy [8.915674937865676]
第一次論理(英: First-Order Logic、FOL)は、自然言語(NL)で表される概念を表現するための強力な形式主義である。
NLをFOL(NL-FOL翻訳)に変換することは、人間と機械の両方にとって長年にわたる課題である。
論文 参考訳（メタデータ） (2025-11-14T19:11:41Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Factual Self-Awareness in Language Models: Representation, Robustness, and Scaling [56.26834106704781]
大規模言語モデル(LLM)のユビキタス展開における主要な関心事の一つは、生成されたコンテンツの事実的誤りである。
我々は, LLMの内部コンパスの存在を裏付ける証拠を提供し, 生成時の事実的リコールの正しさを規定する。
モデルサイズにわたる実験のスケールとトレーニングのダイナミクスは、トレーニング中に自己認識が急速に出現し、中間層でピークとなることを浮き彫りにしている。
論文 参考訳（メタデータ） (2025-05-27T16:24:02Z) - Steering LLMs for Formal Theorem Proving [1.083373217040891]
我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。
このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。
1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
論文 参考訳（メタデータ） (2025-02-21T15:04:48Z) - Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。
まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。
ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z) - How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。
最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文 参考訳（メタデータ） (2024-01-11T09:27:50Z) - CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。
このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。
LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
論文 参考訳（メタデータ） (2023-11-29T08:29:54Z) - Large Language Models can Contrastively Refine their Generation for Better Sentence Representation Learning [57.74233319453229]
大規模言語モデル(LLM)は画期的な技術として登場し、それらの非並列テキスト生成能力は、基本的な文表現学習タスクへの関心を喚起している。
コーパスを生成するためにLLMの処理を分解するマルチレベルコントラスト文表現学習フレームワークであるMultiCSRを提案する。
実験の結果,MultiCSRはより高度なLCMをChatGPTの性能を超えつつ,ChatGPTに適用することで最先端の成果を得られることがわかった。
論文 参考訳（メタデータ） (2023-10-17T03:21:43Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。