論文の概要: Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit
- arxiv url: http://arxiv.org/abs/2606.14688v1
- Date: Fri, 12 Jun 2026 17:52:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-15 16:00:43.02381
- Title: Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit
- Title(参考訳): フラッドとハーベスト:限界における言語生成のレンズによる有意義な数学を生成するためのトリビアの必要性
- Authors: Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao,
- Abstract要約: 我々は,有意義な数学の生成を,その限界においてネストされた言語生成としてモデル化する。
すべての出力は価値(H$)、自明(Fset H$)、幻覚(F$)である。
- 参考スコア(独自算出の注目度): 42.15597840680038
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: AI systems coupled to proof assistants now generate formal mathematics at scale, and the gap between what a checker can verify and what a mathematician would value has become the binding constraint. We model the generation of valuable mathematics as nested language generation in the limit: a verifiable formal language $F$, accessed through a membership oracle (the proof checker), contains an unknown valuable language $H \in \mathcal{H}$ revealed only through an adversarial enumeration of a core $C \subseteq H$ of exact density $α$ (the literature). Every output is valuable ($\in H$), trivial ($\in F \setminus H$), or a hallucination ($\notin F$). We settle four questions. First, the verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wise by Angluin's condition. Second, the verifier does buy sound coverage, covering all unseen valuable statements while asserting only valid ones: possible with it, impossible without it; it relocates unavoidable errors from false to trivial. Third, and centrally, a sharp dichotomy on the tight family: generators emitting finitely many trivia achieve optimal coverage $α/2$, while any infinite trivia allowance, even at vanishing rate, jumps the optimum to $1-α/2$ (both tight, for cores presented as the candidate intersection), and one generator attains both ends. The transition is in trivia count, not rate; the gap $1-α$ is the unrecorded mass. Fourth, both regimes instantiate in a compression model of mathematics. A perfect verifier cannot substitute for taste: the unbounded stream of correct-but-worthless statements is not an engineering accident but a provable necessity, since covering unrecorded valuable mathematics requires an infinite, but asymptotically negligible, stream of certified trivia.
- Abstract(参考訳): 証明アシスタントに結合されたAIシステムは、大規模に公式な数学を生成するようになり、チェッカーが検証できるものと数学者が値するものとの間のギャップが、バインディング制約になった。
検証可能な形式言語$F$は、メンバーシップオラクル(証明チェッカー)を通してアクセスされ、未知の貴重な言語$H \in \mathcal{H}$を含み、コアの$C \subseteq H$の正密度$α$の対数列挙によってのみ示される。
すべてのアウトプットは価値($\in H$)、自明($\in F \setminus H$)、幻覚($\notin F$)である。
私たちは4つの質問に答える。
第一に、検証者は味ではなく、幅のある生成を認めるコレクションは、正確には、アングルンの条件によって繊維的に特徴づけられる、オラクルのないモデルのものである。
第二に、検証者は音のカバレッジを購入し、有効なもののみを主張しながら、見当たらないすべてのステートメントをカバーします。
有限個のトリビアを放出するジェネレータは最適なカバレッジを最大$α/2$を達成するが、無限のトリビア許容度は消えても、最適値が1-α/2$にジャンプする(どちらも候補交点として提示されるコアに対してきつい)。
遷移はトリビア数であり、レートではなく、ギャップ1-α$は記録されていない質量である。
第4に、両体制は数学の圧縮モデルにおいてインスタンス化される。
完全検証器は、味に代わることができない: 正当だが無意味な文の非有界ストリームは、工学的な事故ではなく、証明可能な必要性である。
関連論文リスト
- Quantum Colorings of Spheres [0.0]
Sn-1$ が量子的に $n$-colorable であれば、$n=2$ または $n$ が 4 の倍数であることを示し、次数 $n$ のアダマール行列が存在するたびに逆が成り立つことを示す。
Sn-1$ が階数 1 の量子 $n$-色付けを認め、かつ、$n が 2,4,8$ である場合に限り、Zeng と Zhang の予想を定めている。
論文 参考訳(メタデータ) (2026-06-09T13:49:08Z) - Scale-Sensitive Shattering: Learnability and Evaluability at Optimal Scale [54.65053906803857]
実数値関数クラスが一様収束と学習可能性を示す最適尺度について検討する。
本研究の主な成果は,PAC学習の基本定理のスケール敏感な一般化である。
また、定量的サンプルの複雑さと評価可能性に関するオープンな質問をいくつか取り上げる。
論文 参考訳(メタデータ) (2026-05-13T15:41:30Z) - $k$-server-bench: Automating Potential Discovery for the $k$-Server Conjecture [4.29490433621832]
我々は、$k$-server予想に基づいて、自動でオープンな数学的発見のためのコードベースの挑戦を紹介する。
この課題は、単純な線形不等式からなる大きなグラフ構造系を満たすポテンシャル関数を発見することである。
以上の結果から,現在の手法の範囲内において,課題は困難である可能性が示唆された。
論文 参考訳(メタデータ) (2026-04-08T16:06:43Z) - Hardness of High-Dimensional Linear Classification [58.29089693778071]
我々は、最大半空間離散性問題に対する次元下界の新たな指数関数を確立する。
どちらも計算幾何学と機械学習の基本的問題であり、その正確で近似的な形式である。
論文 参考訳(メタデータ) (2026-03-19T15:53:41Z) - Language Generation and Identification From Partial Enumeration: Tight Density Bounds and Topological Characterizations [1.6203023551115867]
敵が未知の言語から文字列を列挙する極限における言語生成の枠組みについて検討する。
C$が$K$でより低い密度$alpha$を持つなら、アルゴリズムの出力は少なくとも$alpha/2$を達成する。
M_t$を仮定すると、最終的に$Cサブセットeq Mサブセットeq K$が満たされる。
論文 参考訳(メタデータ) (2025-11-07T14:56:04Z) - Burau representation, Squier's form, and non-Abelian anyons [53.92822954974537]
ブレイド群 $B_3$ のブラウ表現から構築した周波数可変2次元非アベリア的演算順序制御を導入する。
Squier 陽性ウィンドウの向こう側にある$Delta(omega)$の符号変更は、因果順序の交互に構成的かつ破壊的干渉を示す。
数値シミュレーションにより、拡張と抑制の両方が確認され、最小の$B_3$ブレイド制御が確立される。
論文 参考訳(メタデータ) (2025-10-21T00:25:21Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳(メタデータ) (2025-06-05T03:16:08Z) - The Aldous--Lyons Conjecture II: Undecidability [3.8370118222043694]
調整された非局所ゲームである$G$が与えられた場合、$G$が特別な種類の完全戦略を持つ場合と、$G$のすべての戦略が完璧ではない場合とを区別することは決定不可能である。
共役紙 [BCLV24] に導入された還元を用いて、この不決定性の結果はアルドゥス=リヨン予想に対する負の答えを意味する。
論文 参考訳(メタデータ) (2024-12-30T22:59:56Z) - Matrix hypercontractivity, streaming algorithms and LDCs: the large alphabet case [3.729242965449096]
We consider streaming algorithm for Approximating the value of Unique Games on a hypergraph with $t$-size hyperedges。
この値の$(r-varepsilon)$-approximationを達成する逆モデルの全てのストリーミングアルゴリズムは、$Omega(n1-2/t)$量子空間を必要とする。
論文 参考訳(メタデータ) (2021-09-06T16:56:19Z) - Quantum double aspects of surface code models [77.34726150561087]
基礎となる量子double $D(G)$対称性を持つ正方格子上でのフォールトトレラント量子コンピューティングの北エフモデルを再検討する。
有限次元ホップ代数$H$に基づいて、我々の構成がどのように$D(H)$モデルに一般化するかを示す。
論文 参考訳(メタデータ) (2021-06-25T17:03:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。