دانلود مقاله شبکه های عصبی در سیستم های حلقه بسته
چکیده
رویکردهای یادگیری ماشین بطور موفق برای خلق مولفه های کنترل با عملکرد بالا در سیستمهای رایا-فیزیکی مورد استفاده قرار گرفته اند و در آنها، دینامیک کنترل از ترکیب چند زیرسیستم بدست می آید. ولی ممکن است این رویکردها فاقد اعتبار لازم برای تضمین کاربرد معتبرشان در بافتی با ایمنی حیاتی باشند. ما در این مقاله، ترکیبی از تکنیکهای صحت سنجی اثبات قضیه و حساب بازه ای برای تحلیل ویژگیهای ایمنی در سیستمهای حلقه بسته که مولفه های شبکه عصبی را در برمیگیرند پیشنهاد میدهیم. ما کاربرد رویکرد پیشنهادی مان برای یک کنترلر پیش بینی کنندۀ مدل در رانندگی اتومات را شرح داده و عملکرد صحت سنجی شبکه عصبی را با سایر ابزارهای موجود مقایسه میکنیم. نتایج نشان میدهند که عملکرد صحت سنجی شبکه عصبی حلقه باز با کمک تکنیک حساب بازه ای در اثبات ویژگیها با سربار زمانی کوچکتر، بهتر از سایر رویکردهای موجود است. ما همچنین قابلیت ترکیب دو رویکرد را برای ساختن یک مدل رسمی از شبکه در منطق مرتبه بالاتر سیستم کنترل شده در یک حلقه بسته شرح میدهیم.
1-مقدمه
سیستمهای رایا-فیزیکی (CPS) (Alur, 2015) ترکیبی از الگوریتمهای محاسباتی و مولفه های فیزیکی هستند که همچون سیستمهای حلقه بسته تعامل میکنند. در دورنمای فعلی از CPS، ادغام شبکه های عصبی، روز به روز رواج بیشتری پیدا میکند (Rathore et.al., 2021)، که قابلیتهای این سیستمها در حوزه های گوناگونی مثل شبکه های هوشمند، تولید هوشمند (Huang et.al., 2021)، وسایل نقلیه خودکار (AV) (Cococcioni et.al., 2021; Rossi et.al., 2024)، اتوماسیون صنعتی (Bernardeschi et.al., 2023)، پزشکی و غیره را تغییر میدهد.
یک رویکرد کلان، استفاده از محاسبات عصبی برای قسمت کنترلر CPSهاست که قابلیتهای مدلیابی و پذیرش را افزایش میدهد (Antsaklis, 1990; Emami et.al., 2022; Jin et.al., 2018). همچنین شبکه های عصبی برای تولید مولفه های CPS جایگزین بکار میروند. برای مثال، در مطالعه Song و دیگران (2024)، محققان یک طرح کنترل با قابلیت تحمل خطا بر مبنای یک شبکه عصبی برای یک وسیله نقلیه هوایی بی سرنشین چهار موتوره پیشنهاد داده اند. همچنین در مطالعه Song و دیگران (2023)، محققان یک رویکرد کوانتش در قبال کنترل شبکه عصبی برای سیستمهای غیرخطی پیشنهاد داده اند. کاربرد بالقوه دیگر یادگیری ماشین برای تحلیل سریهای زمانی، نگهداری و تعمیرات پیشگویانه ماشین آلات میباشد (Putnik et.al., 2021). همچنین شبکه های عصبی بازگشتی (RNN) و تکنیکهای حافظه کوتاه مدت – بلندمدت (LSTM) از طریق بررسی داده های آنی بدست آمده از حسگرهای سامانه فیزیکی، برای تشخیص ناهنجاری بکار میروند (Jeffrey et.al., 2023). محققان در مطالعه Vereno et.al., 2023 از یادگیری تقویتی به همراه شبیه سازی همزمان یک سیستم شبکه هوشمند و نیز از معماریهای مجزایی برای ادغام شبکه برق و سیستم AI استفاده کرده اند. استفاده از مولفه های شبکه عصبی در CPS با ایمنی حیاتی، نگرانی درباره ایمنی و قابلیت اتکا آنها را افزایش میدهد.
8- نتیجه گیری
ما در اینجا یک رویکرد نوین صحت سنجی را معرفی کردیم که از نقاط قوت حساب بازه ای و تکنیک صحت سنجی رسمی اثبات قضیه بهره میبرد. این ترکیب، چارچوب معتبری برای تضمین ایمنی و پایایی شبکه های عصبی در سیستمهای حلقه بسته ارائه میدهد.
رویکرد ما بطور یکدست و بی نقص با چارچوب یادگیری عمیق PyTorch ادغام میشود و بدون ایجاد تغییراتی عمده در روند کار فعلی پذیرفته میشود. و به ما امکان میدهد یک سیستم حلقه بسته از یک سامانه کروز کنترل تطبیقی فرمالیزه کنیم که در آن، کنترلر پیش بینی کننده با یک شبکه عصبی آموزش دیده جایگزین میشود. سرانجام ما توانستیم شرایط ایمنی متغیر کنترل شده با سیستم را شناسایی و صحت سنجی کنیم.
رویکرد ما اصلاحات چشمگیری در بازدهی صحت سنجی ایجاد کرده، و بطور قابل توجهی سربار زمانی را در مقایسه با سایر رویکردهای پیشرفته کاهش داده است. کارهای بعدی شامل بهینه سازی روش حساب بازه ای هستند که محدودیتهای رویکرد فعلی را از طریق محدودسازی تخمین دست بالای نتیجه، تا حد ممکن کاهش داده و سرعت محاسبات بازه ای را از طریق GPU افزایش میدهند. همچنین توسعه بیشتر این مطالعه، دینامیک دقیقتری از وسایل نقلیه، مثل مدلسازی رفتار در PVS را با مجموعه ای از معادلات دیفرانسیل، جهت بررسی سناریوهای پیچیده تر شرح خواهد داد.
Abstract
Machine Learning approaches have been successfully used for the creation of high-performance control components of cyber–physical systems, where the control dynamics result from the combination of many subsystems. However, these approaches may lack the trustworthiness required to guarantee their reliable application in a safety-critical context. In this paper, we propose a combination of interval arithmetic and theorem-proving verification techniques to analyze safety properties in closed-loop systems that embed neural network components. We show the application of the proposed approach to a model-predictive controller for autonomous driving comparing the neural network verification performance with other existing tools. The results show that open-loop neural network verification through interval arithmetic can outperform existing approaches proving properties with a smaller time overhead. Furthermore, we demonstrate the capability of combining the two approaches to construct a formal model of the network in higher-order logic of the controlled system in a closed-loop.
1. Introduction
Cyber–physical systems (CPS) (Alur, 2015) are a combination of computational algorithms and physical components that interact as closed-loop systems. In the current landscape of CPS neural network integration is becoming more and more common (Rathore et al., 2021), changing the capabilities of these systems in various fields including smart grids, smart manufacturing (Huang et al., 2021), autonomous vehicles (AVs) (Cococcioni et al., 2021, Rossi et al., 2024), industrial automation (Bernardeschi et al., 2023), medical, and more.
A widespread approach is to apply neural computing to the controller part of CPSs, increasing modeling and adaptation capabilities (Antsaklis, 1990, Emami et al., 2022, Jin et al., 2018). Neural networks are also applied for the generation of surrogated components of CPSs. For example, in Song et al. (2024) authors proposed a neural-network based, fault-tolerant control design for a quadrotor unmanned aerial vehicle. Furthermore, in Song et al. (2023) authors proposed a quantization approach to neural network control for non-linear systems. Another potential application of machine learning to time-series analysis is predictive maintenance for machinery (Putnik et al., 2021). Furthermore, by examining real-time data from the physical system’s sensors, recurrent neural networks (RNN) and long short-term memory (LSTM) techniques can be utilized to carry out anomaly detection (Jeffrey et al., 2023). The authors of Vereno et al. (2023) used reinforcement learning in conjunction with the co-simulation of a smart grid system; they used separate architectures for the power grid integration and the AI system. The use of neural network components in safety-critical CPS, however, raises concerns about their dependability and safety.
8. Conclusion
We introduced a novel verification approach that leverages the strengths of interval arithmetic and theorem-proving formal verifica- tion technique. This combination provides a robust framework for ensuring the safety and reliability of neural networks in closed-loop systems.
Our approach seamlessly integrates with the PyTorch deep learn- ing framework, ensuring that it can be adopted without significant changes to existing workflows. This allowed us to formalize a closed- loop system of an adaptive cruise control application where the model- predictive controller was replaced by a well-trained neural network. Finally, we were able to specify and verify safety requirements on the system-controlled variable.
Our approach demonstrated significant improvements in verifica- tion performance, considerably reducing the time overhead when com- pared to other state-of-the-art approaches. Future works will include the optimization of the interval arithmetic method mitigating the lim- itations of the approach by constraining the overapproximation of the result and accelerating interval computation through GPU as much as possible. Moreover, further expansions of this work will add more detailed dynamics of the vehicle including modeling the behavior in PVS with a set of differential equations to consider more complex scenarios.
(جهت بزرگ نمایی روی عکس کلیک نمایید)
چکیده
1-مقدمه
2- مطالعات مرتبط
ابزار مبتنی بر نظریه صدق پذیری در پیمانه (SMT)
نظریه ماشینهای خودکار ترکیبی
رویکرد مبتنی بر شبیه سازی
اثبات کننده های رسمی
مجموعه بازه و انتشار مقید
3- پیشینه
3.1- زبان PVS
3.2- شبکه عصبی
3.3- چارچوب PyTorch
4- صحت سنجی تحلیلی با کمک حساب بازه ای
5- تبدیل شبکه های عصبی به مدلهای رسمی
5.1- مشخصات شبکه
5.2- قیود و ویژگیهای شبکه
6- ادغام شدن درون PyTorch
6.1- تولید خودکار نظریه
6.2- محاسبات حساب بازه ای
6.3- یک مثال کوچک از دو تکنیک
6.4- محدودیتهای تولید و اثبات نظریه PVS
7- مورد کاربردی: سامانه کروز کنترل تطبیقی با سیستم کنترل جایگزین
7.1- مدلیابی و اثبات ویژگیها برای شبکه عصبی
ویژگی ایمنی: فاصله ایمن بین دو خودرو
7.2- ارزیابی کرانهای شبکه عصبی
7.3- صحت سنجی حلقه بسته
7.4- محدودیتها و مقیاس پذیری رویکرد
8- نتیجه گیری
منابع
Abstract
1. Introduction
2. Related works
Satisfiability modulo theory (SMT) based tools.
Hybrid automata.
Simulation-based.
Formal provers.
Interval-sets and bound propagation.
3. Background
3.1. PVS language
3.2. Neural network
3.3. PyTorch
4. Analytical verification using interval arithmetic
5. Translation of neural networks to formal models
5.1. Network specification
5.2. Network constraints and properties
6. Integration inside PyTorch
6.1. Automatic theory generation
6.2. Interval arithmetic computation
6.3. A small example of the two techniques
6.4. Limits of the PVS theory generation and proof
7. Use case: adaptive cruise control with surrogated controller
7.1. Modeling and proving properties for the neural network
Safety property: safety distance between the two cars.
7.2. Evaluation of the neural network bounds
7.3. Closed-loop verification
7.4. Limitations and scalability of the approach
8. Conclusion
Acknowledgments
Data availability
References
این محصول شامل پاورپوینت ترجمه نیز می باشد که پس از خرید قابل دانلود می باشد. پاورپوینت این مقاله حاوی 27 اسلاید و 6 فصل است. در صورت نیاز به ارائه مقاله در کنفرانس یا سمینار می توان از این فایل پاورپوینت استفاده کرد.
در این محصول، به همراه ترجمه کامل متن، یک فایل ورد ترجمه خلاصه نیز ارائه شده است. متن فارسی این مقاله در 13 صفحه (2100 کلمه) خلاصه شده و در داخل بسته قرار گرفته است.
علاوه بر ترجمه مقاله، یک فایل ورد نیز به این محصول اضافه شده است که در آن متن به صورت یک پاراگراف انگلیسی و یک پاراگراف فارسی درج شده است که باعث می شود به راحتی قادر به تشخیص ترجمه هر بخش از مقاله و مطالعه آن باشید. این فایل برای یادگیری و مطالعه همزمان متن انگلیسی و فارسی بسیار مفید می باشد.
بخش مهم دیگری از این محصول لغت نامه یا اصطلاحات تخصصی می باشد که در آن تعداد 50 عبارت و اصطلاح تخصصی استفاده شده در این مقاله در یک فایل اکسل جمع آوری شده است. در این فایل اصطلاحات انگلیسی (تک کلمه ای یا چند کلمه ای) در یک ستون و ترجمه آنها در ستون دیگر درج شده است که در صورت نیاز می توان به راحتی از این عبارات استفاده کرد.
- ترجمه فارسی مقاله با فرمت ورد (word) با قابلیت ویرایش و pdf بدون آرم سایت ای ترجمه
- پاورپوینت فارسی با فرمت pptx
- خلاصه فارسی با فرمت ورد (word)
- متن پاراگراف به پاراگراف انگلیسی و فارسی با فرمت ورد (word)
- اصطلاحات تخصصی با فرمت اکسل