論文の概要: ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib

• arxiv url: http://arxiv.org/abs/2608.20432v1
• Date: Thu, 20 Aug 2026 02:39:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-24 14:49:32.06646
• Title: ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib
• Title（参考訳）: ProofJudge: ツール・グラウンド LLM によるMathlib の形式的証明品質の評価
• Abstract要約: ProofJudgeは,正当性を超えた5次元の形式的証明品質を評価するエージェント式LCM-as-judgeシステムである。 異なるMathlib PRから抽出した218個の宣言のデータセット上でProofJudgeを評価する。 評価された6つの審査モデルは全て、審査員の選好をチャンスよりはるかに上回っており、2人のオープンウェイトな審査員は、ベストな審査員のコストの10分の1で約70%に達する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers' preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.
• Abstract（参考訳）: カーネルの型チェッカーをパスするLean 4の形式的証明は、しかしながら、品質において大きく異なる可能性がある。 ProofJudgeは,ライブラリレバレッジ,自動化適合性,構造的明確性,ステートメント品質,Mathlib規約の5次元を超えて,形式的証明品質をスコアするエージェント的LCM-as-judgeシステムである。 異なるMathlib PRから抽出した218個の宣言のデータセット上でProofJudgeを評価する。 判定エージェントは、PRが適用されるコミットへのツールアクセスによって接地され、スコアリング時にライブラリ状態に問い合わせることができる。 審査員は、修正のために送り返された最初のバージョンより上位に受け入れられたPR Mathlibのバージョンを評価すると、人間の嗜好に沿うと見なされる。 評価された6つの審査員モデルは全て、審査員の選好を80.8%から63.5%にかなり上回り、2人のオープンウェイト審査員がベスト審査員のコストの10分の1で約70%に達する。 我々は、さらなる研究を支援するためのオープンソースアーティファクトとして、審査ハーネス、評価データセット、評価トレースをリリースする。

関連論文リスト

• MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
  MemToCは、実行時ツールによるポストツール-リターン仲裁のベンチマークである。 MemToCは、542の質制御された事実質問から構築された6,504回の評価エピソードで構成されている。 オープンウェイトな7-9Bモデルでは、ツールが強く支配的なクローズドブックの回答を返す。
  論文  参考訳（メタデータ） (2026-08-26T18:22:03Z)
• Beyond Accuracy: A Dual-Judge Evaluation Protocol for Vision-Language Models in Legally Grounded Tasks [1.2555090617748867]
  我々は、標準の0-10品質判断と厳密な二項意味等価判定とを、人為的な基準に対して組み合わせた二重判断プロトコルを寄贈する。 我々は、制御された視覚的基盤を持つ規制課題について研究し、その意味は、すべての入力に対して既知の参照を持つコーデレートされた質問である。
  論文  参考訳（メタデータ） (2026-08-25T08:49:46Z)
• How Reliable Is Your Jailbreak Judge? Calibration and Adversarial Robustness of Automated ASR Scoring [7.789295015218435]
  LLMジェイルブレイクとプロンプトインジェクションに関するほぼすべての論文は、アタック・サクセス・レート(ASR)を報告している。 我々は2人の裁判官の家族と人間の多数決を比較して攻撃する。 審査員の精度とリコールを報告し、審査員の精度を補正したASRを報告し、審査員の逆チェックを含めることを推奨する。
  論文  参考訳（メタデータ） (2026-06-24T07:14:17Z)
• JudgeSense: A Benchmark for Prompt Sensitivity in LLM-as-a-Judge Systems [0.0]
  大規模言語モデルは、他のモデルを評価するための自動判断器として、ますます多くデプロイされている。 我々は、判断感度スコア(JSS)を通じて、このプロパティを定量化するフレームワークとベンチマークであるJiceSenseを紹介します。 事実として、すべての審査員は、極性反転プロンプトアーティファクトによって駆動されるJSS付近に約0.63のクラスタをクラスタする。 コード、意思決定ログ、検証済みのパラフレーズデータセットをリリースし、標準化されたJSSレポートをサポートします。
  論文  参考訳（メタデータ） (2026-04-26T00:08:30Z)
• PoQ-Judge: A Multi-Architecture Evaluation Framework for Cost-Aware Proof-of-Quality in Decentralized LLM Inference [2.621929201001929]
  PoQ-Judgeは、厳格な参照なしでクエリとアウトプットのペアをスコアする専用の判断モデルを訓練するフレームワークである。 本研究では,テキストCNNジャッジ,MiniLMクロスエンコーダ,DeBERTaジャッジの3つのアーキテクチャについて検討する。
  論文  参考訳（メタデータ） (2026-04-20T02:29:52Z)
• The Judge Who Never Admits: Hidden Shortcuts in LLM-based Evaluation [17.386684382460242]
  大規模言語モデル(LLM)は、推論、質問応答、創造的記述といったタスクにおけるシステムの出力を評価するために、ますます使われてきている。 6つの判定モデルに対する評価プロンプトに挿入された制御キュー摂動合成メタデータラベルを用いて,この理想を検証した。 情報源,時間,年齢,性別,民族,教育的地位の6つのキュー族を調査する。
  論文  参考訳（メタデータ） (2026-02-08T14:45:23Z)
• TrustJudge: Inconsistencies of LLM-as-a-Judge and How to Alleviate Them [58.04324690859212]
  自動評価器(LLM-as-a-judge)としての大規模言語モデル(LLM)は、現在の評価フレームワークにおいて重大な矛盾を明らかにしている。 スコア比較不整合とペアワイズ・トランジティビティ不整合という2つの基本的不整合を同定する。 我々は2つの重要なイノベーションを通じてこれらの制限に対処する確率的フレームワークであるTrustJudgeを提案する。
  論文  参考訳（メタデータ） (2025-09-25T13:04:29Z)
• Evaluating Judges as Evaluators: The JETTS Benchmark of LLM-as-Judges as Test-Time Scaling Evaluators [66.83088028268318]
  本稿では,テスト時間スケーリングベンチマークの判定評価について紹介する。 3つのタスク設定の下で、3つのドメイン(推論、コード生成、命令従)での判定性能を評価する。 我々のベンチマークは、審査員が再評価において結果報酬モデルと競合する一方で、ビームサーチにおけるプロセス報酬モデルよりも一貫して悪いことを示している。
  論文  参考訳（メタデータ） (2025-04-21T17:33:23Z)
• Support Evaluation for the TREC 2024 RAG Track: Comparing Human versus LLM Judges [53.12387628636912]
  RAG評価において重要な要素は、引用された文書の情報が回答をサポートするかどうかである。 TREC 2024 RAG Trackの36項目について,45件の参加者を大規模に比較検討した。 以上の結果から,手動によるオフスクラッチ評価の56%では,ヒトとGPT-4oの予測が完全に一致していることが示唆された。
  論文  参考訳（メタデータ） (2025-04-21T16:20:43Z)
• JudgeBench: A Benchmark for Evaluating LLM-based Judges [61.048125269475854]
  judgeBenchは、知識、推論、数学、コーディングにまたがる挑戦的な応答ペアに関するLSMベースの判断を評価するためのベンチマークである。 審査員、微調整された審査員、マルチエージェントの審査員、報酬モデルに関する包括的な評価は、審査員ベンチが以前のベンチマークよりもかなり大きな課題を課していることを示している。
  論文  参考訳（メタデータ） (2024-10-16T17:58:19Z)
• LLMs Can Patch Up Missing Relevance Judgments in Evaluation [56.51461892988846]
  我々は、大きな言語モデル(LLM)を使って、不確定な文書を自動的にラベル付けします。 TREC DLトラックの関連性判定から関連文書をランダムにドロップすることで,穴の度合いの異なるシナリオをシミュレートする。 Vicuna-7B と GPT-3.5 Turbo の平均値に対して,Kendall tau の0.87 と 0.92 の相関式が得られた。
  論文  参考訳（メタデータ） (2024-05-08T00:32:19Z)

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

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