論文の概要: Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs

• arxiv url: http://arxiv.org/abs/2608.15432v1
• Date: Sat, 15 Aug 2026 22:20:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-18 19:59:03.29822
• Title: Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
• Title（参考訳）: 証明はそれを証明しているのか? 要素証明の忠実な形式化
• Abstract要約: 我々は,5つの条件を満たす形式的なリーン証明を生成する,エージェント的・オラクル誘導型証明探索であるPristisを紹介した。 その中核は、新しい忠実に保存される分割とコンカレント検索であり、これは orderDecompose という名前で呼ばれる。 ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。
• 参考スコア（独自算出の注目度）: 16.584143060150165
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In formal verification, both the autoformalization of statements and automated proof search have been studied extensively. While automated proof search can produce a formal proof that compiles, the generated proof does not necessarily reflect how the natural-language argument arrives at its conclusion--a property we refer to as faithfulness. With faithfully formalized proofs, one can check the reasoning behind a human- or AI-written argument, and assist mathematicians in formalizing their proof sketches. However, it is particularly challenging due to misalignment of formal proof tactics and natural language reasoning. In this work, we rigorously describe a set of five necessary conditions a faithful formal proof must satisfy, and introduce Pistis, an agentic, oracle-guided proof search that produces formal Lean proofs that satisfy them. At its core is a novel faithfulness-preserving divide-and-conquer search, which we name OrderDecompose, that tracks citation dependencies and blocks unfaithful shortcuts, paired with a refutation search, that surfaces gaps and errors in the natural language proof source. OrderDecompose completes proofs that baselines cannot close even within a 12-hour budget, and its artifacts compile over 33$\times$ as fast as prior work's. We apply Pistis on the first three books of Euclid's Elements, producing high-quality artifacts containing faithful formal proofs. Under a blinded human study and an LLM-as-a-judge protocol on rigorous rubrics, Pistis-generated proofs are favored over prior works--2.89$\times$ and 5.2$\times$ as often by human reviewers and the LLM judge, respectively. It further uncovers gaps in Euclid's proofs and their translation, and can accept or refute natural language proofs written by humans or AI, demonstrating that faithful formalization is useful as a proof-checking tool.
• Abstract（参考訳）: 形式的検証では、ステートメントの自動形式化と自動証明探索の両方が広く研究されている。 自動証明探索は、コンパイルする形式的な証明を生成することができるが、生成された証明は、自然言語の議論がその結論にどのように到達するかを必ずしも反映していない。 忠実に形式化された証明では、人間やAIで書かれた議論の背後にある推論をチェックし、数学者が証明のスケッチを形式化するのを助けることができる。 しかし、形式的証明戦術や自然言語推論の誤りのため、特に困難である。 本研究では, 忠実な形式的証明が満たさなければならない5つの条件の集合を厳密に記述し, それらを満たす形式的リーン証明を生成するエージェント的, オラクル指向の証明探索であるPristisを紹介する。 OrderDecomposeという名前で、引用の依存関係を追跡し、不誠実なショートカットをブロックし、難解な検索と組み合わせて、自然言語の証明ソースのギャップとエラーを表面化する。 OrderDecomposeは12時間以内の予算でもベースラインがクローズできないという証明を完了し、その成果物は以前の作業と同じ速さで33$\times$をコンパイルする。 ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。 目隠しされた人間の研究と厳格な潤滑剤に関するLSM-as-a-judgeプロトコルの下では、ピスティスが生成した証明は以前の研究よりも好まれる:-2.89$\times$と5.2$\times$は、それぞれ人間のレビュアーとLLMの審査員によってそれぞれ好まれる。 さらに、ユークリッドの証明と翻訳のギャップを明らかにし、人間やAIによって書かれた自然言語の証明を受け入れたり否定したりすることができ、忠実な形式化が証明チェックツールとして有用であることを示す。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Pseudo-Formalization for Automatic Proof Verification [17.612188352560494]
  証明の信頼性検証は、厳密な数学的推論に基づくAIシステムのトレーニングと評価のボトルネックとして依然として残っている。 Pseudo-Formalization (PF) は形式的証明のモジュラリティと精度をキャプチャする証明形式である。 今後の研究を支援するため,研究レベルの検証ベンチマークArxivMathGradingBenchをリリースする。
  論文  参考訳（メタデータ） (2026-05-19T22:08:51Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  本稿では,ステップ・バイ・ステップ検証のための新しい自動形式化手法であるStepProofを提案する。 StepProofは、完全な証明を複数の検証可能なサブプロテクションに分解し、文レベルの検証を可能にする。 StepProofは従来の手法に比べて証明成功率と効率を著しく改善することを示す。
  論文  参考訳（メタデータ） (2025-06-12T10:31:23Z)
• 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)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
  本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。 大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
  論文  参考訳（メタデータ） (2022-10-21T22:37:22Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)

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

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