論文の概要: Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

• arxiv url: http://arxiv.org/abs/2603.24372v1
• Date: Wed, 25 Mar 2026 14:53:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-26 21:06:11.340533
• Title: Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning
• Title（参考訳）: サイクル一貫性ファインチューニングによるLean4の自動形式化の改善
• Authors: Arsen Shebzukhov,
• Abstract要約: オートフォーマル化はAIによる数学的研究の加速に役立つ。 自然言語用のLoRAを使ってQwen3.5-2Bを微調整し、FinLeanCorpusでLean4の形式化します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization - automatically translating natural language mathematical texts into formal proof language such as Lean4 - can help accelerate AI-assisted mathematical research, be it via proof verification or proof search. I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning (SFT) with curriculum learning (difficulty 1 to 10), SFT without curriculum ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward. Cycle consistency measures how well the meaning of a statement is preserved through a NL to Lean4 to NL' loop, computed as cosine similarity of off-the-shelf sentence embeddings. On an unseen subset of FineLeanCorpus (FLC) and on PutnamBench, RL substantially outperforms both SFT variants (mean cycle consistency 0.669 vs. 0.513 on FLC; 0.561 vs. 0.422 on PutnamBench), while increasing cross-entropy loss by only 0.011 nats, with minimal impact on formalization quality. Curriculum ordering provides no measurable benefit over shuffled training.
• Abstract（参考訳）: 自動形式化(Autoformalization) - 自然言語の数学的テキストをLean4のような形式的証明言語に自動翻訳することで、AIによる数学的研究の加速に役立つ。 I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning with curical learning (difficulty 1 to 10), SFT without curical ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward。 サイクル整合性(Cycle consistency)は、文の意味がNLからLean4からNLのループを通してどれだけよく保存されているかを測定する。 FineLeanCorpus (FLC) と PutnamBench の目に見えない部分では、RL は SFT 変種 (平均サイクル一貫性 0.669 対 FLC 0.513 ; パットナムベンチ 0.561 対 0.422 対 0.561 対 0.511 対 0.511 対 0.511 対 0.011ナット) を著しく上回り、形式化品質に最小限の影響を与える。 カリキュラムオーダリングは、シャッフルトレーニングよりも測定可能なメリットを提供する。

関連論文リスト

• PRECEPT: Planning Resilience via Experience, Context Engineering & Probing Trajectories A Unified Framework for Test-Time Adaptation with Compositional Rule Learning and Pareto-Guided Prompt Evolution [2.28438857884398]
  自然言語として知識を格納するLLMエージェントは、条件数の増加に伴って急激な検索劣化に悩まされる。 本稿では,3つの密結合コンポーネントによるテスト時間適応のための統合フレームワークであるPreCEPTを紹介する。
  論文  参考訳（メタデータ） (2026-03-10T13:16:45Z)
• Prioritize the Process, Not Just the Outcome: Rewarding Latent Thought Trajectories Improves Reasoning in Looped Language Models [0.0]
  RLTT(Reward Latent Thought Trajectories)は,潜在的推論軌道全体にわたって報酬を分配する強化学習フレームワークである。 RLTTはGRPOよりも大幅に改善され、MATH-500では+14.4%、AIME24では+16.6%、BeyondAIMEでは+10.0%の精度が向上した。 RLTTは数学に特化して訓練されているにもかかわらず、非数学的推論ベンチマークに効果的に移行し、LoopLMにおける強化学習における軌道レベルの信用割当の有効性を実証している。
  論文  参考訳（メタデータ） (2026-02-11T04:39:42Z)
• DISPO: Enhancing Training Efficiency and Stability in Reinforcement Learning for Large Language Model Mathematical Reasoning [31.369103012768964]
  DISPOは単純だが効果的なREINFORCEスタイルのアルゴリズムで、正しい反応と間違った反応のために重要なサンプリング重量の上昇と下降を分離する。 DISPO は AIME'24 (55.42% CISPO と 50.21% DAPO) で 61.04% を達成することを示す。
  論文  参考訳（メタデータ） (2026-02-01T02:45:04Z)
• Distributional Clarity: The Hidden Driver of RL-Friendliness in Large Language Models [50.99097734404912]
  RLフレンドリなモデルでは, クラス内コンパクト性やクラス間分離が, 正誤応答に対する確率割当に現れることを示す。 6つの数学ベンチマークによる実験では、すべてのモデルファミリで一貫した改善が見られ、AIME24では5.9ポイントまで向上した。
  論文  参考訳（メタデータ） (2026-01-11T13:34:44Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
  論文  参考訳（メタデータ） (2025-10-17T14:20:50Z)
• RIDE: Enhancing Large Language Model Alignment through Restyled In-Context Learning Demonstration Exemplars [57.6513924960128]
  調整調整は、大きな言語モデル(LLM)が倫理的かつ有用な振る舞いを確実にするために不可欠である。 本稿では,LLMアライメントを向上させるために,ICL(In-context Learning)を用いた低コストでチューニング不要な手法を提案する。
  論文  参考訳（メタデータ） (2025-02-17T11:16:19Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。 まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。 ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)

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

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