論文の概要: Pseudo-Formalization for Automatic Proof Verification

• arxiv url: http://arxiv.org/abs/2605.20531v1
• Date: Tue, 19 May 2026 22:08:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-21 19:19:56.394984
• Title: Pseudo-Formalization for Automatic Proof Verification
• Title（参考訳）: 自動証明のための擬似形式化
• Authors: Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma,
• Abstract要約: 証明の信頼性検証は、厳密な数学的推論に基づくAIシステムのトレーニングと評価のボトルネックとして依然として残っている。 Pseudo-Formalization (PF) は形式的証明のモジュラリティと精度をキャプチャする証明形式である。 今後の研究を支援するため,研究レベルの検証ベンチマークArxivMathGradingBenchをリリースする。
• 参考スコア（独自算出の注目度）: 17.612188352560494
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.
• Abstract（参考訳）: 証明の信頼性検証は、厳密な数学的推論に基づくAIシステムのトレーニングと評価のボトルネックとして依然として残っている。 リーンのような言語での完全な形式的な証明は、曖昧でモジュール化されているため、容易に検証できます。 ほとんどの証明、特にAIシステムによって書かれた証明は、プロパティを持っておらず、それらを形式言語に翻訳することは、多くのフロンティア数学設定において難しいままである。 Pseudo-Formalization (PF) は、自然言語の柔軟性を維持しつつ、形式的証明のモジュラリティと精度をキャプチャする証明形式である。 擬形式証明は自己完備加群に分解され、それぞれが自然言語の前提、結論、証明を記述する。 正規自然言語証明の正当性を検証するために、LLMはそれを擬形式に変換し、各モジュールを独立に検証する。 PF+BVはオリンピアードと研究レベルの数学の2つのベンチマークで評価され,LLM-as-judgeベースラインは誤りフィリングの精度とリコールに基づいてパレートされる。 今後の研究を支援するため,研究レベルの検証ベンチマークArxivMathGradingBenchをリリースする。

関連論文リスト

• Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure [0.15293427903448023]
  本手法は、学部レベルの教科書から得られた自然言語証明に従って作成された形式的証明データに適用される。 本手法は,リーン証明アシスタントの既存の形式証明ライブラリに適用することにより,極めて可読かつ正確な自然言語証明を出力できることを実証する。
  論文  参考訳（メタデータ） (2025-09-10T09:22:12Z)
• 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)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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