論文の概要: VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
- arxiv url: http://arxiv.org/abs/2606.19399v1
- Date: Wed, 17 Jun 2026 09:08:39 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-19 18:23:39.443163
- Title: VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
- Title（参考訳）: VERITAS: ゼロショット形式定理証明のための検証ガイド付き証明
- Authors: Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang,
- Abstract要約: 本稿では,検証結果を2段階のプロトコルで検証するフレームワークであるVERITASを提案する。
ベスト・オブ・Nサンプリング(Best-of-N sample)は、まず批判を導いたMCTSがフェーズ1の障害を明示的な負の例として取り込みます。
このプロトコルは、自身のフェーズ1で解いたすべての定理を保存するため、フェーズ2のさらなる解はフィードバック駆動の探索に起因する。
- 参考スコア（独自算出の注目度）: 12.732220151515492
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a two-phase protocol: Best-of-N sampling first, then a critic-guided MCTS pass that ingests Phase 1 failures as explicit negative examples. The protocol preserves every theorem solved by its own Phase 1 sweep, so Phase 2's additional solves are attributable to feedback-driven exploration. VERITAS reaches 40.6% on miniF2F (vs. an independently run Best-of-5 at 36.9%, Portfolio 26.2%) and 7.3% on VERITAS-CombiBench, a 55-theorem combinatorics benchmark we release on which Best-of-5 (1.8%) falls below Portfolio (3.6%), exposing that unguided sampling hurts when correct lemma names must be recovered iteratively from verifier feedback. Artifacts are available on GitHub.
- Abstract（参考訳）: LLMベースのフォーマルプロバーは、リッチ検証信号(シンタクスエラー、型ミスマッチ、部分ゴールプログレス)をバイナリパス/フェイルビットに分解することが多い。
提案するゼロショットフレームワークであるVERITASは,各検証器の信号を2段階のプロトコルで復号し,まず2段階のサンプリングを行い,次に批判誘導MCTSパスを通過させ,第1相の障害を負の例として取り込む。
このプロトコルは、自身のフェーズ1で解いたすべての定理を保存するため、フェーズ2のさらなる解はフィードバック駆動の探索に起因する。
VERITAS は miniF2F (vs. an independent run Best-of-5 at 36.9%, Portfolio 26.2%) で 40.6% に達し、VERITAS-CombiBench で 7.3% に達した。
アーティファクトはGitHubで入手できる。
関連論文リスト
- Evidence-Grounded Ensemble Diagnosis of 802.11 Packet Captures: A Multi-Stage Pipeline with Deterministic Reliability Scoring [1.0170129555792935]
802.11パケットキャプチャの診断には、専門家のプロトコル知識が必要で、遅く、エンジニア間で一貫性がなく、スケールできない。
LLMベースのアプローチは、キャプチャーから欠落するが製造されたプロトコルイベントを聴取し、未校正された信頼スコアを生成し、テスト中のモデルによって黄金の基準が共同生成されると評価バイアスを被る。
PROBEは3つの障害に対処する多段階パイプラインである。
論文 参考訳（メタデータ） (2026-06-05T03:39:58Z) - Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
シャノン型エントロピーの不等式を証明することは情報理論の基本的な課題である。
我々は,原子実証のステップを微調整した小規模大規模言語モデルがこのプロセスを自動化することができるか検討する。
GPT-5.5は0ショットプロンプトで1.7%のサンプルを解き、Psitipは33.3%のサンプルを解いた。
論文 参考訳（メタデータ） (2026-06-04T05:43:12Z) - OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。
エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。
OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
論文 参考訳（メタデータ） (2026-05-17T06:39:05Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳（メタデータ） (2025-12-22T16:34:21Z) - Reliable Fine-Grained Evaluation of Natural Language Math Proofs [30.992321135182905]
本稿では,0-7スケールの微粒なスコアをモデル生成数学の証明に割り当てる評価器を開発するための体系的手法を提案する。
ProofBenchは,6つの主要な数学コンペティションから145の問題にまたがる,詳細な証明評価のエキスパートによる最初のデータセットである。
本稿では,強力な推論バックボーンLMと参照解とマーキングスキームからのリッチコンテキストを組み合わせた評価器ProofGraderと,シンプルなアンサンブル手法を提案する。
論文 参考訳（メタデータ） (2025-10-14T02:59:07Z) - CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
隠れアクティベーションの軌跡内の幾何的に分離可能なシグネチャとして解の正しさが符号化されていることを示す。
ClUE は LLM-as-a-judge ベースラインを一貫して上回り、候補者の再選において近代的な信頼に基づく手法に適合または超えている。
論文 参考訳（メタデータ） (2025-10-02T02:14:33Z) - Evaluating the Use of LLMs for Documentation to Code Traceability [3.076436880934678]
大規模言語モデルは、様々なソフトウェアドキュメンテーションとソースコードの間のトレースリンクを確立することができる。
私たちは2つのオープンソースプロジェクト(Unity CatalogとCrawl4AI)から2つの新しいデータセットを作成します。
その結果、最高の性能のLLMは2つのデータセットで79.4%と80.4%のF1スコアを達成した。
論文 参考訳（メタデータ） (2025-06-19T16:18:53Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。