مجله علمی تفریحی بیبیس
0

دانلود استاندارد ISO/IEC 24029-2 – هوش مصنوعی (AI) – ارزیابی استحکام شبکه‌های عصبی – بخش دوم: روش‌شناسی استفاده از روش‌های رسمی

بازدید 753
  • عنوان: ISO/IEC 24029-2 – Artificial intelligence (AI) — Assessment of the robustness of neural networks — Part 2: Methodology for the use of formal methods
  • نویسنده: ISO/IEC
  • حوزه: استانداردهای هوش مصنوعی
  • سال انتشار: 2023
  • تعداد صفحه: 30
  • زبان اصلی: انگلیسی
  • نوع فایل: pdf
  • حجم فایل: 1.49 مگابایت

شبکه های عصبی به طور گسترده ای برای انجام وظایف پیچیده در زمینه های مختلف مانند پردازش تصویر یا زبان طبیعی و نگهداری پیش بینی استفاده می شوند. مدل‌های کیفیت سیستم هوش مصنوعی شامل ویژگی‌های خاصی از جمله استحکام هستند. به عنوان مثال، ISO/IEC 25059:2023، [1] که استانداردهای بین المللی SQuaRE [2] را به سیستم های هوش مصنوعی گسترش می دهد، در مدل کیفیت خود این را در نظر می گیرد که استحکام یک ویژگی فرعی قابلیت اطمینان است. نشان دادن توانایی یک سیستم برای حفظ سطح عملکرد خود در شرایط مختلف می تواند با استفاده از تجزیه و تحلیل آماری انجام شود، اما اثبات آن مستلزم نوعی تحلیل رسمی است. در این راستا روش‌های رسمی می‌توانند مکمل روش‌های دیگر به منظور افزایش اعتماد به استحکام شبکه عصبی باشند. روش‌های رسمی، تکنیک‌های ریاضی برای تعیین دقیق و تایید سیستم‌های نرم‌افزاری و سخت‌افزاری با هدف اثبات درستی آنها هستند. روش‌های رسمی را می‌توان برای استدلال رسمی در مورد شبکه‌های عصبی و اثبات اینکه آیا آنها ویژگی‌های استحکام مربوطه را برآورده می‌کنند استفاده کرد. به عنوان مثال، یک طبقه‌بندی شبکه عصبی را در نظر بگیرید که یک تصویر را به عنوان ورودی می‌گیرد و یک برچسب از مجموعه ثابتی از کلاس‌ها (مانند خودرو یا هواپیما) خروجی می‌گیرد. چنین طبقه‌بندی‌کننده‌ای را می‌توان به‌عنوان یک تابع ریاضی رسمی کرد که شدت پیکسل‌های یک تصویر را به عنوان ورودی می‌گیرد، احتمالات را برای هر کلاس ممکن از مجموعه ثابت محاسبه می‌کند و یک برچسب مربوط به بالاترین احتمال را برمی‌گرداند. این مدل رسمی می تواند برای استدلال ریاضی در مورد شبکه عصبی زمانی که تصویر ورودی اصلاح می شود استفاده شود. به عنوان مثال، فرض کنید هنگامی که به یک تصویر بتن داده می شود که شبکه عصبی برای آن برچسب “ماشین” را خروجی می دهد، می توان این سوال را پرسید: “اگر مقدار یک پیکسل دلخواه در تصویر اصلاح شود، آیا شبکه یک برچسب متفاوت تولید می کند؟” این سوال را می توان به عنوان یک گزاره ریاضی رسمی فرموله کرد که برای یک شبکه عصبی و تصویر مشخص یا درست یا نادرست است. یک رویکرد کلاسیک برای استفاده از روش های رسمی شامل سه مرحله اصلی است که در این سند توضیح داده شده است. ابتدا، سیستم مورد تجزیه و تحلیل به طور رسمی در مدلی تعریف می شود که دقیقاً تمام رفتارهای ممکن سیستم را نشان می دهد. سپس، یک نیاز به صورت ریاضی تعریف می شود. در نهایت، یک روش رسمی، مانند حل‌کننده، تفسیر انتزاعی یا بررسی مدل، برای ارزیابی اینکه آیا سیستم نیازهای داده شده را برآورده می‌کند، استفاده می‌شود، که یک اثبات، یک مثال متقابل یا یک نتیجه غیرقطعی به دست می‌دهد. این سند چندین تکنیک روش رسمی موجود را پوشش می دهد. در هر مرحله از چرخه حیات، این سند معیارهایی را ارائه می‌کند که برای ارزیابی استحکام شبکه‌های عصبی و تعیین چگونگی تأیید شبکه‌های عصبی با روش‌های رسمی قابل اجرا هستند. روش‌های رسمی می‌توانند از نظر مقیاس‌پذیری مشکلاتی داشته باشند، با این حال، آنها همچنان برای همه انواع شبکه‌های عصبی که وظایف مختلفی را بر روی چندین نوع داده انجام می‌دهند، قابل استفاده هستند. در حالی که روش‌های رسمی مدت‌هاست در سیستم‌های نرم‌افزاری سنتی مورد استفاده قرار گرفته‌اند، استفاده از روش‌های رسمی در شبکه‌های عصبی نسبتاً جدید است و هنوز یک زمینه فعال برای بررسی است. هدف این سند کمک به توسعه دهندگان هوش مصنوعی است که از شبکه های عصبی استفاده می کنند و وظیفه ارزیابی استحکام آنها را در مراحل مناسب چرخه حیات هوش مصنوعی بر عهده دارند. ISO/IEC TR 24029-1 نمای کلی تری از تکنیک های موجود برای ارزیابی استحکام شبکه های عصبی، فراتر از روش های رسمی شرح داده شده در این سند، ارائه می دهد.

Neural networks are widely used to perform complex tasks in various contexts, such as image or natural language processing and predictive maintenance. AI system quality models comprise certain characteristics, including robustness. For example, ISO/IEC 25059:2023,[1] which extends the SQuaRE International Standards[2] to AI systems, considers in its quality model that robustness is a sub-characteristic of reliability. Demonstrating the ability of a system to maintain its level of performance under varying conditions can be done using statistical analysis, but proving it requires some form of formal analysis. In that regard formal methods can be complementary to other methods in order to increase trust in the robustness of the neural network.
Formal methods are mathematical techniques for rigorous specification and verification of software and hardware systems with the goal to prove their correctness. Formal methods can be used to formally reason about neural networks and prove whether they satisfy relevant robustness properties. For example, consider a neural network classifier that takes as input an image and outputs a label from a fixed set of classes (such as car or airplane). Such a classifier can be formalized as a mathematical function that takes the pixel intensities of an image as input, computes the probabilities for each possible class from the fixed set, and returns a label corresponding to the highest probability. This formal model can then be used to mathematically reason about the neural network when the input image is modified. For example, suppose when given a concrete image for which the neural network outputs the label “car” the following question can be asked: “does the network output a different label if the value of an arbitrary pixel in the image is modified?” This question can be formulated as a formal mathematical statement that is either true or false for a given neural network and image.
A classical approach to using formal methods consists of three main steps that are described in this document. First, the system to be analyzed is formally defined in a model that precisely captures all possible behaviours of the system. Then, a requirement is mathematically defined. Finally, a formal method, such as solver, abstract interpretation or model checking, is used to assess whether the system meets the given requirement, yielding either a proof, a counterexample or an inconclusive result.
This document covers several available formal method techniques. At each stage of the life cycle, the document presents criteria that are applicable to assess the robustness of neural networks and to establish how neural networks are verified by formal methods. Formal methods can have issues in terms of scalability, however, they are still applicable to all types of neural networks performing various tasks on several data types. While formal methods have long been used on traditional software systems, the use of formal methods on neural networks is fairly recent and is still an active field of investigation.
This document is aimed at helping AI developers who use neural networks and who are tasked with assessing their robustness throughout the appropriate stages of the AI life cycle. ISO/IEC TR 24029-1 provides a more detailed overview of the techniques available to assess the robustness of neural networks, beyond the formal methods described in this document.

این کتاب را میتوانید بصورت رایگان از لینک زیر دانلود نمایید.

Download: ISO/IEC 24029-2 – Artificial intelligence (AI)

نظرات کاربران

  •  چنانچه دیدگاه شما توهین آمیز باشد تایید نخواهد شد.
  •  چنانچه دیدگاه شما جنبه تبلیغاتی داشته باشد تایید نخواهد شد.

دیدگاهتان را بنویسید

نشانی ایمیل شما منتشر نخواهد شد.

بیشتر بخوانید