論文の概要: Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

• arxiv url: http://arxiv.org/abs/2606.29493v1
• Date: Sun, 28 Jun 2026 16:46:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-30 18:07:15.941138
• Title: Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving
• Title（参考訳）: フォーマルベンチマークの失敗: リーン理論のデータセットの欠陥と評価失敗
• Abstract要約: リーンで証明されたLCM支援定理のベンチマークは、すべての解決されたインスタンスがマシンチェックされた証明を持ってくるため、本質的に信頼できるものとして扱われることが多い。 コーパススケールの静的チェッカーを用いて4,833個の結果を得た。 本稿では,フォールト分類法,自動チェッカーとリコール指向のセマンティック監査プロンプト,および公式な数学データセットの作成を導くための標準リリースを提案する。
• 参考スコア（独自算出の注目度）: 13.87786274932945
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof. However, the kernel only checks that a proof establishes a \emph{formal} statement; it does not verify that the statement faithfully encodes the intended informal problem, nor that evaluation harnesses are robust to trivial or adversarial solutions. We audit five widely used Lean theorem-proving benchmarks and their forks, using corpus-scale static checkers to surface 4,833 findings, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms. We also document semantic defects such as missing hypotheses, problem simplification, incomplete or incorrect translations, and Lean-specific specification hazards. Beyond dataset construction, we survey evaluation-time failure modes and show, on corrected subsets, that defects can both inflate and deflate reported prover scores. We propose a fault taxonomy, a suite of automated checkers and recall-oriented semantic audit prompts, and release standards to guide the creation of formal math datasets and to make evaluation more reproducible and trustworthy. Our checkers, audit prompts, and corrected dataset snapshots are available at https://github.com/Shashi456/atp-checkers.
• Abstract（参考訳）: リーンで証明されたLCM支援定理のベンチマークは、すべての解決されたインスタンスがマシンチェックされた証明を持ってくるため、本質的に信頼できるものとして扱われることが多い。 しかし、カーネルは証明が \emph{formal} のステートメントを確立することのみを確認し、このステートメントが意図された非公式な問題を忠実に符号化し、評価ハーネスが自明または逆解に対して堅牢であることを確認するものではない。 我々は、コーパススケールの静的チェッカーを用いて4,833の発見を表面化し、5つの広く使用されているリーンの定理証明ベンチマークとそのフォークを監査した。 また、仮説の欠如、問題の単純化、不完全あるいは誤った翻訳、リーン固有の仕様の危険など、セマンティックな欠陥も文書化しています。 データセットの構築以外にも、評価時間障害モードを調査し、修正されたサブセットに基づいて、欠陥が報告された証明結果のインフレーションとデフレーションの両方を可能にすることを示す。 本稿では,自動チェッカーとリコール指向のセマンティック監査プロンプトのスイートであるフォールト分類法を提案し,公式な数学データセットの作成をガイドし,再現性が高く信頼性の高い評価を行うための標準をリリースする。 チェッカー、監査プロンプト、修正されたデータセットスナップショットはhttps://github.com/Shashi456/atp-checkers.comから入手可能です。

関連論文リスト

• RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving [27.43470148162019]
  本稿では,Lean-oriented Neural theorem proversをベンチマーク書き換えに統合するために,Proof-Verified Benchmark Rewriting (RePro)を提案する。 ReProは問題を書き直し、リーン検証の証明によって確認された正確さで回答を再生する。 GSM8KとMATHの実験では、ReProの保持された再書き込みインスタンスが100%明確に定義され、実現可能であり、答えの正しさが得られることが示されている。
  論文  参考訳（メタデータ） (2026-08-30T14:23:48Z)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。 証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。 350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
  論文  参考訳（メタデータ） (2026-08-26T18:43:30Z)
• Bayesian control for coding agents [63.64172141184361]
  本稿では,コーディングエージェントのためのコスト依存型シーケンシャル仮説テストフレームワークを提案する。 ベイズ管制官は、正確性に対する信念を維持し、より多くの証拠を集め、候補者を精査し、検証し、停止するかを決定する。 本研究では, 信頼状態が, 不確実性定量化のためのトークン確率と生ツール・サクセスベースラインを上回り, 解釈可能な正当性スコアを得ることを示す。
  論文  参考訳（メタデータ） (2026-06-23T11:41:32Z)
• Stress-Testing Neural Network Verifiers with Provably Robust Instances [10.017475431603389]
  我々は,地中構造ラベルを用いた検証インスタンス生成のための再利用可能なフレームワークを提案する。 また、インスタンスの硬さの異なるソースを推定可能な量の集合であるDifficulty Profileについても紹介する。 我々のフレームワークとこれらのプロファイルを用いて、5つの最先端検証ツールを評価し、異なるインスタンスが検証パイプラインの異なる側面を強調していることを示す。
  論文  参考訳（メタデータ） (2026-05-16T20:56:52Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
  論文  参考訳（メタデータ） (2026-04-07T01:19:41Z)
• What Do Claim Verification Datasets Actually Test? A Reasoning Trace Analysis [34.429649156970015]
  GPT-4o-miniを用いて24Kクレーム検証例の構造化推論トレースを生成する。 直接的エビデンス抽出が支配的であるのに対し,多文合成と数値推論は極めて不十分である。
  論文  参考訳（メタデータ） (2026-04-02T05:54:51Z)
• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Checkは、大規模な言語モデルの解釈ときめ細かい事実チェックのためのフレームワークである。 InFi-Checkerは、サポートエビデンスを提供し、きめ細かいエラータイプを分類し、修正と共に正当化を生成する。 実験の結果,InFi-CheckerはInFi-Check-FGの最先端性能を実現することがわかった。
  論文  参考訳（メタデータ） (2026-01-10T20:00:17Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• SoundnessBench: A Soundness Benchmark for Neural Network Verifiers [45.86647998712757]
  NN検証のための新しいベンチマーク「SoundnessBench」を開発した。 SoundnessBenchは、敵の攻撃から隠された意図的に挿入された反例を持つインスタンスで構成されている。 我々のトレーニングは,隠れた反例を効果的に生成し,SoundnessBenchは最先端のNN検証器のバグの同定に成功したことを実証する。
  論文  参考訳（メタデータ） (2024-12-04T09:24:33Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheckは、カスタマイズされたファクトチェックシステムを構築するためのフレームワークである。 ユーザーは自動的にファクトチェッカーをカスタマイズし、文書やクレームの事実的正当性を検証できる。 CheckerEVALは、人間の注釈付きデータセットを使用して、自動ファクトチェッカーの検証結果の信頼性を高めるソリューションである。
  論文  参考訳（メタデータ） (2024-05-09T07:15:19Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Interpretable Automatic Fine-grained Inconsistency Detection in Text Summarization [56.94741578760294]
  本研究の目的は, 要約中の事実誤りの微粒化を予測し, 微粒化不整合検出の課題を提案することである。 要約における現実的不整合の検査方法に触発され,解析可能な微粒不整合検出モデルであるFinGrainFactを提案する。
  論文  参考訳（メタデータ） (2023-05-23T22:11:47Z)
• Zero-shot Faithful Factual Error Correction [53.121642212060536]
  事実の誤りを忠実に訂正することは、テキストの知識基盤の整合性を維持し、シーケンス・ツー・シーケンス・モデルにおける幻覚を防ぐために重要である。 提案するゼロショットフレームワークは,入力クレームに関する質問を定式化し,与えられたエビデンスにおける正しい回答を求め,そのエビデンスとの整合性に基づいて各補正の忠実さを評価する。
  論文  参考訳（メタデータ） (2023-05-13T18:55:20Z)

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

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