تیمی از دانشمندان رایانه به رهبری دانشگاه ماساچوست آمهرست اخیراً روش جدیدی را برای تولید خودکار مدارک کامل اعلام کردند که می تواند برای جلوگیری از اشکالات نرم افزاری و تأیید صحت کد زیربنایی استفاده شود.
این روش جدید که 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 و سمپوزیوم مبانی مهندسی نرم افزار.
اطلاعات بیشتر:
امیلی فرست و همکاران، بالدور: نسل کامل اثبات و تعمیر با مدلهای زبان بزرگ، مجموعه مقالات سی و یکمین کنفرانس مشترک مهندسی نرم افزار اروپایی ACM و سمپوزیوم مبانی مهندسی نرم افزار (2023). DOI: 10.1145/3611643.3616243
نقل قول: محققان روش بررسی ماشینی مبتنی بر هوش مصنوعی را برای تأیید کد نرم افزار توسعه داده اند (2024، 4 ژانویه) بازیابی شده در 4 ژانویه 2024 از
این برگه یا سند یا نوشته تحت پوشش قانون کپی رایت است. به غیر از هرگونه معامله منصفانه به منظور مطالعه یا تحقیق خصوصی، هیچ بخشی بدون اجازه کتبی قابل تکثیر نیست. محتوای مذکور فقط به هدف اطلاع رسانی ایجاد شده است.