論文の概要: Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

• arxiv url: http://arxiv.org/abs/2605.10379v1
• Date: Mon, 11 May 2026 11:23:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.762018
• Title: Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
• Title（参考訳）: すべての証明が同等であるとは限らない:LLMの証明品質を正確性を超えて評価する
• Authors: Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov, Martin Vechev,
• Abstract要約: 大規模言語モデル(LLM)は数学的な問題解決に有効である。 ProofRankは、挑戦的な数学的競争から得られたベンチマークである。 正当性のみのベンチマークでは得られない証明品質にはかなりの違いがある。
• 参考スコア（独自算出の注目度）: 7.694715050727414
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient: mathematical proofs should also be clear, concise, insightful, and transferable to other problems. While this proof quality is subjective and depends on the reader and context, many of its components are concrete and broadly valued. In this work, we identify such components and introduce ProofRank, a benchmark curated from challenging mathematical competitions. ProofRank evaluates several scalable proxies of proof quality: (i) conciseness, measuring whether proofs avoid unnecessary steps; (ii) computational ease, measuring the extent to which a proof relies on tedious calculations; (iii) cognitive simplicity, measuring how accessible the used proof techniques are; (iv) diversity, measuring how varied a model's proofs for a single problem are; and (v) adaptivity, measuring whether a model can follow a specified proof technique. Across models, we find substantial differences in proof quality that are not captured by correctness-only benchmarks. We also observe significant trade-offs between proof-quality metrics and correctness, suggesting that future evaluations of mathematical reasoning should measure how useful LLM-generated proofs are.
• Abstract（参考訳）: 大規模言語モデル(LLM)は数学的な問題解法となり、しばしば問題に対する正しい証明を生み出している。 しかし、正しさだけでは十分ではない:数学的証明は明確で簡潔で、洞察に富み、他の問題に転移できる。 この証明品質は主観的であり、読者と文脈に依存するが、そのコンポーネントの多くは具体的で広く評価されている。 本研究では,これらのコンポーネントを同定し,挑戦的な数学的競合から算出したベンチマークであるProofRankを紹介する。 ProofRankは、いくつかのスケーラブルな証明品質プロキシを評価している。 一 証明が不要な措置を免れるか否かを測る簡潔さ 二 計算の容易さ、証明が退屈な計算に依存する程度を測定すること。 三 認識の単純さ、使用済みの証明技術がどの程度アクセス可能かを測定すること。 四 一つの問題に対するモデルの証明がどの程度異なるかを測定すること。 (v)適応性は、あるモデルが特定の証明手法に従うことができるかどうかを測定する。 モデル全体では、正当性のみのベンチマークでは得られない証明品質にかなりの差がある。 また、証明品質の指標と正当性の間に大きなトレードオフが見られ、数学的推論の今後の評価は、LCMの生成した証明がいかに有用かを測定するべきであることを示唆している。

関連論文リスト

• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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