論文の概要: FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
- arxiv url: http://arxiv.org/abs/2608.26310v1
- Date: Wed, 26 Aug 2026 18:43:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-28 16:30:58.155675
- Title: FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence
- Title（参考訳）: FaithSieve: Fithful Formal Evidenceを用いた数学証明の微粒化評価
- Abstract要約: FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。
証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。
350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
- 参考スコア（独自算出の注目度）: 9.041607777624504
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge. Existing evaluation approaches largely depend on model-based natural-language judgments, which often overlook local reasoning gaps. While formal theorem provers like Lean offer a path to rigorous verification, using them to evaluate informal text requires solving locality and semantic mismatches: a prover might bypass a local flaw by proving an overly broad target, or validate an auto-formalized statement that drifts from the original mathematical intent. To address this, we introduce FaithSieve, a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs. FaithSieve decomposes coarse proof steps into local reasoning units, extracts typed proof obligations, and verifies them through a formal evaluation agent. Formal validation is gated by semantic alignment scoring, so Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim. We construct two expert-verified datasets, ProofLoc-Olympiad and ProofLoc-University, to benchmark first-error localization. On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy, outperforming the direct-judging baseline of 72.29%. Furthermore, on the 200-problem ProofLoc-University benchmark spanning six advanced domains, FaithSieve reaches 84.5% exact accuracy, compared to 75.0% for the direct judge. Our work demonstrates that decomposing proofs into fine-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural-language reasoning.
- Abstract（参考訳）: 大規模言語モデルは、複雑で多段階の数学的証明を生成できるようになったが、それらの正確さを確実に決定し、初期の論理的誤りをローカライズすることは、依然として重要な課題である。
既存の評価手法はモデルに基づく自然言語判断に大きく依存しており、しばしば局所的な推論のギャップを見落としている。
リーンのような形式的定理の証明者は厳密な検証の道を提供する一方で、非公式テキストを評価するには局所性や意味的なミスマッチの解決が必要である。
これを解決するために、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークであるFaithSieveを紹介します。
FaithSieveは、粗い証明ステップを局所的な推論単位に分解し、型付き証明義務を抽出し、正式な評価エージェントを通じて検証する。
形式的検証はセマンティックアライメントのスコアリングによって強制されるので、形式的証拠は、形式的ステートメントが元のクレームのコンテキスト、オブジェクト、論理的形式を忠実に保存している場合にのみ組み込まれます。
我々は、ファーストエラーローカライゼーションをベンチマークするために、ProofLoc-OlympiadとProofLoc-Universityの2つの専門家検証データセットを構築した。
350プロブレムのオリンピアドデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を達成し、72.29%のダイレクトアジャッジベースラインを上回った。
さらに、6つの高度なドメインにまたがる200プロブレムのProofLoc-Universityベンチマークでは、FaithSieveの精度は84.5%に達し、直接審査では75.0%に達した。
本研究は, 証明を細粒度単位に分解し, 忠実な形式的証拠で根拠付けることにより, 自然言語推論の信頼性を著しく向上させることを示した。
関連論文リスト
- Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。
ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
論文 参考訳（メタデータ） (2026-06-30T00:27:53Z) - Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
我々は、厳密な証明オートフォーマライザは、理想化された証明から分岐する非公式な証明であっても忠実でなければならないと論じる。
ミニF2FとMATH-500の両摂動によるベンチマークを構築した。
我々は,近年の7つのモデルを評価する。これらはいずれもグローバルな摂動に敏感であり,局地的な摂動の下では忠実に保たない。
論文 参考訳（メタデータ） (2026-06-12T18:10:21Z) - Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
そこで本研究では,地平線アノテーションを必要としないラウンドトリップ検証手法を提案する。
2つの形式化が一致するとき、これは忠実な形式化の証拠となる。
我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
論文 参考訳（メタデータ） (2026-04-27T22:26:01Z) - Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
T は形式定理の意味的正しさを評価する枠組みである。
5つの実世界のLean 4リポジトリからベンチマークを構築します。
実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
論文 参考訳（メタデータ） (2026-04-26T13:24:20Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。