4 ژانویه 2024 -توسط دانشگاه ماساچوست آمهرست-اعتبار: دامنه عمومی Pixabay/CC0
تیمی از دانشمندان رایانه به رهبری دانشگاه ماساچوست آمهرست اخیراً روش جدیدی را برای تولید خودکار مدارک کامل اعلام کردند که می تواند برای جلوگیری از اشکالات نرم افزاری و تأیید صحت کد زیربنایی استفاده شود.
این روش جدید که Baldur نام دارد، از قدرت هوش مصنوعی مدل‌های زبان بزرگ (LLM) استفاده می‌کند و هنگامی که با ابزار پیشرفته Thor ترکیب می‌شود، اثربخشی بی‌سابقه‌ای نزدیک به 66 درصد به دست می‌دهد. این تیم اخیراً در کنفرانس و سمپوزیوم مشترک مهندسی نرم افزار اروپایی ACM در زمینه مبانی مهندسی نرم افزار جایزه مقاله ممتاز را دریافت کرد.
یوری برون، استاد کالج اطلاعات و علوم کامپیوتر منینگ در UMass Amherst و کارشناس ارشد مقاله می‌گوید: «متاسفانه ما انتظار داریم که نرم‌افزار ما باگ داشته باشد، علی‌رغم این واقعیت که همه جا وجود دارد و همه ما هر روز از آن استفاده می‌کنیم.
تأثیرات نرم‌افزار باگ دار می‌تواند در هر نقطه‌ای از مزاحم – قالب‌بندی پر زرق و برق یا خرابی‌های ناگهانی – تا فاجعه‌بار بالقوه در موارد نقض امنیتی یا نرم‌افزار دقیق مورد استفاده برای اکتشاف فضا یا کنترل دستگاه‌های مراقبت بهداشتی باشد.
البته از زمانی که نرم افزار وجود داشته، روش هایی برای بررسی وجود داشته است. یکی از روش‌های رایج ساده‌ترین روش است: شما از یک انسان می‌خواهید که کد را خط به خط مرور کند و به صورت دستی تأیید کند که هیچ خطایی وجود ندارد. یا می توانید کد را اجرا کنید و آن را با آنچه انتظار دارید انجام دهد بررسی کنید. برای مثال، اگر انتظار دارید نرم‌افزار واژه‌پرداز شما با هر بار فشار دادن کلید «بازگشت» خط را بشکند، اما در عوض یک علامت سؤال ایجاد کند، می‌دانید که چیزی در کد اشتباه است.
مشکل هر دو روش این است که آنها مستعد خطای انسانی هستند و بررسی در برابر هر اشکال احتمالی فوق العاده وقت گیر، پرهزینه و غیرقابل اجرا برای هر چیزی جز سیستم های بی اهمیت است.
یک روش بسیار دقیق‌تر، اما سخت‌تر، تولید یک اثبات ریاضی است که نشان می‌دهد کد همان کاری را که انتظار می‌رود انجام می‌دهد، و سپس از یک اثبات‌کننده قضیه استفاده کنید تا مطمئن شوید که اثبات نیز درست است. به این روش چک کردن ماشینی می گویند.
اما نوشتن دستی این شواهد فوق العاده زمان بر است و به تخصص گسترده ای نیاز دارد. امیلی فرست، نویسنده اصلی مقاله که این تحقیق را به عنوان بخشی از پایان نامه دکترای خود در UMass Amherst به پایان رساند، می گوید: «این اثبات ها می توانند چندین برابر بیشتر از خود کد نرم افزار باشند.
با ظهور LLM ها، که ChatGPT معروف ترین نمونه آن است، یک راه حل ممکن این است که سعی کنیم چنین اثبات هایی را به صورت خودکار تولید کنیم. با این حال، برون می گوید: «یکی از بزرگترین چالش های LLM این است که همیشه درست نیستند. آنها به جای اینکه تصادف کنند و به شما بفهمانند که چیزی اشتباه است، تمایل دارند “در سکوت شکست بخورند”، پاسخی نادرست تولید می کنند اما آن را به گونه ای نشان می دهند که گویی درست است. و اغلب، بدترین کاری که می توانید انجام دهید این است که در سکوت شکست بخورید.”
اینجاست که بالدر وارد می شود.
ابتدا، تیمی که کارش را در گوگل انجام داد، از Minerva، یک LLM که بر روی مجموعه بزرگی از متن به زبان طبیعی آموزش دیده بود، استفاده کرد و سپس آن را روی 118 گیگابایت مقاله علمی ریاضی و صفحات وب حاوی عبارات ریاضی تنظیم کرد.
سپس، او LLM را بر روی زبانی به نام Isabelle/HOL که در آن برهان های ریاضی نوشته شده است، دقیق تر تنظیم کرد. سپس بالدور یک اثبات کامل ایجاد کرد و با اثبات قضیه کار کرد تا کار آن را بررسی کند. هنگامی که اثبات قضیه یک خطا را تشخیص داد، اثبات و همچنین اطلاعات مربوط به خطا را به LLM برگرداند تا بتواند از اشتباه خود درس بگیرد و یک اثبات جدید و امیدوارانه بدون خطا ایجاد کند.
این فرآیند افزایش قابل توجهی در دقت به همراه دارد. ابزار پیشرفته‌ای برای تولید خودکار اثبات‌ها، Thor نام دارد که می‌تواند در 57 درصد مواقع اثبات تولید کند. وقتی بالدور (برادر ثور، طبق اسطوره‌های نورس) با ثور جفت می‌شود، این دو می‌توانند در 65.7 درصد مواقع اثبات کنند.
اگرچه هنوز درجه زیادی از خطا وجود دارد، Baldur تا حد زیادی مؤثرترین و کارآمدترین روشی است که تاکنون برای تأیید صحت نرم افزار ابداع شده است، و همانطور که قابلیت های هوش مصنوعی به طور فزاینده ای گسترش یافته و بهبود می یابد، اثربخشی Baldur نیز باید افزایش یابد.
این مقاله به عنوان بخشی از مجموعه مقالات سی و یکمین کنفرانس مشترک مهندسی نرم افزار اروپایی ACM و سمپوزیوم در زمینه مبانی مهندسی نرم افزار منتشر شده است.
