論文の概要: Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation
- arxiv url: http://arxiv.org/abs/2609.33066v1
- Date: Sun, 27 Sep 2026 00:56:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-06 10:48:39.432223
- Title: Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation
- Title（参考訳）: 境界ダイナミクスによるゼロストレージ手続き型ニューラル合成:リーン4の形式的検証とベアメタルガントレット検証
- Abstract要約: WERR(Waves & Errors)と第III相軌道誤差ダイナミクス(OED)の形式的検証とベアメタル的実証について述べる。
我々はベクトル化された36ビットCPUカーネルプロセスの評価を6.49秒で10,000の判定(15,397の判定/s,0バイトVRAM,15.15倍の高速化)。
我々は、Mathlib4 と 0 の未証明予想 (sorry): $mathcalI_3 = 0,3,6 の部分集合 mathbbZ を証明して、Lean 4 (v4.34.1) において 10 つの機械検証定理を確立する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Contemporary neural inference architectures rely on dense floating-point weight matrices stored in high-bandwidth memory (VRAM), incurring severe memory-wall bottlenecks and preventing native execution inside deterministic virtual machines like the Ethereum Virtual Machine (EVM). Verifying termination and arithmetic invariants for recursive dynamical systems over continuous domains is generally undecidable in the Blum-Shub-Smale model. Here, we present the formal verification and bare-metal empirical validation of WERR (Waves & Errors) and Phase III Orbital Error Dynamics (OED), a non-tensor decision paradigm that procedurally synthesizes non-linear decision boundaries on demand from a 24-byte coordinate seed $Θ= (c_x, c_y, \text{zoom})$ along the boundary of the Mandelbrot set ($\partial\mathcal{M}$). By projecting the recurrence $z_{n+1} = z_n^2 + c$ onto the modular residue ring $\mathbb{Z}/9\mathbb{Z}$ and the fixed-point domain $\mathbb{Q}_{16.16}$, we establish ten machine-verified theorems in Lean 4 (v4.34.1) with Mathlib4 and zero unproven conjectures (sorry): proving $\mathcal{I}_3 = \{0,3,6\} \subset \mathbb{Z}/9\mathbb{Z}$ ideal closure, universal fuel-bounded halting ($\le 9$ and $\le 12$ steps), absence of $\mathbb{Q}_{16.16}$ square overflow below $2^{63}-1$, non-constant boundary escape sensitivity, and a parametric EVM gas bound ($\le 22,557 \le 24,000$ gas). Evaluated on a 40-core Dual Intel Xeon server, the vectorized 36-iteration CPU kernel processes 100,000 decisions in 6.49 s (15,397 decisions/s, 0 Bytes VRAM, 15.15x speedup), while a sigmoidal outlier gate suppresses 100.00% of adversarial spikes while preserving 89.60% of clean baseline signals.
- Abstract（参考訳）: 現代の神経推論アーキテクチャは、高帯域メモリ(VRAM)に格納された密度の浮動小数点重み行列に依存しており、深刻なメモリウォールボトルネックを引き起こし、Ethereum仮想マシン(EVM)のような決定論的仮想マシン内でネイティブな実行を防止する。
連続領域上の再帰的力学系に対する終端と算術不変性を検証することは、一般にBlum-Shub-Smaleモデルでは決定できない。
ここでは, WERR(Waves & Errors)とOED(Phase III Orbital Error Dynamics)の形式的検証と, 24 バイト座標のシード=(c_x, c_y, \text{zoom})$から要求に応じて非線形決定境界を手続き的に合成する非テンソル決定パラダイム)をマンデルブロット集合(\partial\mathcal{M}$)の境界に沿って行う。
z_{n+1} = z_n^2 + c$ をモジュラー剰余環 $\mathbb{Z}/9\mathbb{Z}$ と固定点領域 $\mathbb{Q}_{16.16}$ に射影することにより、マドリブ4 と 0 の未証明予想 (sorry: proving $\mathcal{I}_3 = \{0,3,6\} \subset \mathbb{Z}/9\mathbb{Z}$ 理想的な閉包、普遍燃料結合停止$\le 9$ と $\le 12$ のステップなし、$\mathbb{Q}_{16.16}$ 263$ 以上の263$ 1 以下のフロー、$2,63$ 以上のフロー、$2,5,54,000 の非可測性(英語版)を持つ 10 個の機械検証定理をリーン 4 (v4.34.1) とゼロ不証明予想 (sorry): proving $\mathcal{I}_3 = \{0,3,6\subset \mathbb{Z}/9\mathbb{Z}$ で表す。
40コアのDual Intel Xeonサーバで評価され、ベクトル化された36個のCPUカーネルは6.49 s (15,397 s/s, 0 Bytes VRAM, 15.15x スピードアップ)で10,000の判定を処理する。
関連論文リスト
- On the SoS Certifiability of Log-Concave Distributions [51.56484100374058]
圏 $(Cm)m|v|m - mathbbE_Xsim Plangle X,vranglem$ は、すべての偶数 mge2$ に対する平方の和であり、$C>0$ は普遍定数である。
これにより、コタリとシュタインハルト(arXiv:1711.07465)の定理におけるポアンカレ定数への依存を排除し、対数凹面分布の最適モーメント境界を回復する。
論文 参考訳（メタデータ） (2026-09-24T16:48:02Z) - $p$-Form Gauge Dynamics and Digital Quantum Simulation -- Flux and Cosmological Constant Neutralization [0.0]
I developed a Hamiltonian framework for $mathbb Z_k$ $p$-form gauge field on arbitrary oriented cell complex。
私はp=2, k=2$に特化しており、磁気3セル項が欠落しており、一形式ガウス法則を正確に解くことができる。
論文 参考訳（メタデータ） (2026-07-12T22:57:37Z) - From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification [0.0]
ポスト量子暗号(PQC)ハードウェアにおけるマスキングの形式的検証は、有限領域上のSMTソルバに依存する。
我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。
構造依存分析フレームワークであるQANaryは、Adams Bridge ML-DSA/ML-KEMアクセラレーターの30モジュールにわたる117万の細胞を検証した。
論文 参考訳（メタデータ） (2026-04-20T18:17:22Z) - Collective Kernel EFT for Pre-activation ResNets [0.20625936401496234]
有限幅ディープニューラルネットワークでは、経験的カーネル$G$が層間で進化する。
プリアクティベーション ResNets のための集合カーネル有効場理論 (EFT) を$G$のみのクロージャ階層に基づいて開発し,その有限クロージャウィンドウの診断を行う。
論文 参考訳（メタデータ） (2026-04-17T06:31:50Z) - INC: An Indirect Neural Corrector for Auto-Regressive Hybrid PDE Solvers [61.84396402100827]
本稿では,学習した補正を支配方程式に統合する間接ニューラルコレクタ(mathrmINC$)を提案する。
$mathrmINC$は、$t-1 + L$の順番でエラー増幅を減らし、$t$はタイムステップ、$L$はリプシッツ定数である。
大規模なベンチマークで$mathrmINC$をテストし、1Dカオスシステムから3D乱流まで、多くの異なる解法、神経バックボーン、テストケースをカバーした。
論文 参考訳（メタデータ） (2025-11-16T20:14:28Z) - Information-Computation Tradeoffs for Noiseless Linear Regression with Oblivious Contamination [65.37519531362157]
このタスクに対する効率的な統計的クエリアルゴリズムは、VSTATの複雑さを少なくとも$tildeOmega(d1/2/alpha2)$で要求する。
論文 参考訳（メタデータ） (2025-10-12T15:42:44Z) - Deep neural networks can provably solve Bellman equations for Markov decision processes without the curse of dimensionality [3.6185342807265415]
離散時間最適制御問題と漏洩決定プロセス(MDP)は、不確実性の下でのシーケンシャルな意思決定の基本的なモデルである。
本稿では、無限時間地平線と有限制御セット$A$を持つMDPに関連する$Q$関数に対するディープニューラルネットワーク(DNN)近似を構築する。
論文 参考訳（メタデータ） (2025-06-28T11:25:44Z) - A Unified Framework for Uniform Signal Recovery in Nonlinear Generative
Compressed Sensing [68.80803866919123]
非線形測定では、ほとんどの先行結果は一様ではない、すなわち、すべての$mathbfx*$に対してではなく、固定された$mathbfx*$に対して高い確率で保持される。
本フレームワークはGCSに1ビット/一様量子化観測と単一インデックスモデルを標準例として適用する。
また、指標集合が計量エントロピーが低い製品プロセスに対して、より厳密な境界を生み出す濃度不等式も開発する。
論文 参考訳（メタデータ） (2023-09-25T17:54:19Z) - Random matrices in service of ML footprint: ternary random features with
no performance loss [55.30329197651178]
我々は、$bf K$ の固有スペクトルが$bf w$ の i.d. 成分の分布とは独立であることを示す。
3次ランダム特徴(TRF)と呼ばれる新しいランダム手法を提案する。
提案したランダムな特徴の計算には乗算が不要であり、古典的なランダムな特徴に比べてストレージに$b$のコストがかかる。
論文 参考訳（メタデータ） (2021-10-05T09:33:49Z) - Naive Exploration is Optimal for Online LQR [49.681825576239355]
最適後悔尺度は$widetildeTheta(sqrtd_mathbfu2 d_mathbfx T)$で、$T$は時間ステップの数、$d_mathbfu$は入力空間の次元、$d_mathbfx$はシステム状態の次元である。
我々の下界は、かつての$mathrmpoly(logT)$-regretアルゴリズムの可能性を排除する。
論文 参考訳（メタデータ） (2020-01-27T03:44:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。