ترجمه فارسی مقاله انتزاع‌های داده‌محور از طریق فرآیندهای گاوسی درخت دودویی برای تأیید رسمی

چکیده

To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.

چکیده به فارسی (ترجمه ماشینی)

برای پیشبرد تأیید رسمی سیستم های تصادفی در برابر الزامات منطق زمانی برای رسیدگی به پویایی ناشناخته ، محققان در حال طراحی رویکردهای مبتنی بر داده با الهام از پیشرفت در تکنیک های یادگیری ماشین هستند.به عنوان یکی از جهت های تحقیق امیدوار کننده ، راه حل های مبتنی بر انتزاع مبتنی بر رگرسیون فرآیند گاوسی (GP) به دلیل توانایی آنها در یادگیری بازنمایی از سیستم نهفته از داده ها با یک خطای کمی محبوب شده اند.نتایج به دست آمده بر اساس این مدل از طریق روش های مختلف به سیستم واقعی ترجمه می شود.در یک انتشار اخیر ، GPS با استفاده از یک هسته به اصطلاح درخت باینری ، سرعت چند جمله ای W.R.T.اندازه داده ها در مقایسه با نسخه وانیل آنها ، از همه تقریب های GP پراکنده موجود استفاده می کند.اتفاقاً ، فرآیند گاوسی باینری حاصل (BTGP) برای عملکردهای متوسط ​​و کواریانس خلفی ثابت آن مشخصه است ، که به طور طبیعی فضای ورودی را در پارتیشن های گسسته انتزاع می کند.در این مقاله ، ما از این انتزاع طبیعی BTGP برای تأیید رسمی استفاده می کنیم ، و نیاز به انتزاع دست و پا گیر و روش های تعیین میزان خطا را از بین می بریم.ما نشان می دهیم که BTGP به ما امکان می دهد تا یک مدل زنجیره ای از مارکوف فاصله از سیستم ناشناخته را با یک سرعت گیری که چند جمله ای W.R.T. است ، بسازیم.اندازه انتزاع در مقایسه با روشهای جایگزین.ما حتی وقتی دینامیک واقعی در فضای عملکرد BTGP زندگی نمی کند ، یک اندازه گیری خطای جدا شده را از طریق یک فرمول یکپارچه ارائه می دهیم.این به ما اجازه می دهد تا مرزهای بالا و پایین را در مورد احتمال رضایت از مشخصات دستیابی به قابلیت دسترسی که برای عدم قطعیت های آلوئوریک و معرفتی قوی هستند محاسبه کنیم.