論文の概要: Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

• arxiv url: http://arxiv.org/abs/2610.21881v1
• Date: Thu, 15 Oct 2026 13:46:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-17 06:09:33.094309
• Title: Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs
• Title（参考訳）: GPU上での効率的な確率的評価のためのリーンフィードバックの学習
• Abstract要約: 我々は、4.84Mラベル付きプログラムを使用して、ニューラルネットワーク評価器をトレーニングし、Lean 4の予測とコンパイラフィードバックをGPU上で予測する。 候補を分類器でスクリーニングし、フィードバックモデルで肯定的な予測をスコアする2段階評価器は、Leanが候補証明を受け入れたかどうかを予測する精度が87.8%に達する。 評価ツールとリーンの判断を組み合わせることで,GRPOのトレーニングステップを約31%短縮するハイブリッド報酬システムを実現しています。
• 参考スコア（独自算出の注目度）: 13.445668749134411
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts often leave GPUs waiting and withhold rewards from potentially correct proofs. We train neural evaluators to predict Lean 4 verdicts and compiler feedback on GPUs using 4.84M labelled programs. We compare two validity classifiers with a feedback model that annotates proof attempts with predicted goal states and error messages. A two-stage evaluator that screens candidates with a classifier and scores its positive predictions with the feedback model reaches 87.8% accuracy in predicting whether Lean accepts a candidate proof, evaluated on a 68,932-program benchmark collected from public provers. The combined evaluator processes 3.5 candidates per second on one H100, 4.2x the throughput of our 64-worker Lean baseline with environment reuse. Finally, we combine our evaluator with Lean verdicts to obtain a hybrid reward system that shortens GRPO training steps by approximately 31%. After one GRPO epoch with hybrid rewards, the prover achieves nearly the same miniF2F pass@1 as with Lean-only rewards (62.2% versus 62.4%) and a pass@32 of 72.4% versus 71.3%.
• Abstract（参考訳）: 形式的定理証明のための訓練言語モデルは、多数の検証者呼び出しを必要とする。 スローチェックとタイムアウトは、GPUを待機させ、潜在的に正しい証明から報酬を控えることが多い。 我々は、4.84Mラベル付きプログラムを使用して、ニューラルネットワーク評価器をトレーニングし、Lean 4の予測とコンパイラフィードバックをGPU上で予測する。 2つの妥当性分類器と,予測された目標状態とエラーメッセージとのアノテートを行うフィードバックモデルを比較した。 候補を分類器でスクリーニングし、フィードバックモデルで肯定的な予測をスコアする2段階評価器は、公のプローバーから収集された68,932のベンチマークで、Leanが候補証明を受け入れたかどうかを予測する際に、87.8%の精度に達する。 H100と4.2倍のスループットで毎秒3.5の候補を処理します。 最後に、評価者とリーンの評定を組み合わせることで、GRPOのトレーニングステップを約31%短縮するハイブリッド報酬システムを得ます。 1つのGRPO epoch with hybrid rewardsの後、証明者は、Lean-only rewards (62.2% vs 62.4%) と 72.4% vs 71.3% とほぼ同じminiF2F pass@1を達成する。

関連論文リスト

• Verifier-Grounded Agentic RL for Provably Correct Code [20.989739880402407]
  私たちはエージェント環境を構築し、その両方に報酬を与えます。 報酬は、検証者の判断よりも、検証者の診断を読み取って、それが排出する証明義務の重み付けされた部分によって候補を採点する。 整合性監査は検証を上回り、仕様を変更したり、それを証明しようとすると仮定する候補を拒絶する。
  論文  参考訳（メタデータ） (2026-10-13T23:17:25Z)
• SpatialChain: A Benchmark for Auditing Spatial Reasoning Faithfulness in VLMs [32.72182829728677]
  思考可能な視覚言語モデル(VLM)は、空間的ベンチマークにおいてずっと高い精度を報告している。 しかし、最終回答スコアは、正しい予測が忠実な空間的推論や言語的ショートカットを反映しているかを明らかにすることはできない。 28350のトレーニングデータセットであるSpatialChainと、空間指向のGQA質問と、シーングラフに基づく推論チェーンをペアにした899のテスト例を紹介する。
  論文  参考訳（メタデータ） (2026-10-05T14:29:54Z)
• VIGIL: Verifier-Informed Gated Improvement Loop for Spreadsheet Question Answering [6.4443425508730625]
  企業エージェントは、すべての修正がシステムの振る舞いを書き換えることなく、遅延したフィードバックから改善すべきである。 コーパスレベルのスプレッドシート質問応答に対する連続的ハーネス学習について検討した。 金のワークブックと期待されたタイプが供給されたことにより、アンゲートとデュアルゲートのフルリプレイは79の文書に対して82.4%と82.0%の精度に達した。
  論文  参考訳（メタデータ） (2026-10-03T04:41:40Z)
• LeanPolish: Verified Supervision for Lean Proof Compression [4.272652712282259]
  これは、33,402件の承認されたローカル編集と65,596件の同じ状態の試行をリリースする象徴的なLean 4パイプラインです。 First-success Searchは、完全なランキング精度でゴールに依存しないルールを認めており、教師が選択した評価サイトは、自明な削除を報いる。 圧縮のために、シンボリックパスを繰り返すと、ミニF2Fの節約率は19.7%から27.5%に上昇する。
  論文  参考訳（メタデータ） (2026-09-29T18:40:00Z)
• Reward Hacking Challenges Oversight of Autonomous Research Agents [104.38175629103235]
  自律的な研究エージェントは実験を設計し、結果を評価し、レポートを書き、科学的結果とそれを支持する証拠の両方を制御できる。 これは、意図した目標を達成することなく、報酬基準を満たす、報酬ハックのリスクを生み出す。 そこで本研究では,ハッキングが許可された場合,その方法がいかに効果的かつ検出可能か,LCMレビューパネルが意思決定と理由を返却した場合にどのように適応するか,などについて検討する。
  論文  参考訳（メタデータ） (2026-09-23T17:54:01Z)
• Step-wise Rubric Rewards for LLM Reasoning [72.17879367869503]
  RLVR(Reinforcement Learning with Verifiable Rewards)は、大規模言語モデルの推論を改善するために広く使われている。 正しい回答の18.2%は間違っているが、肯定的な報酬がある。 6つの数学的推論ベンチマークで、SRaRはRaRの平均精度を3.57ポイント改善した。
  論文  参考訳（メタデータ） (2026-05-17T07:08:14Z)
• Solver-in-the-Loop: MDP-Based Benchmarks for Self-Correction and Behavioral Rationality in Operations Research [19.31559944205485]
  運用 調査実践者は反復的なプロセスを通じて、不可能なモデルを日常的にデバッグする。 評価ループにtextbfsolver を配置するベンチマークを2つ導入する。 ドメイン固有のRLVRトレーニングによって、8BモデルがフロンティアAPIを越えられることが分かりました。
  論文  参考訳（メタデータ） (2026-01-28T20:02:44Z)
• TreeRPO: Tree Relative Policy Optimization [65.51935468270916]
  nameは、ツリーサンプリングを用いて、様々な推論ステップで報酬の数学的期待を推定する新しい方法である。 GRPOの集団相対的な報酬訓練機構に基づいて、木サンプリング時に生成されたステップレベルグループに基づいて報酬を革新的に計算する。
  論文  参考訳（メタデータ） (2025-06-05T15:56:38Z)
• Self-Taught Evaluators [77.92610887220594]
  本稿では,人工的なトレーニングデータのみを用いて,人間のアノテーションを使わずに即興で証明することを目的としたアプローチを提案する。 我々の自己学習評価器は、RewardBench上で75.4から88.3までの強いLDMを改善することができる。
  論文  参考訳（メタデータ） (2024-08-05T17:57:02Z)
• Large Language Models are not Fair Evaluators [60.27164804083752]
  候補回答の品質ランキングは,文脈の出現順序を変えることで容易にハックできることがわかった。 この操作により、評価結果をスキューし、一方のモデルを他方よりもかなり優れているようにすることができる。 この問題を緩和するための3つのシンプルかつ効果的な戦略を持つフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-05-29T07:41:03Z)

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

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