論文の概要: Neural Proofs for Sound Verification and Control of Complex Systems

• arxiv url: http://arxiv.org/abs/2512.18389v1
• Date: Sat, 20 Dec 2025 15:01:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-23 18:54:32.314834
• Title: Neural Proofs for Sound Verification and Control of Complex Systems
• Title（参考訳）: 複雑系の音響検証と制御のためのニューラル証明
• Authors: Alessandro Abate,
• Abstract要約: この非公式な貢献は、音響証明の構築に対する新しいアプローチを追求している研究の進行中のラインを示す。 証明可能な正確なポリシ/ストラテジー/コントローラを生成することができ、ニューラル証明書と合わせて、興味のあるモデルの所定の仕様を正式に達成することができる。
• 参考スコア（独自算出の注目度）: 64.97409769546992
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.
• Abstract（参考訳）: この非公式なコントリビューションは、動的システムの複雑な確率モデル、反応プログラム、より一般的にはサイバー物理システムのモデルの形式的検証と制御のための音響証明の構築に対する新しいアプローチを追求している。 ニューラル証明は2つの重要な構成要素から構成される。 1 利害関係のモデルに関する一般時的仕様の検証に係る要件を規定する証明規則及び 2a)モデルのダイナミックスからサンプルにアクセスし、それに従ってニューラルネットワークをトレーニングし、2b)モデルの完全な知識を活用するSAT-modulo-theory (SMT)クエリを介してそのようなネットワークを一般化する。 複雑な確率的モデルに対する逐次決定問題の文脈では、証明可能な正しいポリシー/戦略/制御子、すなわち、ニューラル証明書と組み合わせて、興味のあるモデルの所定の仕様を正式に達成する状態フィードバック関数を生成できる。

関連論文リスト

• KBQA-R1: Reinforcing Large Language Models for Knowledge Base Question Answering [64.62317305868264]
  テキスト模倣から強化学習によるインタラクション最適化へパラダイムをシフトするフレームワークである textbfKBQA-R1 を提案する。 KBQAを多ターン決定プロセスとして扱うことで,行動のリストを用いて知識ベースをナビゲートすることを学ぶ。 WebQSP、GrailQA、GraphQuestionsの実験では、KBQA-R1が最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-12-10T17:45:42Z)
• Learning from Imperfect Data: Robust Inference of Dynamic Systems using Simulation-based Generative Model [4.430997638097218]
  本研究では,動的システムに対する高精度かつロバストな推論を可能にするシミュレーションに基づく不完全データ生成モデル(SiGMoID)を提案する。 我々は、SiGMoIDがデータノイズを定量化し、システムパラメータを推定し、観測されていないシステムコンポーネントを推測することを示した。
  論文  参考訳（メタデータ） (2025-07-15T00:56:21Z)
• Certified Neural Approximations of Nonlinear Dynamics [51.01318247729693]
  安全クリティカルな文脈では、神経近似の使用は、基礎となるシステムとの密接性に公式な境界を必要とする。 本稿では,認証された一階述語モデルに基づく新しい,適応的で並列化可能な検証手法を提案する。
  論文  参考訳（メタデータ） (2025-05-21T13:22:20Z)
• Fuzzy Recurrent Stochastic Configuration Networks for Industrial Data Analytics [3.8719670789415925]
  本稿では,ファジィリカレント構成ネットワーク(F-RSCN)と呼ばれる新しいニューロファジィモデルを提案する。 提案したF-RSCNは,複数の貯留層によって構成され,各貯留層は高木・スゲノ・カン(TSK)ファジィ則に関連付けられている。 TSKファジィ推論システムをRCCNに統合することにより、F-RSCNは強力なファジィ推論能力を有し、学習と一般化の両面での音響性能を実現することができる。
  論文  参考訳（メタデータ） (2024-07-06T01:40:31Z)
• Constructing Neural Network-Based Models for Simulating Dynamical Systems [59.0861954179401]
  データ駆動モデリングは、真のシステムの観測からシステムの力学の近似を学ぼうとする代替パラダイムである。 本稿では,ニューラルネットワークを用いた動的システムのモデル構築方法について検討する。 基礎的な概要に加えて、関連する文献を概説し、このモデリングパラダイムが克服すべき数値シミュレーションから最も重要な課題を概説する。
  論文  参考訳（メタデータ） (2021-11-02T10:51:42Z)
• Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning [49.6928533575956]
  我々は、神経系1と論理系2の間を仲介するために神経推論を用いる。 強靭なストーリー生成とグラウンドド・インストラクション・フォローリングの結果、このアプローチは神経系世代におけるコヒーレンスと精度を高めることができることを示した。
  論文  参考訳（メタデータ） (2021-07-06T17:59:49Z)
• The Role of Isomorphism Classes in Multi-Relational Datasets [6.419762264544509]
  アイソモーフィックリークは,マルチリレーショナル推論の性能を過大評価することを示す。 モデル評価のためのアイソモーフィック・アウェア・シンセサイティング・ベンチマークを提案する。 また、同型類は単純な優先順位付けスキームによって利用することができることを示した。
  論文  参考訳（メタデータ） (2020-09-30T12:15:24Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。 このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。 その結果,音のBCsを最大2桁の速度で合成できることがわかった。
  論文  参考訳（メタデータ） (2020-07-07T07:39:42Z)

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

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