論文の概要: FormaRL: Enhancing Autoformalization with no Labeled Data
- arxiv url: http://arxiv.org/abs/2508.18914v1
- Date: Tue, 26 Aug 2025 10:38:18 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-27 17:42:38.807673
- Title: FormaRL: Enhancing Autoformalization with no Labeled Data
- Title（参考訳）: FormaRL: ラベル付きデータなしでのオートフォーマル化を実現する
- Authors: Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, Yang Liu,
- Abstract要約: 自動形式化のための簡易かつ効率的な強化学習フレームワークである textbfFormaRL を提案する。
FormaRLは、Leanコンパイラからの構文チェックと、大きな言語モデルからの一貫性チェックを統合して、報酬を計算する。
実験の結果、FormaRLはQwen2.5-Coder-7B-Instructのpass@1オートフォーマル化精度を4$sim$6x向上できることがわかった。
- 参考スコア（独自算出の注目度）: 5.607770363395876
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization is one of the central tasks in formal verification, while its advancement remains hindered due to the data scarcity and the absence efficient methods. In this work we propose \textbf{FormaRL}, a simple yet efficient reinforcement learning framework for autoformalization which only requires a small amount of unlabeled data. FormaRL integrates syntax check from Lean compiler and consistency check from large language model to calculate the reward, and adopts GRPO algorithm to update the formalizer. We also curated a proof problem dataset from undergraduate-level math materials, named \textbf{uproof}, in the hope to facilitate the exploration of autoformalization and theorem proving in advanced math. Experiments show that FormaRL can increase the pass@1 autoformalization accuracy of Qwen2.5-Coder-7B-Instruct by 4 $\sim$ 6x (4.04\% $\to$ 26.15\% on ProofNet and 2.4\% $\to$ 9.6\% on uproof) with merely 859 unlabeled data. And on uproof our method also achieved a strong improvement in out-of-distribution performance compared to existing open-source state-of-the-art autoformalizers on both pass@1 accuracy (6.2\% $\to$ 9.6\%) and pass@16 accuracy (24.4\% $\to$ 33.6\%). Training code of FormaRL is open-sourced at https://github.com/THUNLP-MT/FormaRL.
- Abstract（参考訳）: オートフォーマル化は形式的検証における中心的な課題の1つだが、データ不足と効率的な方法の欠如により、その進歩は妨げられ続けている。
本研究では,少数の未ラベルデータしか必要としない自動形式化のための簡易かつ効率的な強化学習フレームワークである \textbf{FormaRL} を提案する。
FormaRLは、Leanコンパイラからの構文チェックと、大きな言語モデルからの一貫性チェックを統合して報酬を計算する。
また、先進数学における自己形式化と定理の探索を容易にするために、学部レベルの数学教材である「textbf{uproof}」から証明問題データセットをキュレートした。
FormaRLは、Qwen2.5-Coder-7B-Instructのpass@1オートフォーマル化精度を4$\sim$ 6x (4.04\% $\to$ 26.15\%、ProofNetでは2.4\% $\to$ 9.6\%)で向上できる。
また,提案手法は,パス@1の精度(6.2\% $\to$9.6\%)とパス@16の精度(24.4\% $\to$33.6\%)に対して,既存のオープンソースオートフォーマライザと比較して,アウト・オブ・ディストリビューション性能の大幅な向上を実現した。
FormaRLのトレーニングコードはhttps://github.com/THUNLP-MT/FormaRLで公開されている。
関連論文リスト
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - FormalAlign: Automated Alignment Evaluation for Autoformalization [12.674957231226871]
textscFormalAlignは、自動形式化シーケンス生成タスクと、入力と出力の間の表現アライメントの両方をトレーニングする。
textscFormalAlignは4つのベンチマークで評価され、優れたパフォーマンスを示している。
この効果的なアライメント評価は、手動検証の必要性を大幅に低減する。
論文 参考訳（メタデータ） (2024-10-14T03:58:35Z) - LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。
実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-06-20T06:42:27Z) - Improving Autoformalization using Type Checking [15.58948808529849]
我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。
ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。
我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z) - Process-Driven Autoformalization in Lean 4 [30.056591518828554]
大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。
また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。
実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
論文 参考訳（メタデータ） (2024-06-04T03:48:08Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。