論文の概要: TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow

• arxiv url: http://arxiv.org/abs/2601.17332v1
• Date: Sat, 24 Jan 2026 06:28:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-27 15:23:07.600132
• Title: TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow
• Title（参考訳）: TheoremForge: 低予算エージェントワークフローによるフォーマルデータ合成のスケールアップ
• Authors: Yicheng Tao, Hongteng Xu,
• Abstract要約: コスト効率の良い形式データ合成パイプラインである textbfTheoremForge を紹介する。 我々の戦略は、標準フィルタリングと比較して、証明生成のための textbf1.6$times$ によるデータ収量を増加させる。 その結果、TheoremForgeは、将来のエキスパートモデルをトレーニングするためのデータフライホイールを構築するためのスケーラブルなフレームワークとして確立されます。
• 参考スコア（独自算出の注目度）: 32.80602352741069
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The high cost of agentic workflows in formal mathematics hinders large-scale data synthesis, exacerbating the scarcity of open-source corpora. To address this, we introduce \textbf{TheoremForge}, a cost-effective formal data synthesis pipeline that decomposes the formalization process into five sub-tasks, which are \textit{statement formalization}, \textit{proof generation}, \textit{premise selection}, \textit{proof correction} and \textit{proof sketching}. By implementing a \textit{Decoupled Extraction Strategy}, the workflow recovers valid training signals from globally failed trajectories, effectively utilizing wasted computation. Experiments on a 2,000-problem benchmark demonstrate that TheoremForge achieves a Verified Rate of 12.6\%, surpassing the 8.6\% baseline, at an average cost of only \textbf{\$0.481} per successful trajectory using Gemini-3-Flash. Crucially, our strategy increases data yield by \textbf{1.6$\times$} for proof generation compared to standard filtering. These results establish TheoremForge as a scalable framework for constructing a data flywheel to train future expert models. Our code is available \href{https://github.com/timechess/TheoremForge}{here}.
• Abstract（参考訳）: 形式数学におけるエージェントワークフローの高コストは、大規模なデータ合成を妨げ、オープンソースのコーパスの不足を悪化させる。 これを解決するために、コスト効率のよい形式データ合成パイプラインである \textbf{TheoremForge} を導入し、形式化プロセスを5つのサブタスクに分解し、それを \textit{statement formalization} 、 \textit{proof generation} 、 \textit{premises selection} 、 \textit{proof correction} 、 \textit{proof sketching} という。 ワークフローは、‘textit{Decoupled extract Strategy}’を実装することで、グローバルに失敗したトラジェクトリから有効なトレーニング信号を復元し、無駄な計算を効果的に活用する。 2,000プロブレムのベンチマークでの実験では、TheoremForgeは、Gemini-3-Flashを使った軌道毎の平均コストで8.6\%を超える12.6\%の検証レートを達成した。 重要なことは、我々の戦略は、標準的なフィルタリングと比較して証明生成のための \textbf{1.6$\times$} によるデータ収量を増加させる。 これらの結果は、将来のエキスパートモデルをトレーニングするためのデータフライホイールを構築するためのスケーラブルなフレームワークとして、TheoremForgeを確立します。 私たちのコードは href{https://github.com/timechess/TheoremForge}{here} で利用可能です。

関連論文リスト

• Generative Myopia: Why Diffusion Models Fail at Structure [0.6768558752130311]
  グラフ拡散モデル(GDM)は統計確率を最適化し、textbf frequency filters(英語版)として暗黙的に機能する。 我々は、この失敗がtextbfGradient Starvation によって引き起こされることを理論的、実証的に証明する。 textbfSpectrally-Weighted Diffusionを導入する。
  論文  参考訳（メタデータ） (2025-11-23T19:27:13Z)
• FormaRL: Enhancing Autoformalization with no Labeled Data [5.607770363395876]
  自動形式化のための簡易かつ効率的な強化学習フレームワークである textbfFormaRL を提案する。 FormaRLは、Leanコンパイラからの構文チェックと、大きな言語モデルからの一貫性チェックを統合して、報酬を計算する。 実験の結果、FormaRLはQwen2.5-Coder-7B-Instructのpass@1オートフォーマル化精度を4$sim$6x向上できることがわかった。
  論文  参考訳（メタデータ） (2025-08-26T10:38:18Z)
• Byzantine Failures Harm the Generalization of Robust Distributed Learning Algorithms More Than Data Poisoning [19.624245500772027]
  頑健な分散学習アルゴリズムは、労働者の不在にもかかわらず信頼性の高い性能を維持することを目的としている。 このような誤動作は、通常、$textitByzantine failures$としてモデル化され、任意に破損した通信を可能にするか、あるいはローカルなトレーニングデータに制限された、より弱い形式の汚職である$textitdata poisoning$としてモデル化される。 ビザンチンの失敗は、データ中毒で達成可能なものよりも、はるかに悪い速度で発生します。
  論文  参考訳（メタデータ） (2025-06-22T12:59:15Z)
• TD3: Tucker Decomposition Based Dataset Distillation Method for Sequential Recommendation [50.23504065567638]
  本稿では,メタラーニングフレームワークにおける textbfDataset textbfDistillation 手法である textbfTD3 を紹介する。 TD3は、オリジナルのデータから完全に表現力のある合成配列の要約を蒸留する。 拡張技術により、学習者は合成要約を忠実に適合させ、アンプループでの正確な更新を確実にすることができる。
  論文  参考訳（メタデータ） (2025-02-05T03:13:25Z)
• Rectified Diffusion Guidance for Conditional Generation [94.83538269086613]
  CFGの背後にある理論を再検討し、不適切な組合せ係数(textiti.e.)が生成分布を期待的にシフトさせることを厳密に確認する。 提案手法は, 強みを考慮すれば, textbftextitform ソリューションが有効であることを示す。 実世界のデータに関する実証的な証拠は、我々の設計と既存の最先端拡散モデルとの整合性を実証している。
  論文  参考訳（メタデータ） (2024-10-24T13:41:32Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)

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

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