論文の概要: Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems

• arxiv url: http://arxiv.org/abs/2606.23821v1
• Date: Mon, 22 Jun 2026 18:03:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-24 22:16:48.619225
• Title: Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems
• Title（参考訳）: 列車上の10桁:2つの固有値問題のAIによる検証
• Authors: Matthew J. Colbrook,
• Abstract要約: 本稿では、そのような2つの計算に関する人間-AIコラボレーションについて報告する。 特異な自己随伴シュルディンガー作用素に対して、証明された零数とディリクレ=ノイマンブラケットは、完全な負スペクトルを10個の十進点に証明する。 微妙な非正規原子分子ベンチマークでは、以前は未解決の共鳴対が分離され、各部材は10桁に囲まれている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Accurate numerical eigenvalues are often difficult to certify, especially in singular or non-normal settings. This article reports a human--AI collaboration on two such computations. For a singular self-adjoint Schrödinger operator, a verified zero count and Dirichlet--Neumann bracketing certify the complete negative spectrum to ten decimal places. For a delicate non-normal atom--molecule benchmark, a previously unresolved resonance pair is separated, with each member enclosed to ten digits. The second result is achieved not by increasing the precision of one-way shooting, but by reformulating the problem as a global matching system for projective solution lines. The infinite tail is encoded as uncertainty in the terminal projective data, and a componentwise, tail-robust Krawczyk--Brouwer inclusion supplies the certificate. This gives a reusable architecture for analytic boundary-value systems with ill-conditioned propagation and uncertain asymptotic data. The collaboration also exposes the strengths and limits of AI assistance. AI rapidly produced accurate candidates and plausible proof strategies, but several failed, including one apparently complete tail argument that omitted the componentwise check required by a nonuniform polydisc. Validated computation is a stringent test of AI-assisted mathematics: the output is not merely a number, but a number with a proof. These examples show why the proof object matters, and why human mathematical judgment remained decisive. More broadly, as AI makes code, exposition, and plausible numerical claims inexpensive, standards for verification, attribution, peer review, and training must adapt. The implications are unsettling; the opportunity is extraordinary.
• Abstract（参考訳）: 正確な数値固有値は、特に特異または非正規の設定において、証明することがしばしば困難である。 本稿では、そのような2つの計算に関する人間-AIコラボレーションについて報告する。 特異な自己随伴シュレーディンガー作用素に対して、証明された零数とディリクレ=ノイマンブラケットは、完全な負のスペクトルを10個の10個の位置まで証明する。 微妙な非正規原子分子ベンチマークでは、以前は未解決の共鳴対が分離され、各部材は10桁に囲まれている。 第2の結果は片方向射撃の精度を高めることではなく、射影解線に対するグローバルマッチングシステムとして問題を再構築することによるものである。 無限尾は終端射影データの不確実性としてエンコードされ、部品的にはテールローバストなKrawczyk--Brouwer包含が証明を提供する。 これにより、不条件な伝搬と不確定な漸近データを持つ分析境界値系に対する再利用可能なアーキテクチャが提供される。 コラボレーションはまた、AIアシストの強みと限界を公開する。 AIは、正確な候補と妥当な証明戦略を迅速に生成したが、いくつかの失敗があった。 検証された計算はAI支援数学の厳密なテストであり、出力は単なる数ではなく、証明付きの数である。 これらの例は、証明対象が重要な理由と、なぜ人間の数学的判断が決定的なままであったのかを示している。 より広い範囲で、AIがコード、説明、そしてもっともらしい数値的な主張を安くするにつれて、検証、属性、ピアレビュー、トレーニングの標準が適応しなければなりません。 その意味は不安定で、機会は並外れている。

関連論文リスト

• Characterizing initial human-AI proof formalization workflows [66.06866890889131]
  AIシステムのコード生成能力の進歩と、証明を形式化し、検証する人々の能力を変えるための高度な数学的推論の約束への関与。 我々は、AIが人々のフォーマル化に与える影響について、混合メソッド分析を行う。 質的な調査では、人々の好みは多様であるが、形式化におけるAI支援に対する一般的な欲求が示されている。
  論文  参考訳（メタデータ） (2026-06-02T22:58:19Z)
• The Deterministic Horizon: Impossibility Results as Design Specifications for Trustworthy AI Systems [0.0]
  この論文は、好奇心から不合理性の結果を設計規則に変える。 そのフラッグシップとなる結果は、アーキテクチャだけで設定された精度の高い天井を証明している。 同じ引数がサブフィールドにまたがって再キャストされる。
  論文  参考訳（メタデータ） (2026-05-21T20:48:35Z)
• The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
  AIが生成するコード品質の問題に対する業界の主要な反応は、AIレビュアーをデプロイすることだ。 本稿では,実行可能な仕様が存在しない場合,この応答は構造的に円形であると主張している。
  論文  参考訳（メタデータ） (2026-03-26T11:59:05Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities [46.111273938884295]
  本研究では,AM/GMのような既知の不等式を適用することにより,与えられた問題が単純化されることを認識するプロバーの能力について検討する。 これらの問題は人間にとって容易なままだが、Goedel、書き直し、Kimina-7Bを含むほとんどのプローバーは、かなり苦労している。 我々の結果は、現在のAIプロデューサの行動と人間の直感の間に持続的なギャップを露呈する。
  論文  参考訳（メタデータ） (2025-05-19T03:56:05Z)
• Validation tests of GBS quantum computers give evidence for quantum advantage with a decoherent target [62.997667081978825]
  複数モードデータの検証に指紋としてグループカウント確率の正P位相空間シミュレーションを用いる。 偽データを解き放つ方法を示し、これを古典的なカウントアルゴリズムに適用する。
  論文  参考訳（メタデータ） (2022-11-07T12:00:45Z)
• Complexity-Theoretic Limitations on Quantum Algorithms for Topological Data Analysis [59.545114016224254]
  トポロジカルデータ解析のための量子アルゴリズムは、古典的手法よりも指数関数的に有利である。 我々は、量子コンピュータにおいても、TDA(ベッチ数の推定)の中心的なタスクが難解であることを示します。 我々は、入力データが単純さの仕様として与えられると、指数的量子優位性を取り戻すことができると論じる。
  論文  参考訳（メタデータ） (2022-09-28T17:53:25Z)
• Neuro-Symbolic Entropy Regularization [78.16196949641079]
  構造化予測では、目的は構造化されたオブジェクトをエンコードする多くの出力変数を共同で予測することである。 エントロピー正則化(Entropy regularization)という1つのアプローチは、決定境界が低確率領域にあるべきであることを示唆している。 我々は、モデルが有効対象を確実に予測することを奨励する損失、ニューロシンボリックエントロピー正規化を提案する。
  論文  参考訳（メタデータ） (2022-01-25T06:23:10Z)

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

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