論文の概要: SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
- arxiv url: http://arxiv.org/abs/2610.08319v1
- Date: Tue, 06 Oct 2026 13:22:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-08 02:58:30.00477
- Title: SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
- Title（参考訳）: SCOPE: 政策プランナーとしての言語モデルを用いた証明理論
- Abstract要約: SCOPE(State-Conditioned Operator Planning and Execution)は、労働の自然な分割を強制する。
システムはオペレータの語彙を計画し、シンボルエンジンが数値を実行し、コンパイラが証明をレンダリングする。
システム認証は191/218 (87.6%) で、バックボーンは135Mである。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.
- Abstract（参考訳）: Leanのような証明アシスタントでは、生成された証明はマシンのコンパイルチェックをパスしなければならない。
証明はすべてのコンテンツ整数が正しい場合にのみ有効であるため、パスレートは整数毎の精度のk番目のパワーによって制限される。
2,617件の基準証明で制御された汚職は、この権限法を裏付ける。
SCOPE(State-Conditioned Operator Planning and Execution)は、オペレータの語彙をモデルに計画し、シンボルエンジンが数値を実行し、コンパイラが証明をレンダリングする。
218プロブレムのスイートでは、191/218 (87.6%)を135Mのバックボーンで認証し、7B DeepSeek-Prover-V1.5-RLはトークンの27.5倍、壁の37.5倍の18/218を認証し、DeepSeek-Prover-V2-7Bは双方向のデュアルスイートで0を認証している。
多段階思考のコストは6.12で、自然言語の思考テキストは生成しない。
判定フレーム内のラグエンジン状態を現在のものと置き換えると、パスレートが117/218から191/218に上がり、チェーンエンド損失の重み付けが問題となる。
パブリックなLean-Workbookライブラリでは、3,536のグレード可能な許容可能な問題のうち2,132が、メインスイートの回帰がゼロである(60.29%)。
すべての読み込みは、独立したリチェックとリバース検証を備えたバージョンフリーのレビューから得られる。
自由生成を制限し、意思決定時の情報を可視化することは、モデルを拡大するよりも直接的な方法である。
関連論文リスト
- JevAdvBench: A Benchmark and Black-Box Attacks for Reinforcement Learning for Calibrated Decisions Models [25.5874772119945]
JevAdvBench は RLCD モデルの最初の敵対的ベンチマークである。
ラベルではなく、モデル自身のクリーンな決定に対して攻撃された各決定をスコア付けし、同じ再実行による変更に対して読み取る。
Jev-1.13.0では、リワードは再実行ベースラインの1.2パーセント以内に留まり、スキーマ外のフィールドはモデルに到達しない。
論文 参考訳（メタデータ） (2026-09-25T11:32:19Z) - BeTaL-GBI: Admission-Aware Benchmark Tuning and Full-Stack Verification of Geometric Belief Interfaces [2.894286977279531]
本研究は,企業検証アーキテクチャが要求を監査しつつ,インターフェース障害,タスク能力,ポリシー適合性,整合性を分離できるかどうかを検討する。
BeTaL-GBI v0.2 は LLM-in-the-loop を2,218,750,380 以上のグリッドポイントで適用し、条件付き性能からフォーマットの入力を分離する。
512の総合的なタスクにおいて、16ゲートポリシーは、116の激しい矛盾を全て検出し、99のクリーンレコードを全て受け入れる。幻覚剤とエビデンスフォーガーサロゲートは無音のプロモーションでブロックされる。
論文 参考訳（メタデータ） (2026-08-21T16:52:38Z) - Reconcile Once, Write Anytime: A Trust-Tiered Librarian and a Multi-Agent Writer for Drift-Free, Point-in-Time Research [7.426963307811556]
本稿では,保守型ポイントインタイム知識ライブラリをレポート作成から分離する2層エージェントシステムを提案する。
ポータブルなマルチエージェント"ライター"ランタイムは、任意の知識遮断Tにおいて矛盾のないエビデンス基底レポートを構成する。
我々は,555,926枚のエビデンスカードを出力する6,130個のソースの自己収集・公開コーパスを評価した。
論文 参考訳（メタデータ） (2026-08-13T09:09:28Z) - Judging Is Not Enumerating: Silent Omissions in LLM-Authored Acceptable Sets [13.85834524293015]
私たちは、ロールが想定する能力を測定し、通常、ロールが配置されるプロトコルの下でそれを欠いていることを見つけます。
モデルは、その候補がセット自体の作者よりもはるかに優れているかどうかを判断する。
論文 参考訳（メタデータ） (2026-08-02T05:00:44Z) - Proof-or-Stop: Don't Trust the Agent, Trust the Evidence -- Loop Engineering for Verifiable Evidence-Gated Lifecycle Control [5.796499740822509]
本稿では, プロフ・オ・ストップライフサイクル・コントロールについて紹介する。
これは、新しい、追跡されたソースベースで機械的に検証可能な証拠が関連するゲートを満たす場合にのみ、ライフサイクルの遷移を可能にする。
我々は, 機構試験, パワードコントロール・ポリシー・アブレーション, セルフアプリケーション・エビデンスによるオープンソース実装の評価を行った。
論文 参考訳（メタデータ） (2026-07-16T12:06:21Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
HumanityのLast Exam (HLE)は、フロンティアの大規模言語モデルを評価するために広く使われているベンチマークである。
HLE-Verifiedは,透過的検証プロトコルときめ細かい誤り分類法を備えたHLEの検証および改訂版である。
我々は,HLEとHLE-Verifiedの7つの最先端言語モデルを評価し,平均7～10ポイントの絶対精度を観測した。
論文 参考訳（メタデータ） (2026-02-15T02:50:15Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。