論文の概要: CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

• arxiv url: http://arxiv.org/abs/2507.06181v1
• Date: Tue, 08 Jul 2025 17:03:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-09 16:34:38.357844
• Title: CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
• Title（参考訳）: CriticLean: 数学的形式化のための批判指導型強化学習
• Authors: Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang,
• Abstract要約: CriticLeanは、新しい批評家による強化学習フレームワークである。 教師付き微調整と強化学習を通じてトレーニングされたCriticLeanGPTを導入し、Lean 4の形式化の意味的忠実さを厳格に評価する。 そして、CryticLeanBenchというベンチマークを紹介します。これは、モデルが意味論的に正しい形式を識別する能力を測定するために設計されたベンチマークです。
• 参考スコア（独自算出の注目度）: 48.61754523492116
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: Translating natural language mathematical statements into formal, executable code is a fundamental challenge in automated theorem proving. While prior work has focused on generation and compilation success, little attention has been paid to the critic phase-the evaluation of whether generated formalizations truly capture the semantic intent of the original problem. In this paper, we introduce CriticLean, a novel critic-guided reinforcement learning framework that elevates the role of the critic from a passive validator to an active learning component. Specifically, first, we propose the CriticLeanGPT, trained via supervised fine-tuning and reinforcement learning, to rigorously assess the semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench, a benchmark designed to measure models' ability to distinguish semantically correct from incorrect formalizations, and demonstrate that our trained CriticLeanGPT models can significantly outperform strong open- and closed-source baselines. Building on the CriticLean framework, we construct FineLeanCorpus, a dataset comprising over 285K problems that exhibits rich domain diversity, broad difficulty coverage, and high correctness based on human evaluation. Overall, our findings highlight that optimizing the critic phase is essential for producing reliable formalizations, and we hope our CriticLean will provide valuable insights for future advances in formal mathematical reasoning.
• Abstract（参考訳）: 自然言語の数学的ステートメントを形式的で実行可能なコードに変換することは、自動定理証明の基本的な課題である。 以前の研究は生成とコンパイルの成功に焦点が当てられていたが、生成された形式化が元の問題の意味的な意図を真に捉えているかどうかを批判する段階にはほとんど関心が向けられていない。 本稿では,批判指導型強化学習フレームワークであるCryticLeanを紹介する。 具体的には、まず、教師付き微調整と強化学習によって訓練されたCriticLeanGPTを提案し、リーン4の形式化の意味的忠実さを厳格に評価する。 次に、CryticLeanBenchという、意味論的に正しい形式とを区別するモデルの能力を測定するためのベンチマークを紹介し、訓練されたCryticLeanGPTモデルが、強力なオープンおよびクローズドソースベースラインを著しく上回ることを示す。 CriticLeanフレームワーク上に構築したFineLeanCorpusは、285K以上の問題からなるデータセットで、豊富なドメインの多様性、幅広い難易度、そして人間の評価に基づく高い正確性を示す。 全体として、批判フェーズの最適化は信頼できる形式化を生み出す上で不可欠であり、私たちのCriticLeanは、形式的な数学的推論における将来の進歩に貴重な洞察を提供することを期待しています。

関連論文リスト

• Training Language Model to Critique for Better Refinement [58.73039433159486]
  textbfRefinement-oriented textbfCritique textbfOptimization (RCO)を導入する。 RCOは、批評家モデルによって生成された批評がアクターモデルに応答を洗練させるためのフィードバックループを使用する。 より良い改善につながる批判に焦点を当てることで、RCOは直接的な批判的嗜好評価の必要性を排除している。
  論文  参考訳（メタデータ） (2025-06-27T12:10:57Z)
• RealCritic: Towards Effectiveness-Driven Evaluation of Language Model Critiques [59.861013614500024]
  我々は,Large Language Models (LLMs) の批判能力を評価するために設計された新しいベンチマークを導入する。 通常、オープンループ方式で機能する既存のベンチマークとは異なり、我々のアプローチでは、批判から生成された修正の質を評価するクローズドループ手法を採用している。
  論文  参考訳（メタデータ） (2025-01-24T13:48:10Z)
• Enabling Scalable Oversight via Self-Evolving Critic [59.861013614500024]
  SCRIT(Self-evolving CRITic)は、批評能力の真の自己進化を可能にするフレームワークである。 コントラストベースの自己批判によって生成される合成データのトレーニングによって自己改善する。 最大で10.3%の改善が達成されている。
  論文  参考訳（メタデータ） (2025-01-10T05:51:52Z)
• Can We Further Elicit Reasoning in LLMs? Critic-Guided Planning with Retrieval-Augmentation for Solving Challenging Tasks [68.49251303172674]
  最先端の大規模言語モデル(LLM)は、目覚ましい問題解決能力を示すが、複雑な推論と事実の正しさに苦慮する可能性がある。 既存の手法では、チェーン・オブ・ソートと検索強化生成(RAG)の強みを利用して、複雑な問題をより単純なステップに分解し、検索を適用して事実の正しさを向上させる。 CR-Planner(CR-Planner, CR-Planner, CR-Planner)は, 微調整された批判モデルを利用して, 推論と検索の両方のプロセスを計画を通してガイドする新しいフレームワークである。
  論文  参考訳（メタデータ） (2024-10-02T11:26:02Z)
• Critic-CoT: Boosting the reasoning abilities of large language model via Chain-of-thoughts Critic [48.94340387130627]
  Critic-CoTは、LLMをSystem-2のような批判能力にプッシュするフレームワークである。 人間のアノテーションを使わずにCoT推論パラダイムと遠隔スーパービジョンデータの自動構築 GSM8KとMATHの実験は、我々の強化されたモデルがタスク解決性能を大幅に向上させることを示した。
  論文  参考訳（メタデータ） (2024-08-29T08:02:09Z)
• CriticBench: Benchmarking LLMs for Critique-Correct Reasoning [26.45110574463893]
  CriticBenchは、大規模言語モデルの推論を批判し修正する能力を評価するために設計されたベンチマークである。 生成, 批判, 修正推論における17個のLLMの性能を評価し, 評価した。
  論文  参考訳（メタデータ） (2024-02-22T18:59:02Z)
• Unveiling Bias in Fairness Evaluations of Large Language Models: A Critical Literature Review of Music and Movie Recommendation Systems [0.0]
  生成的人工知能の台頭、特にLarge Language Models (LLMs) は、正確性とともに公正性を精査する衝動を強めている。 近年,レコメンデーションなどの領域におけるLCMの公平性評価が研究されている。 しかし、現在の公平性評価フレームワークがパーソナライズに寄与する程度は未定である。
  論文  参考訳（メタデータ） (2024-01-08T17:57:29Z)

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

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