論文の概要: ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
- arxiv url: http://arxiv.org/abs/2510.24592v1
- Date: Tue, 28 Oct 2025 16:22:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-29 15:35:37.270981
- Title: ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
- Title（参考訳）: ReForm: 予測境界列最適化による反射オートフォーマライゼーション
- Authors: Guoxin Chen, Jing Wu, Xinjie Chen, Wayne Xin Zhao, Ruihua Song, Chengxi Li, Kai Fan, Dayiheng Liu, Minpeng Liao,
- Abstract要約: 本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均17.2ポイントの改善を達成した。
- 参考スコア（独自算出の注目度）: 73.0780809974414
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization, which translates natural language mathematics into machine-verifiable formal statements, is critical for using formal mathematical reasoning to solve math problems stated in natural language. While Large Language Models can generate syntactically correct formal statements, they often fail to preserve the original problem's semantic intent. This limitation arises from the LLM approaches' treating autoformalization as a simplistic translation task which lacks mechanisms for self-reflection and iterative refinement that human experts naturally employ. To address these issues, we propose ReForm, a Reflective Autoformalization method that tightly integrates semantic consistency evaluation into the autoformalization process. This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors through progressive refinement. To effectively train this reflective model, we introduce Prospective Bounded Sequence Optimization (PBSO), which employs different rewards at different sequence positions to ensure that the model develops both accurate autoformalization and correct semantic validations, preventing superficial critiques that would undermine the purpose of reflection. Extensive experiments across four autoformalization benchmarks demonstrate that ReForm achieves an average improvement of 17.2 percentage points over the strongest baselines. To further ensure evaluation reliability, we introduce ConsistencyCheck, a benchmark of 859 expert-annotated items that not only validates LLMs as judges but also reveals that autoformalization is inherently difficult: even human experts produce semantic errors in up to 38.5% of cases.
- Abstract（参考訳）: 自然言語数学を機械で検証可能な形式ステートメントに変換するオートフォーマル化は、自然言語で述べられている数学問題を解くために形式的な数学的推論を使用するために重要である。
大規模言語モデルは構文的に正しい形式文を生成することができるが、しばしば元の問題の意味的な意図を保存できない。
この制限は、LLMアプローチの自己形式化を、人間の専門家が自然に採用する自己回帰と反復的洗練のメカニズムが欠如している単純な翻訳タスクとして扱うことに由来する。
これらの問題に対処するために,意味的整合性評価を自己形式化プロセスに密に統合する反射的自己形式化手法であるReFormを提案する。
これにより、モデルが形式的ステートメントを反復的に生成し、セマンティックな忠実さを評価し、プログレッシブ・リファインメントを通じて自己修正された識別エラーを発生させることができる。
この反射モデルを効果的に訓練するために、異なる順序位置で異なる報酬を利用するプロスペクティブ・バウンド・シーケンス・最適化(PBSO)を導入し、モデルが正確な自己形式化と正しいセマンティック・バリデーションの両方を発達させ、反射の目的を損なう表面的批判を防止する。
4つのオートフォーマル化ベンチマークによる大規模な実験により、ReFormは最強のベースラインに対して平均17.2ポイントの改善を達成した。
評価の信頼性をさらに高めるため、審査員としてLSMを検証するだけでなく、オートフォーマル化が本質的に困難であることを明らかにした859件のエキスパートアノテート項目のベンチマークであるConsistencyCheckを導入する。
関連論文リスト
- Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
結論を導かない限り、多くの数学的問題は直接形式化できない。
本研究では,大規模言語モデルの導出能力を測定するためにConjectureBenchを開発した。
提案手法は,GPT-4.1と7とDeepSeek-V3.1の13のPutnamBench問題において,最初のエンドツーエンドの自動形式化を実現する。
論文 参考訳（メタデータ） (2025-10-13T22:29:49Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning [8.135142928659546]
自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。
提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。
全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
論文 参考訳（メタデータ） (2025-06-12T17:09:51Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - ReVISE: Learning to Refine at Test-Time via Intrinsic Self-Verification [53.80183105328448]
Refine via Intrinsic Self-Verification (ReVISE)は、LLMが自己検証を通じてアウトプットを自己修正できる効率的なフレームワークである。
様々な推論タスクに関する実験により、ReVISEは効率的な自己補正を実現し、推論性能を大幅に向上することを示した。
論文 参考訳（メタデータ） (2025-02-20T13:50:02Z) - Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
本稿では,自然言語問題記述から解法対応最適化モデルを自動生成する,$textitautoformulation$の問題にアプローチする。
オートフォーミュレーションの3つの主要な課題を識別する: $textit(1)$ 巨大で問題に依存した仮説空間、および$textit(2)$ 不確実性の下でこの空間を効率的かつ多様に探索する。
我々は,$textitLarge Language Models$と$textitMonte-Carlo Tree Search$を併用した新しい手法を提案する。
論文 参考訳（メタデータ） (2024-11-03T20:41:38Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳（メタデータ） (2024-10-28T11:37:39Z) - Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。
本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2024-06-05T16:35:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。