論文の概要: VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization
- arxiv url: http://arxiv.org/abs/2606.15096v1
- Date: Sat, 13 Jun 2026 04:12:25 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-16 16:21:32.841558
- Title: VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization
- Title（参考訳）: RH-隣接形式進行のためのVGPT-RSI:境界証明書、検証された有限ラガリアの不等式、明示的故障局在
- Abstract要約: 再帰的自己改善を伴う検証可能な成長物理変換器を2つのRH隣接認証タスクに適用する。
まず、領域上のパラメータ化された安全な下曲線上で、不等式に対する有限RH境界証明書を構築し、検証する。
第二に、公式なラガリア・ルート証明書を開始する。ラガリアの基準では、RHは世界的不平等と同値である。
- 参考スコア（独自算出の注目度）: 4.067416725742151
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: The Riemann Hypothesis remains one of the central unsolved problems in mathematics. Rather than claiming proof, we investigate whether a verifiable AI-assisted reasoning system can produce reliable, formally checked partial progress while explicitly identifying the remaining mathematical obstructions. We apply the Verifiable Growing Physical Transformer with Recursive Self-Improvement (VGPT-RSI) to two RH-adjacent certification tasks. First, we construct and verify a finite RH-boundary certificate for inequality on a parameterized safe lower curve over a region. The numerical boundary curve is converted into a certificate-backed lower curve, audited using outward-rounded interval arithmetic and Arb/FLINT ball arithmetic, and then checked in Rocq/CoqInterval for the parameterized theorem. Second, we initiate a formal Lagarias-route certificate. Lagarias criterion states that RH is equivalent to the global inequality. We formalize the finite quantity and produce a Coq-checked finite certificate. The final system identifies the exact unresolved mathematical bottlenecks: formalizing the Lagarias equivalence, proving the global tail theorem beyond any finite cutoff, and potentially reducing counterexamples to colossally abundant or related extremal integers. These results demonstrate that VGPT-RSI can produce certified RH-adjacent formal progress, organize proof dependencies, and avoid overclaiming when the remaining obstruction is genuinely mathematical.
- Abstract（参考訳）: リーマン仮説は数学の中心的な未解決問題の1つである。
検証可能なAI支援推論システムが、証明を主張するよりも、数学的障害を明確に識別しながら、信頼性が高く、形式的にチェックされた部分的な進展を得られるかどうかを調査する。
VGPT-RSI(Verifiable Growing Physical Transformer with Recursive Self-Improvement)を2つのRH-adjacent認証タスクに適用する。
まず、領域上のパラメータ化された安全な下曲線上で、不等式に対する有限RH境界証明書を構築し、検証する。
数値境界曲線は証明付き低曲線に変換され、外周間隔演算と Arb/FLINT 球算術を用いて監査され、パラメータ化定理のRocq/CoqInterval でチェックされる。
第二に、正式なラガリアルート証明書を開始する。
ラガリアスの基準では、RHは大域不等式と同値である。
有限量を形式化し、Coqチェックした有限証明を生成する。
ラガリアス同値性を形式化し、任意の有限カットオフを越えて大域的テール定理を証明し、反例を余剰に豊富なあるいは関連する極小整数に還元する。
これらの結果から, VGPT-RSIは, 証明されたRH依存の形式的進展を発生し, 証明依存関係を整理し, 残りの障害が真に数学的である場合の過大評価を回避できることが示唆された。
関連論文リスト
- A Reference-Free Score for Detecting Silent Reasoning Failures in Large Language Models [1.0602247913671219]
Reasoning Answer Faithfulness Score (RAFS) は、出力された数学的トレースが局所的に信頼できるかどうかの基準自由なインスタンスレベルの診断である。
RAFSは、ステップの妥当性、解答の推論と反ファクトの感度、解答のコンセンサス、条件付き推論安定性を組み合わせている。
RAFSは、数学的な解答精度を、サイレント推論の失敗と解答の誤りに対する監査可能な警告信号で補完することを目的としている。
論文 参考訳（メタデータ） (2026-07-28T07:28:38Z) - Domain-Validity-Gated Metamorphic Testing of Scientific ML Surrogates [6.691613382732758]
本研究では,SciMLサロゲートの候補準同型関係をドメインの有効性を検証し,実行可能なテストアセットに変換する方法について検討する。
本稿では,演算子の数値フロアに耐性が支配的であり,前提条件が保たれている場合にのみ,候補を許容する領域正当性を提案する。
証拠は2つのCFDタスクと第2のPDEファミリーにまたがり、候補MRから監査可能なSciMLテストアセットへの妥当性を認識可能なブリッジをサポートする。
論文 参考訳（メタデータ） (2026-06-16T05:13:05Z) - Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
本稿では,文脈条件付き言語モデル行動を検証するためのモデル理論フレームワークを開発する。
有限コンテキスト証明書、ペアセパレータのヒットセット、クエリ教育のディメンション、プロンプト保存基準、スケール制限証人を提供する。
論文 参考訳（メタデータ） (2026-05-30T14:07:58Z) - Value Functions as Supermartingale Certificates [48.922124609307566]
適切な報酬の下では、$$-regularプロパティをほぼ確実に満足するポリシーに関連する値関数が、その仕様のStreet Supermartingale証明書を符号化していることを示す。
我々の結果は有限マルコフ決定過程で実験的に検証され、有限で数え切れないほど無限で連続的な状態空間を保ち、RLによる証明書合成への原則的経路を示唆している。
論文 参考訳（メタデータ） (2026-05-29T16:39:02Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - Exact Structural Abstraction and Tractability Limits [0.0]
正確な正確性は、誘導されたクラス $s sim_R simation' iff MathrmAdm_R(s)$ にのみ依存する。
決定、探索、近似、統計的、ランダム化された地平線、分布保証は全て同じ商-回復問題に還元される。
論文 参考訳（メタデータ） (2026-04-08T17:59:47Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Towards Evading the Limits of Randomized Smoothing: A Theoretical
Analysis [74.85187027051879]
決定境界を複数の雑音分布で探索することにより,任意の精度で最適な証明を近似できることを示す。
この結果は、分類器固有の認証に関するさらなる研究を後押しし、ランダム化された平滑化が依然として調査に値することを示す。
論文 参考訳（メタデータ） (2022-06-03T17:48:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。