Fugu-MT 論文翻訳(概要): Pseudo-Formalization for Automatic Proof Verification

論文の概要: 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（参考訳）: 自動証明のための擬似形式化
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をリリースする。

関連論文リスト

Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs [16.584143060150165]
我々は,5つの条件を満たす形式的なリーン証明を生成する,エージェント的・オラクル誘導型証明探索であるPristisを紹介した。その中核は、新しい忠実に保存される分割とコンカレント検索であり、これは orderDecompose という名前で呼ばれる。ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。
論文参考訳（メタデータ） (2026-08-15T22:20:08Z)
Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文参考訳（メタデータ） (2026-02-02T17:42:53Z)
Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文参考訳（メタデータ） (2025-10-29T15:30:31Z)
Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure [0.15293427903448023]
本手法は、学部レベルの教科書から得られた自然言語証明に従って作成された形式的証明データに適用される。本手法は,リーン証明アシスタントの既存の形式証明ライブラリに適用することにより,極めて可読かつ正確な自然言語証明を出力できることを実証する。
論文参考訳（メタデータ） (2025-09-10T09:22:12Z)
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)
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)
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)

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

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