論文の概要: Do We Need Frontier Models to Verify Mathematical Proofs?

• arxiv url: http://arxiv.org/abs/2604.02450v1
• Date: Thu, 02 Apr 2026 18:31:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-06 17:20:24.170573
• Title: Do We Need Frontier Models to Verify Mathematical Proofs?
• Title（参考訳）: 数学的証明にフロンティアモデルが必要か?
• Abstract要約: より小さなオープンソースモデルは、精度でフロンティアモデルに最大10%遅れていることが示されています。 そして、より小さなモデルが、実際にフロンティアモデルのレベルで証明を検証する数学的能力を持っていることを実証する。 我々は、小型モデルの特定の障害モードを克服し、その性能を9.1%の精度で15.9%の自己整合性で向上する特殊プロンプトのアンサンブルを合成する。
• 参考スコア（独自算出の注目度）: 14.254472131009654
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Advances in training, post-training, and inference-time methods have enabled frontier reasoning models to win gold medals in math competitions and settle challenging open problems. Gaining trust in the responses of these models requires that natural language proofs be checked for errors. LLM judges are increasingly being adopted to meet the growing demand for evaluating such proofs. While verification is considered easier than generation, what model capability does reliable verification actually require? We systematically evaluate four open-source and two frontier LLMs on datasets of human-graded natural language proofs of competition-level problems. We consider two key metrics: verifier accuracy and self-consistency (the rate of agreement across repeated judgments on the same proof). We observe that smaller open-source models are only up to ~10% behind frontier models in accuracy but they are up to ~25% more inconsistent. Furthermore, we see that verifier accuracy is sensitive to prompt choice across all models. We then demonstrate that the smaller models, in fact, do possess the mathematical capabilities to verify proofs at the level of frontier models, but they struggle to reliably elicit these capabilities with general judging prompts. Through an LLM-guided prompt search, we synthesize an ensemble of specialized prompts that overcome the specific failure modes of smaller models, boosting their performance by up to 9.1% in accuracy and 15.9% in self-consistency. These gains are realized across models and datasets, allowing models like Qwen3.5-35B to perform on par with frontier models such as Gemini 3.1 Pro for proof verification.
• Abstract（参考訳）: トレーニング、ポストトレーニング、推論の手法の進歩により、フロンティア推論モデルは数学競技で金メダルを獲得し、挑戦的なオープンな問題を解決できるようになった。 これらのモデルの応答に対する信頼を得るには、自然言語の証明をエラーでチェックする必要がある。 LLM審査員は、こうした証明を評価する需要が高まる中、ますます採用されている。 検証は生成よりも容易と考えられるが、信頼できる検証には実際にどのモデルが必要か? 競合レベルの問題に対する人間による自然言語証明のデータセット上で,4つのオープンソースと2つのフロンティアLCMを体系的に評価した。 検証精度と自己整合性(同一の証明上の繰り返し判定における一致率)の2つの重要な指標を考察する。 より小さなオープンソースモデルは、フロンティアモデルよりも10%ほどしか正確ではないが、最大25%は一貫性がない。 さらに、検証器の精度は、全てのモデルにまたがる迅速な選択に敏感であることがわかった。 続いて、より小さなモデルが、実際にフロンティアモデルのレベルで証明を検証できる数学的能力を持っていることを実証するが、一般的な判定プロンプトでこれらの能力を確実に引き出すのに苦労する。 LLM誘導のプロンプトサーチにより、小型モデルの特定の障害モードを克服する特別なプロンプトのアンサンブルを合成し、その性能を9.1%の精度で15.9%の自己整合性で向上させる。 これらのゲインはモデルとデータセット間で実現されており、Qwen3.5-35Bのようなモデルが証明検証のためにGemini 3.1 Proのようなフロンティアモデルと同等に動作する。

関連論文リスト

• LLMs as a Jury: Cross-Model Consensus Can Outperform Process Reward Models for LLM Reasoning [6.241883798820154]
  モデル間コンセンサス(モデル間コンセンサス)について検討し、独立に訓練されたモデル(各モデルが一度解ける程度)が最終解に一致するかを検討した。 パネルをLCM判定として扱い、合意の構造は、他のモデルのスコアではなく、検証信号である。 3つのパネル統計値から平均絶対誤差0.03$までのコンセンサス精度を予測する。
  論文  参考訳（メタデータ） (2026-07-11T05:57:54Z)
• How reliable are LLMs when it comes to playing dice? [0.0]
  離散確率問題に対する制御ベンチマークによる大規模言語モデルの推論能力について検討する。 モデルの平均精度は標準問題では0.96であるが、直観に反するものでは0.59である。 このプロンプトに誤解を招く提案を埋め込むことで、パフォーマンスが最大34%低下し、免疫力を示すモデルが存在しない。
  論文  参考訳（メタデータ） (2026-06-05T17:59:42Z)
• Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
  大規模言語モデルでは, A* 探索のガイダンスを用いて, 正確かつ効率的な証明を生成することができるかを検討する。 経験的に、1B--3B範囲のLlama-3.2モデルはA*ポストトレーニングの恩恵が大きいことが判明した。 より大きな探索空間では、不完全で訓練されたモデルの方が精度が高い。
  論文  参考訳（メタデータ） (2026-05-23T14:28:57Z)
• FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models [0.0]
  我々はtextbfFormalRewardBenchを紹介します。これはLean 4.0で証明された形式的定理で報酬モデルを評価するための最初のベンチマークです。 その結果,フロンティア LLM は最高性能 (59.8%) を達成し,特殊定理証明器は最低性能 (24.4%) を達成した。 textbfFormalRewardBenchを公開し、形式数学における報酬モデルの開発についてさらなる研究を奨励する。
  論文  参考訳（メタデータ） (2026-05-11T07:51:15Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Mitigating LLM Hallucination via Behaviorally Calibrated Reinforcement Learning [32.32593439144886]
  振舞い校正された強化学習により、小さなモデルは不確実な定量化においてフロンティアモデルを超えることができる。 当社のモデルでは,GPT-5の0.207を超える精度向上率(0.806)を挑戦的なドメイン内評価において達成している。
  論文  参考訳（メタデータ） (2025-12-22T22:51:48Z)
• Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
  RFMDataset(Reveal Failure Modes)は200種類の数学的証明問題の集合である。 先進モデルの性能を徹底的に評価する。 解析により,現在の大規模推論モデルの基本的制約を示す10種類のきめ細かい誤差型が明らかになった。
  論文  参考訳（メタデータ） (2025-06-20T16:14:18Z)
• ProcessBench: Identifying Process Errors in Mathematical Reasoning [62.80402845414901]
  本稿では,数学的推論における誤ったステップを識別する能力を測定するためのProcessBenchを紹介する。 ProcessBenchは3400のテストケースで構成され、主に競合とオリンピアードレベルの数学問題に焦点を当てている。 我々はProcessBenchについて、プロセス報酬モデル(PRM)と批判モデルという2種類のモデルを含む広範囲な評価を行う。
  論文  参考訳（メタデータ） (2024-12-09T15:11:40Z)
• An Assessment of Model-On-Model Deception [0.0]
  Llama-2 7B, 13B, 70B, および GPT-3.5 を用いて, MMLU の質問に対する誤った回答を正当化することにより, 1万以上の誤解を招く説明のデータセットを作成する。 さらに悪いことに、すべての能力のモデルは他人を誤解させるのに成功しており、より有能なモデルは詐欺に抵抗するのにわずかに優れている。
  論文  参考訳（メタデータ） (2024-05-10T23:24:18Z)
• The False Promise of Imitating Proprietary LLMs [158.65692029352584]
  より弱い言語モデルを安価に改善するための新しい方法は、より強力なモデルからの出力に対してそれを微調整することである。 このアプローチは、より弱いオープンソースモデルを使用して、プロプライエタリなモデルの機能を安価に模倣することを目指している。 まず、様々なベースモデルサイズを用いてChatGPTを模倣する一連のLMを微調整する。 次に、群衆レーダと標準NLPベンチマークを用いてモデルを評価する。
  論文  参考訳（メタデータ） (2023-05-25T05:00:12Z)
• How Can We Know When Language Models Know? On the Calibration of Language Models for Question Answering [80.82194311274694]
  言語モデルがいつ、自信を持って、特定のクエリに対する答えを知っているか、どのように知ることができるか? 我々は,T5,BART,GPT-2の3つの強力な生成モデルを検討した。 次に、そのようなモデルの校正方法を検討し、その信頼性スコアを正しさの確率と相関させる。
  論文  参考訳（メタデータ） (2020-12-02T03:53:13Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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