ریاضیات و محاسبه
عددها، اثباتها، گرافها و ماشینها، که با محاسبه و نیز با استنتاج بررسی میشوند.
ریاضیات و علوم رایانه اکنون ایدههایشان را با شبیهسازی میآزمایند. میلیونها گراف تصادفی تولید میکنند تا ببینند چه چیزی معمول است. ماشینی را اجرا میکنند تا ببینند یک الگوریتم واقعاً چه میکند. بارها به یک رمز حمله میکنند تا بدانند چگونه شکست میخورد. هیچکدام جهان فیزیکی را توصیف نمیکند. فضای اعداد، ساختارها و محاسبات را خودشان کاوش میکنند. این رویه از ریاضیات تجربی که قرنها با دست انجام میشد تا ابزارهای راستیآزمایی امروزی را شامل میشود که پیش از ساخت، طرح را در برابر هر حالت دستیافتنی وارسی میکنند.
آزمایشهای ماتریس تصادفی
ماتریسهای بزرگ پر از اعداد تصادفی که بارها قطری میشوند تا آمار مقادیر ویژهشان مطالعه شود.
پرسشی که پاسخ میدهد: مقدارهای ویژهٔ یک ماتریس تصادفی به چه الگویی میرسند، و آیا با شاخههای دیگر ریاضی و فیزیک میخواند؟
کنار میگذارد: همیشه فقط گوشهای ریز از فضای بینهایت ماتریسهای ممکن را نمونه میگیرد.
اجرا میشود روی: حدود 1012 FLOPS تقریبی خوشهٔ یک دانشگاه که ماتریسهای بزرگ بسیاری را میسازد و قطری میکنداز: 1955 کار اولیهٔ Wigner دربارهٔ آمار مقدارهای ویژهٔ ماتریس تصادفی
آزمایشهای گراف تصادفی
گرافهایی که با یک قاعدهٔ تصادفی، گرهبهگره یا یالبهیال، ساخته میشوند تا دیده شود چه ویژگیهایی، مثل همبندی یا خوشهبندی، معمولاً پدید میآیند.
پرسشی که پاسخ میدهد: یک شبکهٔ «معمولی» با این قاعدهٔ افزودن گره و یال چه شکلی دارد؟
کنار میگذارد: شبکههای دنیای واقعی بهندرت به تمیزیِ قاعدهای هستند که مدل را تولید میکند.
اجرا میشود روی: حدود 1010 FLOPS تقریبی روی یک رایانهٔ رومیزی برای گرافهایی تا میلیونها گره اجرا میشوداز: 1959 مدل گراف تصادفی اردوش و رنی
شبیهسازی تراوش
شبکهای که جایگاهها یا پیوندهایش تصادفی باز میشوند، و لحظهای که مسیری پیوسته ناگهان کل سامانه را درمینوردد زیر نظر است.
پرسشی که پاسخ میدهد: در چه چگالیای شبکهای تصادفی ناگهان سرتاسر به هم پیوسته میشود؟
کنار میگذارد: شبکههای آرمانی از هر مادهٔ متخلخل یا شبکهٔ واقعی تمیزتر رفتار میکنند.
اجرا میشود روی: حدود 1010 FLOPS تقریبی رایانهای رومیزی برای جاروبهای بزرگ شبکهایاز: 1957 معرفی نظریهٔ تراوش توسط برودبنت و همرزلی
جستوجوهای ریاضیات تجربی
جستوجوی عددیِ فراگیر (brute force) برای الگوها، مثالهای نقض یا رابطههای دقیق میان اعداد، بسیار فراتر از آنچه با دست قابل وارسی باشد.
پرسشی که پاسخ میدهد: آیا این حدس برای هر موردی که کسی توان بررسیاش را دارد درست است و آیا الگویی پدید میآید؟
کنار میگذارد: هیچ شمار موارد وارسیشدهای اثبات نیست، هرچند بسیاری برقرار بمانند.
اجرا میشود روی: حدود 1011 FLOPS تقریبی خوشهٔ یک دانشگاه که روزها روی یک جستوجو اجرا میشوداز: 1963 تا 1963، جستوجوهای رایانهای برای رابطههای صحیح و الگوهای اعداد اول
برآورد ثابتها با مونتکارلو
نمونهگیری تصادفی برای برآورد یک ثابت یا انتگرال ریاضی، مثل پاشیدن نقطهها برای برآورد مساحت، بهعنوان تمرین نه برای یک مدل فیزیکی.
پرسشی که پاسخ میدهد: نمونهگیری تصادفی کورکورانه بهتنهایی چقدر دقیق میتواند یک کمیت ریاضی را مشخص کند؟
کنار میگذارد: از تقریباً هر روش عددی پیشرفتهتری بسیار کندتر همگرا میشود.
اجرا میشود روی: حدود 109 FLOPS تقریبی روی یک لپتاپ در ثانیه تا دقیقه اجرا میشوداز: 1946 ایدهٔ Ulam در 1946؛ von Neumann در مارس 1947 نسخهای برای رایانهٔ الکترونیکی پیشنهاد کرد، و روش نخستین بار در 1949 منتشر شد منبعدر درخت شبیهسازیها: روش مونتکارلو
جستوجوهای محاسباتی نظریهٔ اعداد
اعداد بزرگی که از نظر اولبودن آزموده، تجزیه، یا برای ویژگیهای خاص مثل اعداد کامل جستوجو میشوند، با الگوریتمهایی که در مقیاس بزرگ اجرا میشوند نه با دست.
پرسشی که پاسخ میدهد: آیا این عدد بسیار بزرگ ویژگیای را که میجوییم دارد، و جستوجو تا کجا میتواند رکورد را پیش ببرد؟
کنار میگذارد: جستوجوهای رکوردشکن دربارهٔ عددهایی که هنوز کسی به بررسیشان فکر نکرده چیز کمی میگویند.
اجرا میشود روی: حدود 1013 FLOPS تقریبی پروژهٔ محاسبات داوطلبانهٔ توزیعشده روی ماشینهای اهدایی بسیاراز: 1951 آزمون دستی لوکاس برای اعداد اول مرسن، که نخستینبار در 1951 با رایانه اجرا شد
عددیسازی جاذب آشوبناک
مجموعهای کوچک از معادلات غیرخطی که گامبهگام انتگرال گرفته میشود تا وابستگی حساس به شرایط اولیه و یک جاذب فراکتالی آشکار شود.
پرسشی که پاسخ میدهد: چرا یک سامانهٔ قطعی ساده غیرقابل پیشبینی میشود؟
کنار میگذارد: گرد کردن عددی یعنی یک مسیر طولانی مدار حقیقی نیست، فقط مداری است که به یک مدار حقیقی نزدیک میماند.
اجرا میشود روی: حدود 103 FLOPS تقریبی چند معادله، چند ثانیه روی یک لپتاپ.از: 1963 جریان قطعی نادورهای لورنتس، یک مدل همرفت که روی رایانه اجرا شد. منبعدر درخت شبیهسازیها: همرفت آشوبناک Lorenz
آزمایشهای شبکهٔ ناخطی
زنجیرهای از جرمها با فنرهای غیرخطی که از یک مد شروع میشود و دنبال میشود تا ببینیم انرژی همانطور که ترمودینامیک پیشبینی میکند بهطور یکنواخت پخش میشود یا نه.
پرسشی که پاسخ میدهد: آیا زنجیرهٔ غیرخطی انرژیاش را بهطور یکنواخت میان همهٔ حرکتهایش پخش میکند؟
کنار میگذارد: نتایج به زنجیرهٔ برگزیده و حالت اولیه بستگی دارند.
اجرا میشود روی: حدود 103 FLOPS تقریبی با معیارهای امروز ریز؛ نمونهٔ اصلی چند ده جرم داشت.از: 1955 مطالعات فرمی، پاستا و اولام دربارهٔ مسئلههای غیرخطی روی یک رایانهٔ دیجیتال اولیه. منبع
آزمایشهای عددی سالیتون
معادلهٔ موج غیرخطی روی یک شبکه حل میشود تا دیده شود تپها از میان هم میگذرند و شکل خود را نگه میدارند، کاری که موجهای خطی نمیکنند.
پرسشی که پاسخ میدهد: چرا برخی موجهای غیرخطی بیتغییر از هم میگذرند؟
کنار میگذارد: یک خانواده از معادلات را نشان میدهد، نه رفتار عمومی موجهای ناخطی را.
اجرا میشود روی: حدود 104 FLOPS تقریبی یک شبکهٔ یکبعدی، امروز ناچیز.از: 1965 برهمکنش سالیتونها در پلاسمای بیبرخورد و بازگشت حالتهای آغازین از Zabusky و Kruskal. منبع
رندر مجموعهٔ فراکتالی
فرمولی تکراری و ساده که در هر نقطه از صفحهٔ مختلط آزموده میشود تا ببینیم میگریزد یا نه، و مرز مجموعهٔ نقاط پایدار را میکشد.
پرسشی که پاسخ میدهد: شکل مجموعهای که در آن یک تکرار ساده کراندار میماند چیست؟
کنار میگذارد: آزمونهای گریز فقط عضویت را القا میکنند، و تصویر نمونهبرداری با تفکیک متناهی از مجموعهای با جزئیات بینهایت است.
اجرا میشود روی: حدود 109 FLOPS تقریبی بزرگنماییهای عمیق به تکرار با دقت گسترده در میلیونها نقطه نیاز دارند.از: 1980 جنبههای فراکتالی ماندلبرو از تکرار z به λz(1-z)، نخستین تصاویر رایانهای مجموعهٔ ماندلبرو. منبع
بحرانیت خودسازمانیافتهٔ تپهٔ شن
دانههایی که روی یک شبکه ریخته میشوند و وقتی شیب زیاد شود فرو میریزند. این کار بدون هیچ تنظیمی بهمنهایی در هر اندازه میدهد و الگویی است از اینکه سامانهها چگونه به حالت بحرانی میرسند.
پرسشی که پاسخ میدهد: چرا بهمنهایی در هر اندازه بدون هیچ تنظیمی پدید میآیند؟
کنار میگذارد: اینکه سامانههای واقعی همین مقیاسبندی را دارند یا نه، محل مناقشه است.
اجرا میشود روی: حدود 109 FLOPS تقریبی اجراهای طولانی روی شبکههای بزرگ برای دیدن مقیاسپذیری.از: 1987 بحرانیت خودسازمانیافته از باک، تانگ و ویزنفلد: توضیحی برای نوفهٔ 1/f. منبع
محاسبهٔ صفرهای زتای ریمان
مقدارهای تابع زتا در امتداد خط بحرانیاش محاسبه میشوند تا صفرهایش پیدا و شمرده شوند، و وارسی شود که همانجایی هستند که فرضیه میگوید.
پرسشی که پاسخ میدهد: آیا همهٔ صفرهای نابدیهی تابع زتا روی یک خط قرار دارند؟
کنار میگذارد: هیچ وارسی متناهی، هر قدر هم بلند، نمیتواند ثابت کند که فراتر از آن صفری خارج از خط وجود ندارد.
اجرا میشود روی: حدود 1018 FLOPS تقریبی چند دهه زمان پردازنده در بزرگترین جستوجوها.از: 1953 محاسبات تورینگ از تابع زتای ریمان. منبع
ارقام عدد پی با رایانه
سریهای پی تا شمار عظیمی رقم با حساب دقیق جمع میشوند، که هم عدد و هم ماشین را میآزماید.
پرسشی که پاسخ میدهد: آیا ارقام عدد پی تصادفی به نظر میرسند، و آیا در این مقیاس میتوان به ماشین اعتماد کرد؟
کنار میگذارد: ارقام به هیچ پرسش بازی پاسخ نمیدهند، و وارسیها خطای سختافزار را فقط وقتی میگیرند که روش مستقل باشد.
اجرا میشود روی: حدود 1017 FLOPS تقریبی ماهها روی یک سرور برای صدها تریلیون رقم.از: 1950 تعیین پی و e تا بیش از 2000 رقم اعشار با انیاک، از ریتوایزنر (منتشرشده در 1950، بازچاپشده در Pi: A Source Book). منبع
کشف حدس با راهنمایی هوش مصنوعی
یادگیری ماشین روی جدولهای بزرگی از اشیای ریاضی مییابد کدام ویژگیها به هم پیوندند، تا حدسی پیشنهاد کند که ریاضیدانان سپس میکوشند اثباتش کنند.
پرسشی که پاسخ میدهد: کدام رابطهٔ دیدهنشده میان این کمیتهای ریاضی ارزش اثبات دارد؟
کنار میگذارد: فقط الگوها را پیشنهاد میکند و خودش چیزی را ثابت نمیکند، و برخی نظمهای داده ممکن است پیامد شیوهٔ ساختهشدن دادهها باشند.
اجرا میشود روی: حدود 1015 FLOPS تقریبی چند روز روی چند GPU برای هر مجموعهداده.از: 2021 پیشبرد ریاضیات با هدایت شهود انسانی توسط هوش مصنوعی، از دیویس و همکارانش. منبع
جستوجوی الگوریتم و ساختار آموختهشده
سامانهای بازیکننده یا مبتنی بر مدل زبانی رویهها یا اشیای ریاضی تازه را میجوید، و رایانه درستی هر نامزد را وارسی میکند.
پرسشی که پاسخ میدهد: آیا برنامه میتواند الگوریتمی سریعتر یا نمونهای بزرگتر از آنچه آدمها یافتهاند کشف کند؟
کنار میگذارد: هر نتیجه یک نمونهٔ تازهٔ تنهاست، و جستوجو فقط انواع اشیایی را میپوشاند که طراحانش بهصورت بازی قاببندی کردهاند.
اجرا میشود روی: حدود 1017 FLOPS تقریبی چند روز تا چند هفته روی خوشههای شتابدهنده.از: 2022 AlphaTensor فوزی و همکارانش، کشف الگوریتمهای سریعتر ضرب ماتریس با یادگیری تقویتی. منبع
وارسی مدل
هر حالت دستیافتنی یک سامانهٔ متناهی، مثل پروتکل یا طرح مدار، با رایانه برشمرده میشود تا وارسی شود ویژگیای در همهٔ آنها برقرار است.
پرسشی که پاسخ میدهد: آیا حالتی دستیافتنی هست که این طراحی در آن قواعد خودش را بشکند؟
کنار میگذارد: فضاهای حالت از آنچه قابل وارسی است بسیار بزرگتر میشوند، پس طرحهای واقعی ابتدا ساده میشوند.
اجرا میشود روی: حدود 1012 FLOPS تقریبی خوشهٔ یک دانشگاه که فضای حالتی بزرگ اما کراندار را بهطور کامل میکاوداز: 1981 معرفی وارسی مدل توسط کلارک و امرسون
جستوجوی اثبات خودکار قضیه
جستوجو در زنجیرههای استنتاج منطقی که رایانه گامبهگام تولید میکند، برای یافتن اثبات یا رد یک گزارهٔ ریاضی.
پرسشی که پاسخ میدهد: آیا زنجیرهٔ معتبری از گامهای منطقی از بدیهیات تا این گزاره وجود دارد؟
کنار میگذارد: اثباتی مییابد که هیچ انسانی نمیگزیند، و گاهی هیچ اثباتی در دسترس نیست.
اجرا میشود روی: حدود 1011 FLOPS تقریبی خوشهٔ یک دانشگاه که ساعتها تا روزها جستوجو میکنداز: 1956 Logic Theorist، یک برنامهٔ اولیهٔ جستجوی اثبات خودکار
SAT و حل قید
میلیونها ترکیب از مقادیر درست یا نادرست که بهطور نظاممند جستوجو میشوند تا مجموعهٔ بزرگی از قیدهای منطقی برآورده شود، برای زمانبندی، مسیریابی یا راستیآزمایی طرحها.
پرسشی که پاسخ میدهد: آیا تخصیصی از مقادیر هست که همهٔ این قیدها را همزمان برآورده کند؟
کنار میگذارد: برخی نمونهها آنقدر سختاند که هیچ حلگری، هرچقدر خوب، بهموقع تمامشان نمیکند.
اجرا میشود روی: حدود 1011 FLOPS تقریبی از یک ایستگاه کاری تا یک خوشه، بسته به اندازهٔ مسئلهاز: 1962 روش دیویس-پاتنم برای جستجوی ارضاپذیری
مدلسازی حملهٔ رمزنگاری
یک رمز یا طرح تبادل کلید که در شبیهسازی میلیونها بار حمله میشود، با جستوجوی فراگیر، سوگیری آماری یا یک ضعف مدلشده، تا سنجیده شود شکستنش واقعاً چهقدر تلاش میخواهد.
پرسشی که پاسخ میدهد: شکستن این واقعاً به چند عملیات نیاز دارد و آیا آن عدد هنوز با اطمینان بزرگ است؟
کنار میگذارد: فقط حملههایی را میآزماید که تحلیلگر به مدلکردنشان فکر کرده بود، نه حملهای که هیچکس هنوز نیافته است.
اجرا میشود روی: حدود 1014 FLOPS تقریبی خوشهای توزیعشده از ماشینهای بسیار که آزمایشهای حمله را اجرا میکنداز: 1976 تا 1976، تحلیل محاسباتی استحکام رمز و تبادل کلید
شبیهسازی نشت کانال جانبی
توان مصرفی، زمانبندی یا تابش الکترومغناطیسی یک دستگاه هنگام اجرای یک عملیات رمزنگاری مدل میشود، تا معلوم شود شنوندهای بیرونی از آن چه میفهمد.
پرسشی که پاسخ میدهد: چقدر از کلید رمز از رفتار فیزیکی دستگاه، نه ریاضیات، بیرون میزند؟
کنار میگذارد: شرایط آزمایشگاه سیگنالهایی تمیزتر میگیرد از آنچه یک دستگاه واقعی پرنویز معمولاً بروز میدهد.
اجرا میشود روی: حدود 1010 FLOPS تقریبی ایستگاه کاری که ردّ توان یا زمانبندی یک دستگاه را مدل میکنداز: 1996 نمایش حملههای زمانی به پیادهسازیهای رمزنگاری توسط کوکر
راستیآزمایی پروتکل امنیتی
هر پیامی که مهاجم میتواند در یک پروتکل ارتباطی بفرستد، بازپخش یا جعل کند، با رایانه برشمرده میشود تا وارسی شود میتوان رازی یا هویتی را از آن بیرون کشید یا نه.
پرسشی که پاسخ میدهد: آیا دنبالهای از پیامها میتواند این پروتکل را فریب دهد که رازی را فاش کند یا هویتی جعلی را بپذیرد؟
کنار میگذارد: پروتکل را همانطور که مشخص شده راستیآزمایی میکند، نه میانبرهایی که یک پیادهسازی واقعی میزند.
اجرا میشود روی: حدود 1011 FLOPS تقریبی ایستگاه کاری تا یک خوشه که فضای پیامهای یک پروتکل را وارسی میکنداز: 1989 مدل دولف-یائو، پایهای بنیادین برای راستیآزمایی پروتکل
اثبات رایانهیار با وارسی تمام حالتها
قضیهای که به فهرستی متناهی از حالتها فروکاسته میشود و هر کدام با برنامه راستیآزمایی میشود، چون هیچ انسانی نمیتواند همه را بررسی کند.
پرسشی که پاسخ میدهد: آیا اثبات را میتوان با ماشینی که هر حالت را وارسی میکند کامل کرد؟
کنار میگذارد: اعتماد به برنامه، سختافزار و استدلال کاهش حالتها منتقل میشود.
اجرا میشود روی: حدود 109 FLOPS تقریبی حدود هزار ساعت روی رایانهٔ بزرگ برای نسخهٔ اصلی؛ امروز بسیار کمتر.از: 1977 اثبات اپل و هاکن که هر نقشهٔ مسطح چهاررنگپذیر است، با کاهشپذیریِ وارسیشده با رایانه. منبع
محاسبات عددی تأییدشده
محاسبههایی با کرانهای تضمینشده، تا نتیجهای عددی گزارهای ریاضی را ثابت کند، مثل وجود جاذب آشوبناک.
پرسشی که پاسخ میدهد: آیا جواب محاسبهشده را میتوان درست اثبات کرد، نه فقط احتمالاً دقیق؟
کنار میگذارد: کرانها در زمانهای بلند میتوانند منفجر شوند، و اثباتها را به مسئلههای کوتاه یا خوشرفتار محدود میکنند.
اجرا میشود روی: حدود 109 FLOPS تقریبی حساب بازهای هزینه را با ضریبی اندک ضرب میکند.از: 2002 حلگر دقیق ODE از Tucker و مسئلهٔ شمارهٔ 14 Smale، که وجود جاذب لورنز را اثبات کرد. منبع
شمارش ماشینهای تورینگ
هر برنامهٔ کوچک یک ماشین کمینه اجرا میشود تا دیده شود کدامها متوقف میشوند و کدام برای همیشه میدوند، تا طولانیترین برنامهٔ متوقفشونده از هر اندازه یافت شود.
پرسشی که پاسخ میدهد: یک برنامهٔ کوچک پیش از توقف تا کی میتواند اجرا شود؟
کنار میگذارد: تصمیمناپذیری یعنی برخی ماشینها را هرگز نمیتوان ردهبندی کرد، هرچقدر هم اجرا شوند.
اجرا میشود روی: حدود 1015 FLOPS تقریبی میلیاردها ماشین، با اثبات برای آنهایی که متوقف نمیشوند.از: 1965 مطالعات رایانهای لین و رادو دربارهٔ مسائل ماشین تورینگ. منبع
وارسی مدل آماری
سامانهای با رفتار تصادفی که بارها شبیهسازی میشود تا با اطمینان برآورد شود که چقدر احتمال دارد ویژگیای را نقض کند.
پرسشی که پاسخ میدهد: یک سامانهٔ تصادفی چقدر احتمال دارد یک قاعدهٔ ایمنی را بشکند؟
کنار میگذارد: اجراهای آماری احتمال را با یک سطح اطمینان میدهند، نه اثبات، و شکستهای نادر به نمونهبرداری اهمیتی نیاز دارند.
اجرا میشود روی: حدود 109 FLOPS تقریبی هزاران تا میلیونها اجرای نمونهبرداریشده.از: 2002 راستیآزمایی احتمالاتی سامانههای رویداد گسسته با نمونهبرداری پذیرش از Younes و Simmons. منبع
آزمون فازی (fuzz)
برنامهای با شمار عظیمی از ورودیهای تصادفی یا جهشیافته تغذیه میشود تا آنهایی که آن را از کار میاندازند پیدا شوند؛ در واقع شبیهسازی جهانی خصمانه یا بیدقت.
پرسشی که پاسخ میدهد: چه ورودیای این نرمافزار را از کار میاندازد؟
کنار میگذارد: فقط خرابیهایی را مییابد که ورودیهای تصادفی به آنها میرسند، و برنامهای میتواند سالها آزمون را پس بدهد در حالی که باگی را پشت یک حالت نادر پنهان کرده است.
اجرا میشود روی: حدود 1014 FLOPS تقریبی سالماشین زمان پردازنده برای یک پایگاه کد بزرگ.از: 1990 پژوهش تجربی میلر، فردریکسن و سو دربارهٔ قابلیت اطمینان ابزارهای یونیکس. منبع
اجرای نمادین
برنامهای با ورودیهای نامعلومِ نوشتهشده بهصورت نماد اجرا میشود، شرطهای هر مسیر جمع میشود و حلگر مقادیری مییابد که هر شاخه را طی کنند.
پرسشی که پاسخ میدهد: کدام ورودیها هر مسیر این برنامه را اجرا میکنند، و آیا هیچکدام به یک اشکال میرسد؟
کنار میگذارد: تعداد مسیرها با اندازهٔ برنامه بهصورت نمایی رشد میکند، پس برنامههای بزرگ فقط بخشی پوشش داده میشوند.
اجرا میشود روی: حدود 1012 FLOPS تقریبی ساعت زمان حلکننده برای هر برنامه، که با شمار مسیرها بهشدت رشد میکند.از: 1976 اجرای نمادین و آزمون برنامه از کینگ. منبع
تفسیر انتزاعی
برنامهای روی مجموعهای از مقدارهای ممکن مثل بازهها، بهجای مقدارهای تکی، اجرا میشود تا ویژگیهایی ثابت شود که برای هر ورودی برقرارند.
پرسشی که پاسخ میدهد: آیا ممکن است این برنامه برای ورودیای بر صفر تقسیم کند یا سرریز شود؟
کنار میگذارد: تقریب ایمن هشدار کاذب میدهد، پس مردم باید باز هم هر هشدار را بررسی کنند.
اجرا میشود روی: حدود 1011 FLOPS تقریبی ساعت روی یک ایستگاه کاری برای یک پایگاه کد بزرگ هوانوردی.از: 1977 تفسیر انتزاعی کوزو و کوزو، مدلی یکپارچهٔ شبکهای برای تحلیل ایستای برنامهها. منبع
وارسی مدل کراندار
رفتار یک طرح تا تعداد معینی گام بهصورت فرمول منطقی نوشته و به یک حلگر ارضاپذیری داده میشود تا هر مسیر کوتاه تا یک اشکال را پیدا کند.
پرسشی که پاسخ میدهد: آیا این مدار یا برنامه میتواند در تعداد معینی گام به حالت خطا برسد؟
کنار میگذارد: فراتر از کران گامها چیزی را ثابت نمیکند، مگر استدلالی جداگانه نشان دهد کافی است.
اجرا میشود روی: حدود 1013 FLOPS تقریبی ساعت روی یک سرور برای هر ملک.از: 1999 وارسی مدل نمادین بدون BDD از بیره، چیماتی، کلارک و ژو. منبع
آزمون تصادفی مبتنی بر ویژگی
قاعدهای که باید همیشه برقرار باشد بیان میشود، و رایانه موردهای تصادفی بسیاری میسازد و هر شکست را به یک مثال نقض کوچک کاهش میدهد.
پرسشی که پاسخ میدهد: آیا این کد در گسترهٔ وسیعی از ورودیها از مشخصات خودش پیروی میکند؟
کنار میگذارد: موارد تصادفی ممکن است هرگز به یک شرط نادر نرسند، و ویژگی نوشتهشده ممکن است آنی نباشد که اهمیت دارد.
اجرا میشود روی: حدود 109 FLOPS تقریبی دقیقه روی یک لپتاپ برای هزاران مورد.از: 2000 QuickCheck کلاسن و هیوز، ابزاری سبک برای آزمون تصادفی برنامههای Haskell. منبع
راستیآزمایی شبکهٔ عصبی
حلگرهای قید ثابت میکنند که برای هر ورودی در یک ناحیه، خروجی شبکهٔ عصبی در کرانها میماند، بهجای آزمودن نمونهها.
پرسشی که پاسخ میدهد: آیا تغییری کوچک در یک ورودی میتواند شبکه را به پاسخ غلط وادارد؟
کنار میگذارد: اثباتها فقط به شبکههای کوچک مقیاس میپذیرند و مجموعهٔ اختلالهایی که میتوان بررسی کرد باریک است.
اجرا میشود روی: حدود 1013 FLOPS تقریبی ساعت تا روز روی یک سرور برای یک شبکهٔ کوچک.از: 2017 Reluplex از کاتز و همکارانش، یک حلکنندهٔ SMT برای راستیآزمایی شبکههای عصبی عمیق. منبع
شبیهسازی معماری رایانه
خط لولهٔ پردازندهٔ پیشنهادی، حافظههای نهان و پیشبین شاخه، دستورالعملبهدستورالعمل مدل میشود تا سرعت تراشه پیش از ساخته شدن برآورد شود.
پرسشی که پاسخ میدهد: طرح این پردازنده پیش از آنکه سیلیکونی بریده شود، برنامههای واقعی را با چه سرعتی اجرا میکند؟
کنار میگذارد: آنقدر از تراشهٔ واقعی را ساده میکند که سیلیکون نهایی همیشه کمی با مدل فرق دارد.
اجرا میشود روی: حدود 1011 FLOPS تقریبی خوشهٔ یک دانشگاه که برنامههای محک را از مدل میگذرانداز: 1990 تا 1990، شبیهسازهای دقیقاً چرخهبهچرخهٔ پردازنده برای پژوهش معماری
شبیهسازی سامانههای توزیعشده و اجماع
رایانههای بسیاری که با تأخیر، افت و خرابی برای هم پیام میفرستند تا آزمون شود آیا یک الگوریتم توزیعشده هنوز بر پاسخ درست توافق میکند.
پرسشی که پاسخ میدهد: آیا این الگوریتم وقتی پیامها گم یا دیر میشوند یا گرهها از کار میافتند هنوز به توافق درست میرسد؟
کنار میگذارد: خرابیهای تزریقشده همانهاییاند که طراح پیشبینی کرده بود، نه آنهایی که در تولید ناگهان پدید میآیند.
اجرا میشود روی: حدود 1010 FLOPS تقریبی خوشهای که صدها گره مجازی را شبیهسازی میکنداز: 1978 کار اولیهٔ لمپورت دربارهٔ ترتیب و خرابی در سامانههای توزیعشده
شبیهسازی سامانههای ذخیرهسازی
دیسکها، درایوها و سامانههای پرونده از نظر نحوهٔ چیدن داده، خرابی و بازیابی مدل میشوند، تا طرح ذخیرهسازی پیش از خرید و پر کردن درایوهای واقعی آزموده شود.
پرسشی که پاسخ میدهد: این طرح ذخیرهسازی در مقیاسی که آزمودن واقعیاش گران است چه عملکردی دارد و چگونه از خرابی جان به در میبرد؟
کنار میگذارد: درایوهای واقعی با شیوههایی درهمتر و همبستهتر از نرخ خرابی تصادفی مدل خراب میشوند.
اجرا میشود روی: حدود 1010 FLOPS تقریبی از یک ایستگاه کاری تا یک خوشهٔ کوچک که یک آرایهٔ ذخیرهسازی را مدل میکنداز: 1988 تا 1988، مدلهای شبیهسازی پایایی آرایهٔ دیسک
شبیهسازی زمانبند سیستمعامل
جریانی از وظایف محاسباتی که مدل میشود و میرسند و بر سر یک پردازنده رقابت میکنند، و با قواعد زمانبندی گوناگون اجرا میشود تا معلوم شود کدام عادلانهترین یا سریعترین است.
پرسشی که پاسخ میدهد: کدام روش ترتیبدادن صف کارها بیشترین کار را انجام میدهد، یا برای همهٔ کارها منصفانهتر است؟
کنار میگذارد: بارهای کاری مصنوعی بهندرت با ترکیب نامنظم کارهایی که یک ماشین واقعی میبیند همخوانی دارند.
اجرا میشود روی: حدود 109 FLOPS تقریبی روی یک لپتاپ یا ایستگاه کاری در ثانیه تا دقیقه اجرا میشوداز: 1968 تا 1968، مطالعات شبیهسازی سیاستهای زمانبندی پردازنده
جستوجوی بهینهسازی کامپایلر و برنامه
شمار عظیمی از تغییرهای کوچک یک تکه کد آزموده و اندازهگیری میشود، تا سریعترین یا کوتاهترین نسخهای که همان کار را میکند یافت شود.
پرسشی که پاسخ میدهد: از میان همهٔ شیوههای همارز نوشتن این تکه کد کوچک، کدام واقعاً سریعترین است؟
کنار میگذارد: برنامههای یافتشده گاهی آنقدر غیرعادیاند که هیچ توضیحی برای اینکه چرا کار میکنند در دست نیست.
اجرا میشود روی: حدود 1010 FLOPS تقریبی خوشهای که فضای بزرگی از گونههای کد را جستوجو میکنداز: 2006 تا 2006، جستوجوی ابربهینهسازی روی دنبالههای کوتاه دستور
آزمون تجربی عملکرد الگوریتم
الگوریتمی که هزاران بار روی ورودیهای تصادفی یا واقعی با اندازهٔ فزاینده اجرا میشود و اینکه زمان اجرایش واقعاً چگونه رشد میکند اندازه گرفته میشود، نه اینکه روی کاغذ ثابت شود.
پرسشی که پاسخ میدهد: زمان اجرای این الگوریتم در عمل، روی ورودیهایی که واقعاً میبیند، چگونه رشد میکند؟
کنار میگذارد: بدترین حالتی که در ورودیهای آزمون نیست تا وقتی رخ ندهد ناشناخته میماند.
اجرا میشود روی: حدود 109 FLOPS تقریبی روی یک ایستگاه کاری در میان ورودیهای آزمون تولیدشدهٔ بسیار اجرا میشوداز: 1970 تا 1970، آزمون تجربی نظاممند زمان اجرای الگوریتمها
اجرای برنامه با مدل زبانی
مدل زبانی هنگام دنبال کردن آنچه یک برنامه محاسبه میکند، حالتهای میانی را گامبهگام مینویسد.
پرسشی که پاسخ میدهد: آیا مدل زبانی میتواند اجرای کد را شبیهسازی کند؟
کنار میگذارد: درستی خروجی تضمین نمیشود و برنامههای بلند شکست میخورند.
اجرا میشود روی: حدود 1014 FLOPS تقریبی استنتاج برای هر پرسشاز: 2021 Show your work: scratchpads for intermediate computation with language models (2021) منبع
شبیهسازی اجماع بلاکچین
شبکهای از گرهها که با وجود تأخیرها بلوک میسازند و به اشتراک میگذارند، تا آزموده شود اندازهٔ بلوک، زمانبندی و مهاجمان چه اثری بر امنیت و توان عملیاتی دارند.
پرسشی که پاسخ میدهد: یک بلاکچین تحت تأخیر شبکه و حمله چقدر امن و سریع است؟
کنار میگذارد: رفتار گره و توپولوژی شبکهٔ واقعی فقط تا حدی اندازهگیری شده است.
اجرا میشود روی: حدود 108 FLOPS تقریبی اجراهای رویدادمحور هزاران گره.از: 2016 تحلیل امنیت و عملکرد بلاکچینهای اثبات کار با شبیهساز از ژروه و همکارانش. منبع
شبیهسازی رویدادگسستهٔ موازی
شبیهسازی رویدادها در زمان میان پردازندههای بسیار تقسیم میشود که هر کدام ساعت خود را جلو میبرند و اگر چیزی دیر برسد به عقب برمیگردند.
پرسشی که پاسخ میدهد: یک شبیهسازی عظیم رویدادمحور، مثل یک شبکه یا میدان نبرد، چگونه میتواند روی ماشینهای بسیار زیاد بهسرعت اجرا شود؟
کنار میگذارد: بازگشتها میتوانند آبشاری شوند و افزایش سرعت به شدت به میزان پیوستگی رویدادها بستگی دارد.
اجرا میشود روی: حدود 1014 FLOPS تقریبی ساعت روی یک ابررایانه برای میلیاردها رویداد.از: 1985 زمان مجازی جفرسون، سازوکار Time Warp برای همگامسازی خوشبینانه. منبع
شبیهسازی معماری پردازندهٔ گرافیکی
هستهها، وارپها و حافظهٔ یک پردازندهٔ گرافیکی چرخهبهچرخه مدل میشوند و برنامههای واقعی را اجرا میکنند تا طرح پیش از ساخت ارزیابی شود.
پرسشی که پاسخ میدهد: یک تغییر طراحی چگونه بر سرعت برنامههای موازی روی یک تراشهٔ گرافیکی اثر میگذارد؟
کنار میگذارد: جزئیات تراشههای واقعی محرمانه یا ناشناخته است، پس مدل فقط تقریباً با عددهای طرحهای موجود میخواند.
اجرا میشود روی: حدود 1012 FLOPS تقریبی ساعت تا روز زمان میزبان برای هر ثانیه اجرای شبیهسازیشده.از: 2009 تحلیل بخودا و همکارانش از بارهای کاری CUDA با شبیهساز دقیق GPU. منبع
شبیهسازی سامانهٔ شتابیافته با FPGA
طرح یک تراشه روی مدارهای پیکربندیپذیر بسیاری بارگذاری میشود که آن را دقیقاً چرخهبهچرخه و با سرعت مگاهرتز اجرا میکنند و کل سرورها و شبکههایشان را شبیهسازی میکنند.
پرسشی که پاسخ میدهد: این پردازنده و خوشهاش هنگام اجرای نرمافزار واقعی، پیش از ساختهشدن، چگونه رفتار میکنند؟
کنار میگذارد: بسیار کندتر از تراشهٔ واقعی است و طرحی که روی مدارها جا نشود قابل اجرا نیست.
اجرا میشود روی: حدود 1015 FLOPS تقریبی چند روز روی ابری از صدها مدار پیکربندیپذیر.از: 2018 FireSim از کارندیکر و همکارانش، شبیهسازی سامانهٔ گسترشپذیر با دقت چرخه روی FPGA در ابر عمومی. منبع
شبیهسازی تمامسامانه
یک رایانهٔ کامل، با پردازنده، حافظه، دیسک و کارت شبکه، آنقدر خوب شبیهسازی میشود که سیستمعاملی دستنخورده را بالا بیاورد و برنامههایش را اجرا کند.
پرسشی که پاسخ میدهد: نرمافزار واقعی روی ماشینی که هنوز وجود ندارد، یا میتوان آن را به دلخواه متوقف و بازپخش کرد، چگونه رفتار میکند؟
کنار میگذارد: زمانبندی برای سرعت تقریب زده میشود، پس نمیتواند کارایی دقیق را بدهد، فقط رفتار کارکردی را.
اجرا میشود روی: حدود 1011 FLOPS تقریبی تقریباً بیدرنگ روی یک سرور برای هر ماشین شبیهسازیشده.از: 2002 Simics از ماگنوسون و همکارانش، یک بستر شبیهسازی کل سامانه. منبع
شبیهسازی سبک شبکه
دهها یا صدها میزبان و سوئیچ مجازی نرمافزار شبکهٔ واقعی را روی یک لپتاپ اجرا میکنند، با کابلهای تقلیدشده که سرعت و تأخیر معین دارند.
پرسشی که پاسخ میدهد: آیا این برنامهٔ کنترل شبکه پیش از استقرار روی یک توپولوژی کامل کار میکند؟
کنار میگذارد: پردازندهٔ خود میزبان میان همهٔ گرههای مجازی تقسیم میشود، پس پیوندهای سریع کند میشوند.
اجرا میشود روی: حدود 1010 FLOPS تقریبی بیدرنگ روی یک ایستگاه کاری.از: 2010 «A network in a laptop» از لانتز، هلر و مککاون، نمونهسازی سریع برای شبکههای نرمافزارمحور. منبع
بازپخت شبیهسازیشده
رایانه مدلی از اتمها یا یک طرح را آهسته سرد میکند و گاهی چیدمانهای بدتر را میپذیرد تا برای یک مسئلهٔ بهینهسازی دشوار راهحلی خوب بیابد.
پرسشی که پاسخ میدهد: در میان شمار نجومی احتمالها، چیدمان یا زمانبندی تقریباً بهینه کدام است؟
کنار میگذارد: بهترین پاسخ را تضمین نمیکند و نتایج به برنامهٔ سردشدن بستگی دارند.
اجرا میشود روی: حدود 1012 FLOPS تقریبی ساعت روی یک ایستگاه کاری برای جانمایی یک تراشه.از: 1983 بهینهسازی با بازپخت شبیهسازیشده، از کرکپاتریک، گلات و وکی. منبع
محاسبات بیزی تقریبی
شبیهسازی با مقدارهای پارامتر آزمایشی بسیار اجرا میشود و آنهایی که دادهای نزدیک به دادههای مشاهدهشده میدهند نگه داشته میشوند، و تصویری از مقدارهای محتمل پدید میآید.
پرسشی که پاسخ میدهد: کدام تنظیمهای یک مدل پیچیده میتوانست دادهٔ مشاهدهشدهٔ ما را تولید کند؟
کنار میگذارد: نتیجه به این بستگی دارد که از کدام خلاصههای داده استفاده شود و تطبیق تا چه حد نزدیک باید باشد تا به حساب آید.
اجرا میشود روی: حدود 1013 FLOPS تقریبی میلیونها اجرای شبیهساز روی یک خوشه.از: 1997 استنباط زمانهای همآیی از دادهٔ توالی DNA با شبیهسازی از Tavaré و همکاران. منبع