論文の概要: Probabilistic Model Checking of Autoregressive Neural Sequence Models

• arxiv url: http://arxiv.org/abs/2609.00838v1
• Date: Tue, 01 Sep 2026 07:37:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-02 16:31:36.437274
• Title: Probabilistic Model Checking of Autoregressive Neural Sequence Models
• Title（参考訳）: 自己回帰型ニューラルシーケンスモデルの確率論的モデル検査
• Authors: Helge Spieker, Dennis Gross, Arnaud Gotlieb,
• Abstract要約: 自己回帰型ニューラルシークエンスモデルをデプロイする上で問題となる2つの問題に対して、テストセットの精度は静かである。 テスト対象のシステムの質量は、サンプリング時に到達可能な制約違反の代替品にどの程度の確率があるか。 確率論的モデル検査で両方答える。
• 参考スコア（独自算出の注目度）: 4.570003973862485
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models: how much probability mass the system under test (SUT) places on constraint-violating alternatives that are reachable under sampling and what fraction of the input population satisfies a domain requirement. We answer both with probabilistic model checking. The pipeline extracts a discrete-time Markov chain (DTMC) from the SUT's token-by-token generation, verifies formal PCTL specifications with the PRISM model checker, and aggregates the per-input verdicts into a coverage curve over the input space. A soundness theorem establishes the DTMC as an under-approximation, so every verdict yields a certified interval on the SUT's true reachability probability. The coverage built from those verdicts is, therefore, conservative by construction. A counterexample-guided abstraction refinement (CEGAR) loop adaptively tightens the interval, and a maximum-likelihood algorithm extracts the most probable falsifying trace. Two case studies exercise the pipeline. On a GPT-2 computer-aided process-planning (CAPP) model with 100% test accuracy, the pipeline quantifies the probability mass greedy decoding hides, but that is reachable with sampling; and identifies the smallest training fraction at which an ordering requirement holds population-wide, neither of which test accuracy can report. We then verify the SMILES molecular generator with a 50x larger vocabulary. The only change is an external chemical-validity oracle, and the pipeline identifies the gap between structural completeness and chemical validity.
• Abstract（参考訳）: 自動回帰ニューラルシークエンスモデルをデプロイする際に問題となる2つの問題 - テスト対象のシステム(SUT)がサンプリング時に到達可能な制約違反の代替品にどの程度の確率質量を配置するか、入力された人口のどの部分がドメイン要件を満たすか。 確率論的モデル検査で両方答える。 パイプラインは、SUTのトークン・バイ・トーケン世代から離散時間マルコフ連鎖(DTMC)を抽出し、PRISMモデルチェッカーで正式なPCTL仕様を検証し、入力空間上のカバレッジ曲線に入力毎の判定を集約する。 健全性定理はDTMCを過度近似として確立するので、全ての判定はSUTの真の到達可能性確率の証明された区間を生じる。 これらの評決から得られた範囲は、建設によって保守的である。 反例誘導抽象改善(CEGAR)ループは、インターバルを適応的に締め付け、最大形アルゴリズムは、最も可能性の高いファルシファイリングトレースを抽出する。 2つのケーススタディがパイプラインを練習します。 GPT-2コンピュータ支援プロセスプランニング(CAPP)モデルにおいて、100%の精度で、パイプラインは確率質量グレディ復号の隠蔽を定量化するが、サンプリングにより到達可能である。 次に、SMILES分子発生器を50倍の語彙で検証する。 唯一の変化は外部の化学価オラクルであり、パイプラインは構造的完全性と化学的妥当性の間のギャップを識別する。

関連論文リスト

• EDGE: a closed-form directed test for the calibration of probabilistic binary classifiers [0.0]
  本稿では,正規確率分類器の校正テストであるEDGEを提案し,ロジスティック回帰法を提案する。 EDGEは、同一のビン付き予測観測テーブルを信頼性図のプロットとして読み出し、その標準化されたビン残差をスムーズなキャリブレーション歪みの小さな前提に投影する。 リンクと特徴の相違により、既定のデフォルトが22のシナリオのうち、19のシナリオで全ての競合するビン付きテストに導かれるか、あるいは結び付けられ、再適合ベースのStukelスコアテストが20%から28%のサンプルで分離される場合、計算可能のままであった。
  論文  参考訳（メタデータ） (2026-08-20T19:06:05Z)
• Auditing Question-Order Effects in Large Language Models with the QQ Equality: Mechanism Characterization and a Saturation Caveat [4.07636450847048]
  人間の調査回答者はQQ(量子質問)平等を満たす質問順序効果を示す。 自己回帰的大言語モデルの逐次判断のための監査基準としてQQ等式を開発する。
  論文  参考訳（メタデータ） (2026-07-19T12:22:06Z)
• When RLVR Shrinks the Reasoning Boundary: Diagnosing Pass@k Inversion [0.0]
  検証可能な報酬(RLVR)を用いた強化学習は、繰り返しサンプリング時にモデルを悪化させながら、一サンプル精度を向上させることができる。 トレーニング後、このポリシーはベースモデルよりも小さな問題を、大きな$k$で解決する可能性がある。 失敗は境界プロンプトに集中しており、ベースモデルにはサンプリングによって回復できる稀な正しい軌道が含まれており、有限のRLVRロールアウトグループに確実に現れるには小さすぎる。
  論文  参考訳（メタデータ） (2026-07-12T17:17:18Z)
• Federated Language Models Under Bandwidth Budgets: Distillation Rates and Conformal Coverage [12.805268849262243]
  集中できない帯域制限ノードに散在するデータに基づいて言語モデルを訓練することは、臨床ネットワーク、企業知識基盤、科学コンソーシアムで発生する設定である。 ノード間でデータを分散し続けなければならない状況について検討し、明示的な帯域幅予算の下では、何の統計的保証が得られるのかを問う。
  論文  参考訳（メタデータ） (2026-05-11T05:01:43Z)
• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。 各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。 これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
  論文  参考訳（メタデータ） (2026-04-20T13:25:40Z)
• Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
  完全証明を軽量なサンプリングベースアプローチで置き換える検証フレームワークとプロトコルを提案する。 我々は,機能的に異なるモデル間のトレース分離を活用可能な条件を定式化し,検証可能な推論プロトコルの安全性について議論する。 我々の手法は、最先端の暗号証明システムと比較して、証明時間を桁違いに削減する。
  論文  参考訳（メタデータ） (2026-03-19T15:24:27Z)
• Large Language Models Are Bad Dice Players: LLMs Struggle to Generate Random Numbers from Statistical Distributions [50.1404916337174]
  大規模言語モデル(LLM)における母国語の確率的サンプリングの大規模,統計的に活用された最初の監査について述べる。 バッチ生成は, ほぼ完全に崩壊する一方, 中央値のパスレートが13%であり, 統計的妥当性はわずかであることがわかった。 現在のLCMには機能的な内部サンプルが欠如しており、統計的保証を必要とするアプリケーションに外部ツールを使う必要があると結論付けている。
  論文  参考訳（メタデータ） (2026-01-08T22:33:12Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  複合イベント認識(CER)システムは、イベントのリアルタイムストリーム上のパターンを"即時"検出する能力によって、過去20年間に人気が高まっている。 このような現象が実際にCERエンジンによって検出される前に、パターンがいつ発生するかを予測する方法が不足している。 複雑なイベント予測の問題に対処しようとする形式的なフレームワークを提案する。
  論文  参考訳（メタデータ） (2021-09-01T09:52:31Z)
• Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model [50.38446482252857]
  本稿では、生成モデル(シミュレータ)へのアクセスを想定して、強化学習のサンプル効率について検討する。 最初に$gamma$-discounted infinite-horizon Markov decision process (MDPs) with state space $mathcalS$ and action space $mathcalA$を考える。 対象の精度を考慮すれば,モデルに基づく計画アルゴリズムが最小限のサンプルの複雑さを実現するのに十分であることを示す。
  論文  参考訳（メタデータ） (2020-05-26T17:53:18Z)

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

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