論文の概要: A First Proof Sprint
- arxiv url: http://arxiv.org/abs/2602.13587v1
- Date: Sat, 14 Feb 2026 04:09:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-17 14:17:28.22298
- Title: A First Proof Sprint
- Title(参考訳): 最初の証明スプリント
- Authors: Joseph Corneli,
- Abstract要約: このモノグラフは10種類の研究レベルの問題に関するマルチエージェント証明スプリントを報告している。
問題3は、ここで使われるスコープ付き基準の下で、検証完全存在パスを持つ。
問題5は、F_O$-ローカル接続スペクトルのスコープ制限形式で解決される。
問題6は、一般の場合において、名前付き残される義務の一部である。
問題7と9にはノードレベルの検証アーティファクトがあるが、未解決のバリデーションギャップがある。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This monograph reports a multi-agent proof sprint on ten research-level problems, combining rapid draft generation with adversarial verification, targeted repair, and explicit provenance. The workflow uses wiring-diagram decompositions of claim dependencies to localize gaps and coordinate reviewer-driven revisions. Final outcomes are heterogeneous but explicit: the manuscript distinguishes mathematical status from QC-validation status. Mathematically, Problem~3 has a validation-complete existence path under the scoped criterion used here (uniqueness/irreducibility treated as optional), Problem 5 is solved in a scope-limited form for $F_O$-local connective spectra, Problem 10 is conditional under clearly stated assumptions (with explicit necessity counterexamples when assumptions are dropped), and Problems 4 and 6 are partial with named remaining obligations in the general case (including an unconditional $K_n$ result for Problem 6 with $c_0 = 1/3$). Problem 7 is treated as provisionally closed via the rotation-route theorem chain, pending independent ledger re-check. At the QC layer, Problems~7 and~9 have node-level validation artifacts but still contain unresolved verifier gaps. The main methodological result is that structure-aware verification and layer-switching strategies improve reliability and calibration in compressed proof sprints.
- Abstract(参考訳): このモノグラフは, 高速なドラフト生成と逆検証, ターゲット修復, 明示的証明を組み合わせ, 10 つの研究レベルの問題に対するマルチエージェント証明スプリントを報告した。
このワークフローは、クレーム依存関係の配線ダイアグラム分解を使用してギャップをローカライズし、レビュア駆動のリビジョンを調整する。
最終結果は不均一であるが明示的であり、この写本はQC価状態と数学的地位を区別する。
数学的には、イシュー~3はここで用いられるスコープ付き基準の下で検証完全存在パスを持ち、イシュー5は、$F_O$-ローカル接続スペクトルのスコープ限定形式で解決され、イシュー10は、明確に定義された仮定の下で条件付きである(仮定が削除されたときの明確な必然性の反例を含む)、イシュー4と6は、一般の場合において、名前付き残される義務(イシュー6の$c_0 = 1/3$の未条件の$K_n$結果を含む)。
問題7は、独立台帳の再チェックを待つ回転経路定理チェーンを介して仮閉体として扱われる。
QC層では、問題~7と9はノードレベルの検証アーティファクトを持っているが、未解決のバリデーションギャップがまだ残っている。
主な手法は, 圧縮された実証スプリントにおいて, 信頼性と校正性を向上することである。
関連論文リスト
- zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing [7.274627641804014]
zkCraftは決定論的、R1CS対応のローカライゼーションと証明付き検索を組み合わせて意味的不整合を検出するフレームワークである。
証明付きローカライゼーションは, 偽陽性が低い多彩な下限および過制約の断層を検出し, コストのかかるソルバ相互作用を低減できることを示す。
論文 参考訳(メタデータ) (2026-01-31T11:31:00Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳(メタデータ) (2025-12-22T16:34:21Z) - The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
この研究は LLM-Verifier Convergence Theorem の開発によってギャップを埋める。
LLMと検証器の相互作用を離散時間マルコフ連鎖としてモデル化する。
われわれはこの予測を90,000件以上の治験を含む広範囲な実証キャンペーンでストレステストした。
論文 参考訳(メタデータ) (2025-11-30T22:19:09Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳(メタデータ) (2025-11-26T06:39:19Z) - Evidence-Bound Autonomous Research (EviBound): A Governance Framework for Eliminating False Claims [0.609170287691728]
EviBoundは、二重ガバナンスゲートを通じて偽のクレームを排除するエビデンスベースの実行フレームワークである。
事前実行承認ゲートは、コードが実行される前に受け入れ基準スキーマを検証する。
実行後検証ゲートは、MLflow APIクエリを通じてアーティファクトを検証する。
論文 参考訳(メタデータ) (2025-10-28T17:47:13Z) - Hierarchical Sequence Iteration for Heterogeneous Question Answering [27.22775290181187]
本稿では,文書,表,知識グラフを可逆的階層列に線形化する統一フレームワークであるHSEQを紹介する。
HotpotQA(テキスト)、HybridQA/TAT-QA(テーブル+テキスト)、MetaQA(KG)の実験では、強いシングルパス、マルチホップ、エージェントRAGベースラインを高い効率で一貫したEM/F1が得られた。
論文 参考訳(メタデータ) (2025-10-23T12:48:18Z) - Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。
Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。
SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
論文 参考訳(メタデータ) (2025-09-25T14:05:55Z) - Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees [8.804277530769532]
State-of-art, branch and bound (BaB) は、オフ・ザ・シェルフ検証器をサブプロブレムに適用し、より優れた性能を発揮する「分別・対数」戦略である。
本稿では,これらのサブプロブレムを優先順位付けすることで,副プロブレム空間を探索する新しい検証フレームワークであるOlivaを提案する。
Olivaには2つのバリエーションがあり、例えば$OlivaGR$は、逆例を見つけやすいサブプロブレムを常に優先する欲求戦略である。
論文 参考訳(メタデータ) (2025-07-23T12:20:20Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳(メタデータ) (2025-05-17T04:16:36Z) - RCOT: Detecting and Rectifying Factual Inconsistency in Reasoning by
Reversing Chain-of-Thought [56.558892336235914]
Reversing Chain-of-Thought (RCoT) は、大規模言語モデルの推論能力を改善する新しい手法である。
RCoTは生成したソリューションにおける事実の不整合を自動的に検出し、修正する。
手書きのきめ細かいフィードバックがLLMの推論能力を大幅に向上させることを示す。
論文 参考訳(メタデータ) (2023-05-19T08:02:52Z) - Faithful Chain-of-Thought Reasoning [51.21714389639417]
CoT(Chain-of-Thought)は言語モデル(LM)のパフォーマンスを様々な推論タスクで向上させる。
翻訳と問題解決という2つの段階を含む推論フレームワークであるFithful CoTを提案する。
このことは、推論連鎖が最終回答の忠実な説明を提供することを保証している。
論文 参考訳(メタデータ) (2023-01-31T03:04:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。