論文の概要: StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
- arxiv url: http://arxiv.org/abs/2508.04440v1
- Date: Wed, 06 Aug 2025 13:28:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-07 20:09:22.73534
- Title: StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
- Title（参考訳）: StepFun-Formalizer:知識推論融合によるLDMの自動化ポテンシャルの解錠
- Authors: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu,
- Abstract要約: 効果的な自己形式化のための2つの重要な能力を特定する。
我々は、両方の能力を改善するデータ合成およびトレーニングパイプラインであるThinkingFを紹介します。
結果の7Bと32Bモデルは、包括的な形式的知識と強い形式的・形式的推論の両方を示す。
- 参考スコア（独自算出の注目度）: 30.51794514312176
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Autoformalization aims to translate natural-language mathematical statements into a formal language. While LLMs have accelerated progress in this area, existing methods still suffer from low accuracy. We identify two key abilities for effective autoformalization: comprehensive mastery of formal-language domain knowledge, and reasoning capability of natural language problem understanding and informal-formal alignment. Without the former, a model cannot identify the correct formal objects; without the latter, it struggles to interpret real-world contexts and map them precisely into formal expressions. To address these gaps, we introduce ThinkingF, a data synthesis and training pipeline that improves both abilities. First, we construct two datasets: one by distilling and selecting large-scale examples rich in formal knowledge, and another by generating informal-to-formal reasoning trajectories guided by expert-designed templates. We then apply SFT and RLVR with these datasets to further fuse and refine the two abilities. The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning. Notably, StepFun-Formalizer-32B achieves SOTA BEq@1 scores of 40.5% on FormalMATH-Lite and 26.7% on ProverBench, surpassing all prior general-purpose and specialized models.
- Abstract（参考訳）: オートフォーマル化は、自然言語の数学的ステートメントを形式言語に翻訳することを目的としている。
LLMはこの分野の進歩を加速しているが、既存の手法は依然として精度が低い。
本稿では,形式的ドメイン知識の包括的習得,自然言語問題理解の推論能力,形式的アライメントという,効果的な自己形式化のための2つの重要な能力を特定する。
前者がいなければ、モデルは正しい形式的オブジェクトを識別できない。後者がなければ、現実世界のコンテキストを解釈し、それらを形式的表現に正確にマッピングするのに苦労する。
これらのギャップに対処するために、両方の能力を改善するデータ合成およびトレーニングパイプラインであるThinkingFを紹介します。
まず、フォーマルな知識に富んだ大規模サンプルを蒸留・選択し、さらに専門家が設計したテンプレートでガイドされた非公式から形式的な推論軌道を生成する。
次に、これらのデータセットにSFTとRLVRを適用し、さらに2つの能力を融合して洗練する。
結果の7Bと32Bモデルは、包括的な形式的知識と強い形式的・形式的推論の両方を示す。
注目すべきは、StepFun-Formalizer-32BがSoTA BEq@1スコアをフォーマルマートライトで40.5%、ProverBenchで26.7%で達成し、従来の汎用モデルと特殊モデルをすべて上回ったことである。
関連論文リスト
- Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - FMC: Formalization of Natural Language Mathematical Competition Problems [12.86616278136374]
本稿では,誤りフィードバックを伴う大規模言語モデルに基づく自動形式化パイプラインを提案する。
Olympiadレベルのデータセットを、自然言語の問題をリーンの形式化と整合させます。
少数ショット学習,エラーフィードバック,サンプリング数の増加により,自動形式化プロセスが促進されることを示す。
論文 参考訳（メタデータ） (2025-07-15T12:52:47Z) - PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement [13.042323420379187]
PEIRCEは、反復的予想批判プロセスを通じて物質と形式的推論を統合するために設計された、神経象徴的なフレームワークである。
自然言語説明生成の領域において,その能力を実証する。
論文 参考訳（メタデータ） (2025-04-05T09:04:47Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳（メタデータ） (2024-10-28T11:37:39Z) - Large Language Models with Controllable Working Memory [64.71038763708161]
大規模言語モデル(LLM)は、自然言語処理(NLP)の一連のブレークスルーをもたらした。
これらのモデルをさらに切り離すのは、事前訓練中に内在する膨大な量の世界的知識だ。
モデルの世界知識が、文脈で提示された事実情報とどのように相互作用するかは、まだ解明されていない。
論文 参考訳（メタデータ） (2022-11-09T18:58:29Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z) - A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
固有プローブ構築のための新しい潜在変数定式化を提案する。
我々は、事前訓練された表現が言語間交互に絡み合ったモルフォシンタクスの概念を発達させる経験的証拠を見出した。
論文 参考訳（メタデータ） (2022-01-20T15:01:12Z) - Semi-supervised Formality Style Transfer using Language Model
Discriminator and Mutual Information Maximization [52.867459839641526]
フォーマル・スタイル・トランスファー(英: Formality style transfer)とは、非公式な文を文法的に正しい形式文に変換するタスクである。
本稿では,言語モデルに基づく識別器を用いて,文が形式的である確率を最大化する半教師付き形式表現スタイル転送モデルを提案する。
実験の結果,我々のモデルは,自動計測と人的判断の両面で,従来の最先端のベースラインを著しく上回りました。
論文 参考訳（メタデータ） (2020-10-10T21:05:56Z) - Leap-Of-Thought: Teaching Pre-Trained Models to Systematically Reason
Over Implicit Knowledge [96.92252296244233]
大規模な事前学習言語モデル(LM)は推論能力を得るが、制御は困難である。
本研究では,暗黙的,事前学習された知識と明示的な自然言語文を併用して,体系的推論を確実に行うことができることを示す。
我々の研究は、シンプルな自然言語文を追加することで、モデルを簡単に修正できるユーザと対話することで、常に改善されるオープンドメインシステムへの道を開く。
論文 参考訳（メタデータ） (2020-06-11T17:02:20Z) - Data Annealing for Informal Language Understanding Tasks [66.2988222278475]
本稿では,非公式な言語タスクのパフォーマンスギャップを埋めるために,データアニーリング変換学習手法を提案する。
これは、非公式言語でBERTのような事前訓練されたモデルを利用することに成功した。
論文 参考訳（メタデータ） (2020-04-24T09:27:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。