Matematik ve hesaplama

Rastgele matris deneyleri

Rastgele sayılarla dolu büyük matrisler; özdeğerlerinin istatistiğini incelemek için tekrar tekrar köşegenleştirilir.

Yanıtladığı soru: Rastgele bir matrisin özdeğerleri hangi örüntüye yerleşir ve bu, matematiğin ve fiziğin başka alanlarıyla örtüşür mü?

Dışarıda bıraktığı: Olası matrislerin sonsuz uzayının yalnızca küçücük bir köşesini örnekler.

Çalıştığı yer: yaklaşık 10¹² FLOPS yaklaşık çok sayıda büyük matris üretip köşegenleştiren bir üniversite kümesiŞu tarihten beri: 1955 Wigner'in rastgele matris özdeğer istatistikleri üzerine ilk çalışması

Rastgele graf deneyleri

Bir rastgele kuralla düğüm düğüm ya da kenar kenar üretilen graflar; bağlantılılık ya da kümelenme gibi hangi özelliklerin tipik olarak ortaya çıktığını görmek için.

Yanıtladığı soru: Düğüm ve kenar ekleme kuralına göre "tipik" bir ağ nasıl görünür?

Dışarıda bıraktığı: Gerçek dünya ağları, modeli üreten kural kadar nadiren temizdir.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık milyonlarca düğüme kadar graflar için bir masaüstünde çalışırŞu tarihten beri: 1959 Erdős ve Rényi'nin rastgele çizge modeli

Sızma simülasyonu

Düğüm noktalarının ya da bağlarının rastgele açıldığı bir örgü ya da ağ; bağlantılı bir yolun bütün sistemi birdenbire kat ettiği nokta izlenir.

Yanıtladığı soru: Rastgele bir ağ hangi yoğunlukta birdenbire uçtan uca bağlantılı hale gelir?

Dışarıda bıraktığı: İdealleştirilmiş kafesler, herhangi bir gerçek gözenekli malzemeden ya da ağdan daha temiz davranır.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık büyük örgü taramaları için bir masaüstü makineŞu tarihten beri: 1957 Broadbent ve Hammersley'in sızma kuramını tanıtması

Deneysel matematik aramaları

Örüntüleri, karşı örnekleri ya da sayılar arasındaki kesin ilişkileri bulmak için elle denetlenebilecek olanın çok ötesine taşan kaba kuvvetli sayısal arama.

Yanıtladığı soru: Bu sanı, kontrol etmeye gücü yeten her durum için doğru mu ve bir örüntü ortaya çıkıyor mu?

Dışarıda bıraktığı: Doğru çıkan vaka sayısı ne kadar çok olursa olsun, kontrol edilen vakalar bir kanıt oluşturmaz.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık tek bir arama için günlerce çalışan bir üniversite kümesiŞu tarihten beri: 1963 1963'e gelindiğinde, tamsayı ilişkileri ve asal örüntüleri için bilgisayar aramaları

Sabitlerin Monte Carlo tahmini

Bir matematiksel sabiti ya da integrali tahmin etmek için kullanılan rastgele örnekleme, örneğin bir alanı tahmin etmek için noktalar saçmak; fiziksel bir model için değil, bir alıştırma olarak.

Yanıtladığı soru: Yalnızca kör rastgele örnekleme, kesin bir matematiksel niceliği ne kadar doğru saptayabilir?

Dışarıda bıraktığı: Neredeyse her daha gelişmiş sayısal yöntemden çok daha yavaş yakınsar.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık bir dizüstü bilgisayarda saniyelerden dakikalara çalışırŞu tarihten beri: 1946 Ulam'ın 1946 tarihli fikri; von Neumann Mart 1947'de elektronik bilgisayar sürümünü önerdi ve yöntem ilk kez 1949'da yayımlandı kaynakSimülasyonlar ağacında: Monte Carlo yöntemi

Etkileşimli modeli çalıştır

Hesaplamalı sayılar kuramı aramaları

Büyük sayılar, el yerine ölçekli çalıştırılan algoritmalarla asallık için sınanır, çarpanlarına ayrılır ya da mükemmel sayılar gibi özel özellikler için aranır.

Yanıtladığı soru: Bu devasa sayı aradığımız özelliğe sahip mi ve arama rekoru ne kadar ileri taşıyabilir?

Dışarıda bıraktığı: Rekor kıran aramalar, kimsenin henüz bakmayı düşünmediği sayılar hakkında çok az şey söyler.

Çalıştığı yer: yaklaşık 10¹³ FLOPS yaklaşık bağışlanmış çok sayıda makineye yayılmış dağıtık bir gönüllü hesaplama projesiŞu tarihten beri: 1951 Lucas'ın Mersenne asalları için elle yaptığı sınama, ilk kez 1951'de bilgisayarla çalıştırıldı

Kaotik çekicilerin sayısal çözümlemesi

Başlangıç koşullarına duyarlı bağımlılığı ve fraktal bir çekiciyi göstermek için adım adım integre edilen küçük bir doğrusal olmayan denklem kümesi.

Yanıtladığı soru: Basit bir belirlenimci sistem neden öngörülemez hâle gelir?

Dışarıda bıraktığı: Sayısal yuvarlama, uzun bir yörüngenin gerçek bir yörünge olmadığı, yalnızca ona yakın kalan bir yol olduğu anlamına gelir.

Çalıştığı yer: yaklaşık 10³ FLOPS yaklaşık birkaç denklem, bir dizüstü bilgisayarda saniyeler.Şu tarihten beri: 1963 Lorenz'in belirlenimci dönemsiz akışı, bir bilgisayarda çalıştırılan bir konveksiyon modeli. kaynakSimülasyonlar ağacında: Lorenz’in kaotik konveksiyonu

Doğrusal olmayan kafes deneyleri

Doğrusal olmayan yaylarla bağlı bir kütle zinciri tek bir modda başlatılır ve enerjinin termodinamiğin öngördüğü gibi eşit yayılıp yayılmadığı izlenir.

Yanıtladığı soru: Doğrusal olmayan bir zincir enerjisini tüm hareketleri arasında eşit paylaşır mı?

Dışarıda bıraktığı: Sonuçlar seçilen zincire ve başlangıç durumuna bağlıdır.

Çalıştığı yer: yaklaşık 10³ FLOPS yaklaşık modern ölçütlere göre küçük; özgün çalışma birkaç düzine kütle kullandı.Şu tarihten beri: 1955 Fermi, Pasta ve Ulam'ın erken bir dijital bilgisayarda doğrusal olmayan problemler üzerine çalışmaları. kaynak

Soliton sayısal deneyleri

Darbelerin birbirinin içinden geçip biçimini koruduğunu, doğrusal dalgaların yapamadığı şeyi görmek için bir ızgarada çözülen doğrusal olmayan bir dalga denklemi.

Yanıtladığı soru: Bazı doğrusal olmayan dalgalar birbirinin içinden neden değişmeden geçer?

Dışarıda bıraktığı: Doğrusal olmayan dalgaların genel davranışını değil, tek bir denklem ailesini gösterir.

Çalıştığı yer: yaklaşık 10⁴ FLOPS yaklaşık tek boyutlu bir ızgara, bugün için sıradan.Şu tarihten beri: 1965 Zabusky ve Kruskal'ın çarpışmasız bir plazmada solitonların etkileşimi ve ilk durumların yinelenmesi çalışması. kaynak

Fraktal küme render etme

Kararlı noktalar kümesinin sınırını çizmek için, karmaşık düzlemin her noktasında kaçıp kaçmadığına bakılan basit bir yinelemeli formül.

Yanıtladığı soru: Basit bir yinelemenin sınırlı kaldığı kümenin şekli nedir?

Dışarıda bıraktığı: Kaçış testleri yalnızca üyeliğe işaret eder ve görüntü, sonsuz ayrıntılı bir kümenin sonlu çözünürlüklü örneklemesidir.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık derin yakınlaştırmalar, milyonlarca noktada genişletilmiş duyarlılıklı yineleme gerektirir.Şu tarihten beri: 1980 Mandelbrot'un z'den lambda z(1-z)'nin yinelemesinin fraktal yönleri, Mandelbrot kümesinin ilk bilgisayar görüntüleri. kaynak

Kum yığını kendiliğinden örgütlenen kritiklik

Bir ızgaraya bırakılan ve fazla dik olunca devrilen taneler; ayar yapmadan her büyüklükte çığ verir ve sistemlerin kritik duruma nasıl ulaştığının bir modelidir.

Yanıtladığı soru: Her boyuttaki çığlar hiçbir ayar yapılmadan neden ortaya çıkar?

Dışarıda bıraktığı: Gerçek sistemlerin aynı ölçeklenmeyi paylaşıp paylaşmadığı tartışmalıdır.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık ölçeklenmeyi görmek için büyük ızgaralarda uzun çalışmalar.Şu tarihten beri: 1987 Bak, Tang ve Wiesenfeld'in kendiliğinden örgütlenen kritikliği: 1/f gürültüsünün bir açıklaması. kaynak

Riemann zeta sıfırı hesabı

Zeta fonksiyonunun kritik doğrusu boyunca aldığı değerler, sıfırlarını bulmak ve saymak, bunların hipotezin söylediği yerde olup olmadığını denetlemek için hesaplanır.

Yanıtladığı soru: Zeta fonksiyonunun bütün aşikâr olmayan sıfırları tek bir doğru üzerinde mi yer alır?

Dışarıda bıraktığı: Ne kadar uzun olursa olsun sonlu bir denetim, onun ötesinde çizgi dışında bir sıfırın bulunmadığını kanıtlayamaz.

Çalıştığı yer: yaklaşık 10¹⁸ FLOPS yaklaşık en büyük aramalarda onlarca yıllık işlemci süresi.Şu tarihten beri: 1953 Turing'in Riemann zeta fonksiyonu hesaplamaları. kaynak

Bilgisayarla pi'nin basamakları

Pi için seriler, hem sayıyı hem makineyi sınayarak, kesin aritmetikle muazzam basamak sayılarına kadar toplanır.

Yanıtladığı soru: Pi'nin basamakları rastgele görünüyor mu ve makineye bu ölçekte güvenilebilir mi?

Dışarıda bıraktığı: Basamaklar hiçbir açık soruyu yanıtlamaz ve denetimler, yöntem bağımsızsa ancak donanım hatalarını yakalar.

Çalıştığı yer: yaklaşık 10¹⁷ FLOPS yaklaşık yüz trilyonlarca basamak için bir sunucuda aylar.Şu tarihten beri: 1950 Reitwiesner'in ENIAC ile pi ve e'yi 2000'den fazla ondalık basamağa kadar belirlemesi (1950'de yayımlandı, Pi: A Source Book'ta yeniden basıldı). kaynak

Yapay zekâ güdümlü sanı keşfi

Matematiksel nesnelerin büyük tablolarında makine öğrenmesi hangi özelliklerin bağlantılı olduğunu bulur ve matematikçilerin ardından kanıtlamaya çalıştığı bir sanı önerir.

Yanıtladığı soru: Bu matematiksel nicelikler arasındaki hangi görünmeyen ilişkiyi kanıtlamaya değer?

Dışarıda bıraktığı: Yalnızca örüntüler önerir ve kendisi hiçbir şeyi kanıtlamaz; verideki bazı düzenlilikler verinin nasıl üretildiğinin yapay sonuçları olabilir.

Çalıştığı yer: yaklaşık 10¹⁵ FLOPS yaklaşık veri kümesi başına birkaç GPU'da günler.Şu tarihten beri: 2021 Davies ve çalışma arkadaşlarının insan sezgisini yapay zekâyla yönlendirerek matematiği ilerletmesi. kaynak

Öğrenilmiş algoritma ve inşa araması

Oyun oynayan ya da dil modeli tabanlı bir sistem yeni yöntemler ya da matematiksel nesneler arar; her adayın doğruluğunu bir bilgisayar denetler.

Yanıtladığı soru: Bir program, insanların bulduğundan daha hızlı bir algoritma ya da daha büyük bir örnek keşfedebilir mi?

Dışarıda bıraktığı: Her sonuç tek bir yeni örnektir ve arama yalnızca tasarımcılarının bir oyun olarak çerçevelediği nesne türlerini kapsar.

Çalıştığı yer: yaklaşık 10¹⁷ FLOPS yaklaşık hızlandırıcı kümelerinde günlerden haftalara.Şu tarihten beri: 2022 Fawzi ve çalışma arkadaşlarının pekiştirmeli öğrenmeyle daha hızlı matris çarpım algoritmaları keşfeden AlphaTensor'u. kaynak

Model denetimi

Bir protokol ya da devre tasarımı gibi sonlu bir sistemin ulaşılabilir her durumu, bir özelliğin hepsinde geçerli olduğunu denetlemek için bilgisayarla sıralanır.

Yanıtladığı soru: Bu tasarımın kendi kurallarını çiğnediği ulaşılabilir herhangi bir durum var mı?

Dışarıda bıraktığı: Durum uzayları denetlenebilecek olanın ötesinde patlar; bu yüzden gerçek tasarımlar önce basitleştirilir.

Çalıştığı yer: yaklaşık 10¹² FLOPS yaklaşık büyük ama sınırlı bir durum uzayını tüketen bir üniversite kümesiŞu tarihten beri: 1981 Clarke ve Emerson'ın model denetimini tanıtması

Otomatik teorem kanıtlama araması

Bir matematiksel önermenin kanıtını ya da çürütmesini arayan, bilgisayarın adım adım ürettiği mantıksal çıkarım zincirleri üzerinde bir arama.

Yanıtladığı soru: Aksiyomlardan bu önermeye giden geçerli bir mantıksal adımlar zinciri var mı?

Dışarıda bıraktığı: Hiçbir insanın seçmeyeceği, bazen de erişilebilir mesafede hiç olmayan kanıtlar bulur.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık saatlerden günlere arama yapan bir üniversite kümesiŞu tarihten beri: 1956 Logic Theorist, ilk otomatik ispat arama programlarından biri

SAT ve kısıt çözme

Büyük bir mantıksal kısıtlar kümesini sağlamak için sistematik olarak aranan milyonlarca doğru ya da yanlış değer birleşimi; çizelgeleme, yönlendirme ya da tasarım doğrulama için kullanılır.

Yanıtladığı soru: Bu kısıtların hepsini aynı anda sağlayan herhangi bir değer ataması var mı?

Dışarıda bıraktığı: Bazı örnekler o kadar zordur ki hiçbir çözücü, ne kadar iyi olursa olsun, zamanında bitiremez.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık problemin boyutuna göre bir iş istasyonundan bir kümeye kadarŞu tarihten beri: 1962 Sağlanabilirlik araması için Davis-Putnam yöntemi

Kriptografik saldırı modelleme

Bir kod ya da anahtar değişim şeması, onu kırmanın gerçekte ne kadar çaba gerektirdiğini ölçmek için simülasyonda kaba kuvvetle, istatistiksel yanlılıkla ya da modellenmiş bir zayıflıkla milyonlarca kez saldırıya uğratılır.

Yanıtladığı soru: Bunu kırmak için gerçekte kaç işlem gerekir ve bu sayı hâlâ güvenle büyük mü?

Dışarıda bıraktığı: Yalnızca analistin modellemeyi düşündüğü saldırıları sınar, henüz kimsenin bulmadığını değil.

Çalıştığı yer: yaklaşık 10¹⁴ FLOPS yaklaşık saldırı denemelerini çalıştıran, çok sayıda makineden oluşan dağıtık bir kümeŞu tarihten beri: 1976 1976'ya gelindiğinde, şifre ve anahtar değişimi gücünün hesaplamalı çözümlemesi

Yan kanal sızıntısı simülasyonu

Bir cihazın şifreleme işlemi yaparken güç tüketimi, zamanlaması ya da elektromanyetik yayını modellenir; dışarıdan dinleyen birinin bundan ne öğrenebileceğini görmek için.

Yanıtladığı soru: Gizli anahtarın ne kadarı, matematik yoluyla değil, aygıtın fiziksel davranışı yoluyla sızar?

Dışarıda bıraktığı: Laboratuvar koşulları, gürültülü gerçek bir aygıtın genellikle ele vereceğinden daha temiz sinyaller yakalar.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık tek bir aygıtın güç ya da zamanlama izini modelleyen bir iş istasyonuŞu tarihten beri: 1996 Kocher'in kriptografik uygulamalara yönelik zamanlama saldırılarını göstermesi

Güvenlik protokolü doğrulaması

Bir saldırganın bir iletişim protokolünde gönderebileceği, yeniden oynatabileceği ya da taklit edebileceği her mesaj, bilgisayarla sıralanır; bir sırrın ya da kimliğin ondan zorla çıkarılıp çıkarılamayacağını denetlemek için.

Yanıtladığı soru: Herhangi bir mesaj dizisi bu protokolü bir sırrı sızdırmaya ya da sahte bir kimliği kabul etmeye kandırabilir mi?

Dışarıda bıraktığı: Protokolü belirtildiği gibi doğrular; gerçek bir uygulamanın aldığı kısayolları değil.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık bir protokolün mesaj uzayını denetleyen bir iş istasyonundan bir kümeye kadarŞu tarihten beri: 1989 Dolev-Yao modeli, protokol doğrulamasının temel dayanağı

Her durumu denetleyerek bilgisayar destekli kanıt

Sonlu bir durum listesine indirgenmiş bir teorem; hiçbir insan hepsini denetleyemeyeceği için her biri programla doğrulanır.

Yanıtladığı soru: Bir kanıt, bir makinenin her durumu denetlemesiyle tamamlanabilir mi?

Dışarıda bıraktığı: Güven programa, donanıma ve durumlara indirgeme argümanına kayar.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık orijinali için bir ana bilgisayarda yaklaşık bin saat; şimdi çok daha az.Şu tarihten beri: 1977 Appel ve Haken'in, bilgisayarla denetlenen indirgenebilirlik yoluyla her düzlemsel haritanın dört renkle boyanabileceğine dair kanıtı. kaynak

Doğrulanmış sayısal yöntemler

Garantili sınırlarla yürütülen hesaplar; böylece sayısal bir sonuç, kaotik bir çekicinin varlığı gibi matematiksel bir önermeyi kanıtlar.

Yanıtladığı soru: Hesaplanmış bir yanıt yalnızca büyük olasılıkla doğru değil, kanıtlanmış biçimde doğru olabilir mi?

Dışarıda bıraktığı: Sınırlar uzun sürelerde patlayabilir; bu da kanıtları kısa ya da uslu problemlerle sınırlar.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık aralık aritmetiği maliyeti mütevazı bir katsayıyla çarpar.Şu tarihten beri: 2002 Tucker'ın titiz ODE çözücüsü ve Smale'in 14. problemi: Lorenz çekicisinin var olduğunun kanıtı. kaynak

Turing makinesi numaralandırması

Asgari bir makinenin her küçük programı, hangilerinin durduğunu ve hangilerinin sonsuza dek çalıştığını görmek için çalıştırılır; her boyutta, durmakla birlikte en uzun süre çalışan program aranır.

Yanıtladığı soru: Küçük bir program durmadan önce ne kadar çalışabilir?

Dışarıda bıraktığı: Karar verilemezlik, bazı makinelerin ne kadar uzun çalışırsa çalışsın hiçbir zaman sınıflandırılamayacağı anlamına gelir.

Çalıştığı yer: yaklaşık 10¹⁵ FLOPS yaklaşık milyarlarca makine, durmayanlar için kanıtlarla.Şu tarihten beri: 1965 Lin ve Rado'nun Turing makinesi problemleri üzerine bilgisayar çalışmaları. kaynak

İstatistiksel model denetimi

Rastgele davranan bir sistem, bir özelliği ihlal etme olasılığını güvenle kestirmek için birçok kez simüle edilir.

Yanıtladığı soru: Rastgele bir sistemin bir güvenlik kuralını çiğneme olasılığı nedir?

Dışarıda bıraktığı: İstatistiksel çalıştırmalar kanıt değil, güven düzeyiyle birlikte bir olasılık verir; nadir arızalar ise önem örneklemesi gerektirir.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık binlerce ila milyonlarca örneklenmiş yürütme.Şu tarihten beri: 2002 Younes ve Simmons'ın kabul örneklemesiyle kesikli olay sistemlerinin olasılıksal doğrulaması. kaynak

Fuzz testi

Bir programa, çökmesine yol açanları bulmak için çok sayıda rastgele ya da bozulmuş girdi verilir; bir bakıma düşmanca ya da özensiz bir dünya simüle edilir.

Yanıtladığı soru: Hangi girdi bu yazılımı çökertir?

Dışarıda bıraktığı: Yalnızca rastgele girdilerin ulaştığı arızaları bulur ve bir program, nadir bir durumun ardına bir hata saklayarak yıllarca geçer not alabilir.

Çalıştığı yer: yaklaşık 10¹⁴ FLOPS yaklaşık büyük bir kod tabanı için makine-yıllarca CPU zamanı.Şu tarihten beri: 1990 Miller, Fredriksen ve So'nun UNIX araçlarının güvenilirliği üzerine deneysel çalışması. kaynak

Sembolik yürütme

Bir program, bilinmeyen girdiler simge olarak yazılarak çalıştırılır, her yoldaki koşullar toplanır, sonra bir çözücü her dalı izleyen değerleri bulur.

Yanıtladığı soru: Hangi girdiler bu programın her yolunu çalıştırır ve herhangi biri bir hataya ulaşır mı?

Dışarıda bıraktığı: Yolların sayısı program boyutuyla üstel olarak artar; bu yüzden büyük programlar yalnızca kısmen kapsanır.

Çalıştığı yer: yaklaşık 10¹² FLOPS yaklaşık program başına saatlerce çözücü süresi, yol sayısıyla dik biçimde artar.Şu tarihten beri: 1976 King'in sembolik yürütmesi ve program testi. kaynak

Soyut yorumlama

Bir program, tek tek değerler yerine aralıklar gibi olası değer kümeleri üzerinde çalıştırılır; her girdi için geçerli özellikleri kanıtlamak için.

Yanıtladığı soru: Bu program, herhangi bir girdi için hiç sıfıra bölebilir ya da taşabilir mi?

Dışarıda bıraktığı: Güvenli yaklaşım yanlış alarmları artırır, bu yüzden insanlar yine de her uyarıyı denetlemek zorundadır.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık büyük bir aviyonik kod tabanı için bir iş istasyonunda saatler.Şu tarihten beri: 1977 Cousot ve Cousot'un soyut yorumlaması; programların statik çözümlemesi için birleşik bir örgü modeli. kaynak

Sınırlı model denetimi

Bir tasarımın belirli sayıda adıma kadarki davranışı bir mantık formülü olarak yazılır ve bir hataya giden herhangi bir kısa yolu bulmak için bir sağlanabilirlik çözücüsüne verilir.

Yanıtladığı soru: Bu devre ya da program, belirli sayıda adım içinde bir hata durumuna ulaşabilir mi?

Dışarıda bıraktığı: Ayrı bir argüman yeterli olduğunu göstermedikçe, adım sınırının ötesinde hiçbir şeyi kanıtlamaz.

Çalıştığı yer: yaklaşık 10¹³ FLOPS yaklaşık mülk başına bir sunucuda saatler.Şu tarihten beri: 1999 Biere, Cimatti, Clarke ve Zhu'nun BDD kullanmayan simgesel model denetimi. kaynak

Özellik tabanlı rastgele test

Her zaman geçerli olması gereken bir kural ifade edilir; bilgisayar birçok rastgele durum üretir ve her başarısızlığı küçük bir karşı örneğe indirger.

Yanıtladığı soru: Bu kod, geniş bir girdi aralığında kendi belirtimine uyuyor mu?

Dışarıda bıraktığı: Rastgele vakalar nadir bir duruma hiç ulaşmayabilir ve yazılan özellik önemli olan özellik olmayabilir.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık bir dizüstü bilgisayarda binlerce vaka için dakikalar.Şu tarihten beri: 2000 Claessen ve Hughes'un Haskell programlarının rastgele testi için hafif bir araç olan QuickCheck'i. kaynak

Sinir ağı doğrulaması

Kısıt çözücüler, örnekleri sınamak yerine, bir bölgedeki her girdi için bir sinir ağının çıktısının sınırlar içinde kaldığını kanıtlar.

Yanıtladığı soru: Bir girdideki küçük bir değişiklik, ağın yanlış yanıt vermesine yol açabilir mi?

Dışarıda bıraktığı: Kanıtlar yalnızca küçük ağlara ölçeklenir ve denetlenebilen tedirginlikler kümesi dardır.

Çalıştığı yer: yaklaşık 10¹³ FLOPS yaklaşık küçük bir ağ için bir sunucuda saatlerden günlere.Şu tarihten beri: 2017 Katz ve çalışma arkadaşlarının Reluplex'i, derin sinir ağlarını doğrulamak için bir SMT çözücüsü. kaynak

Bilgisayar mimarisi simülasyonu

Önerilen bir işlemcinin ardışık düzeni, önbellekleri ve dal öngörücüsü, yapılmadan önce çipin hızını kestirmek için komut komut modellenir.

Yanıtladığı soru: Bu işlemci tasarımı, daha silikon kesilmeden gerçek programları ne kadar hızlı çalıştırır?

Dışarıda bıraktığı: Gerçek çipin yeterince çoğunu basitleştirir; bu yüzden son silikon her zaman modelden biraz farklıdır.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık model üzerinden kıyaslama programları çalıştıran bir üniversite kümesiŞu tarihten beri: 1990 1990'a gelindiğinde, mimari araştırması için çevrim doğruluklu işlemci simülatörleri

Dağıtık sistemler ve uzlaşma simülasyonu

Birbirine gecikmeler, kayıplar ve arızalarla mesaj gönderen birçok bilgisayar modellenir; dağıtık bir algoritmanın hâlâ doğru yanıt üzerinde uzlaşıp uzlaşmadığını sınamak için.

Yanıtladığı soru: Bu algoritma, mesajlar kaybolduğunda, geciktiğinde ya da düğümler çöktüğünde yine doğru uzlaşmaya ulaşır mı?

Dışarıda bıraktığı: Enjekte edilen arızalar tasarımcının önceden beklediği arızalardır; üretimde beklenmedik biçimde ortaya çıkanlar değil.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık yüzlerce sanal düğümü simüle eden bir kümeŞu tarihten beri: 1978 Lamport'un dağıtık sistemlerde sıralama ve arıza üzerine erken çalışması

Depolama sistemleri simülasyonu

Veriyi nasıl düzenlediklerine, nasıl bozulup toparlandıklarına göre modellenen diskler, sürücüler ve dosya sistemleri; gerçek sürücüler alınıp doldurulmadan önce bir depolama tasarımını sınamak için.

Yanıtladığı soru: Bu depolama tasarımı, önce gerçekten denemek için fazla pahalı bir ölçekte nasıl performans gösterir ve arızadan nasıl sağ çıkar?

Dışarıda bıraktığı: Gerçek sürücüler, modelin rastgele arıza oranından daha dağınık, daha ilişkili biçimlerde bozulur.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık bir depolama dizisini modelleyen bir iş istasyonundan küçük bir kümeye kadarŞu tarihten beri: 1988 1988'e gelindiğinde, disk dizisi güvenilirliğinin simülasyon modelleri

İşletim sistemi zamanlayıcı simülasyonu

Gelip bir işlemci için yarışan bir hesaplama görevleri akışı modellenir; hangisinin en adil ya da en hızlı olduğunu görmek için farklı çizelgeleme kurallarıyla çalıştırılır.

Yanıtladığı soru: Görev kuyruğunu sıralamanın hangi yolu en çok işi bitirir ya da her göreve en adildir?

Dışarıda bıraktığı: Yapay iş yükleri, gerçek bir makinenin karşılaştığı düzensiz görev karışımıyla nadiren örtüşür.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık bir dizüstü bilgisayarda ya da iş istasyonunda saniyelerden dakikalara çalışırŞu tarihten beri: 1968 1968'e gelindiğinde, işlemci çizelgeleme politikalarının simülasyon çalışmaları

Derleyici ve program eniyileme araması

Bir kod parçasının çok sayıda küçük varyasyonu denenir ve ölçülür; aynı işi yapan en hızlı ya da en kısa sürümü aramak için.

Yanıtladığı soru: Bu küçük kod parçasını yazmanın eşdeğer yollarından hangisi gerçekte en hızlıdır?

Dışarıda bıraktığı: Bulunan programlar bazen o kadar olağandışıdır ki neden çalıştıklarına dair hiçbir açıklama yoktur.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık geniş bir kod varyantı uzayını tarayan bir kümeŞu tarihten beri: 2006 2006'ya gelindiğinde, kısa komut dizileri üzerinde süper eniyileme araması

Deneysel algoritma başarım testi

Rastgele üretilmiş ya da gerçek dünya girdileri üzerinde, giderek büyüyen boyutlarda binlerce kez çalıştırılan bir algoritma; kâğıt üzerinde kanıtlamak yerine çalışma süresinin gerçekte nasıl büyüdüğünü ölçer.

Yanıtladığı soru: Bu algoritmanın çalışma süresi, gerçekte göreceği girdilerde pratikte nasıl büyür?

Dışarıda bıraktığı: Test girdilerinde bulunmayan en kötü durum, ortaya çıkana dek fark edilmez.

Çalıştığı yer: yaklaşık 10⁹ FLOPS yaklaşık çok sayıda üretilmiş test girdisi boyunca bir iş istasyonunda çalışırŞu tarihten beri: 1970 1970'e gelindiğinde, algoritma çalışma sürelerinin sistematik deneysel sınanması

Dil modeli ile program yürütme

Bir dil modeli, bir programın ne hesaplayacağını izlerken adım adım ara durumları yazar.

Yanıtladığı soru: Bir dil modeli kod çalıştırmayı taklit edebilir mi?

Dışarıda bıraktığı: Çıktının doğruluğu garanti değildir ve uzun programlar başarısız olur.

Çalıştığı yer: yaklaşık 10¹⁴ FLOPS yaklaşık Sorgu başına çıkarımŞu tarihten beri: 2021 Show your work: scratchpads for intermediate computation with language models (2021) kaynak

Blokzincir uzlaşma simülasyonu

Gecikmeler altında blok üretip paylaşan bir düğüm ağı; blok boyutunun, zamanlamanın ve saldırganların güvenliği ve verimi nasıl etkilediğini sınamak için.

Yanıtladığı soru: Bir blokzincir, ağ gecikmesi ve saldırı altında ne kadar güvenli ve hızlıdır?

Dışarıda bıraktığı: Gerçek düğüm davranışı ve ağ topolojileri yalnızca kısmen ölçülmüştür.

Çalıştığı yer: yaklaşık 10⁸ FLOPS yaklaşık binlerce düğümün olay güdümlü çalıştırmaları.Şu tarihten beri: 2016 Gervais ve çalışma arkadaşlarının iş kanıtlı blokzincirlerin bir simülatörle güvenlik ve başarım çözümlemesi. kaynak

Paralel ayrık olay simülasyonu

Zaman içindeki olayların bir simülasyonu birçok işlemciye bölünür; her biri kendi saatini ilerletir ve biri geç gelirse geri sarılır.

Yanıtladığı soru: Bir ağ ya da savaş alanı gibi devasa olay güdümlü bir simülasyon, birçok makinede nasıl hızlı çalışabilir?

Dışarıda bıraktığı: Geri almalar zincirleme yayılabilir ve hızlanma, olayların ne kadar sıkı bağlı olduğuna büyük ölçüde bağlıdır.

Çalıştığı yer: yaklaşık 10¹⁴ FLOPS yaklaşık milyarlarca olay için bir süper bilgisayarda saatler.Şu tarihten beri: 1985 Jefferson'ın sanal zamanı, iyimser eşzamanlama için Time Warp mekanizması. kaynak

Grafik işlemci mimarisi simülasyonu

Bir grafik işlemcisinin çekirdekleri, warp'ları ve belleği, bir tasarımı üretmeden önce değerlendirmek için gerçek programlar çalıştırılarak çevrim çevrim modellenir.

Yanıtladığı soru: Bir tasarım değişikliği, grafik çipi üzerindeki paralel programların hızını nasıl etkiler?

Dışarıda bıraktığı: Gerçek çiplerin ayrıntıları gizlidir ya da bilinmez, bu yüzden model mevcut tasarımların sayılarına yalnızca kabaca uyar.

Çalıştığı yer: yaklaşık 10¹² FLOPS yaklaşık simüle edilen yürütmenin her saniyesi için saatlerden günlere ana makine zamanı.Şu tarihten beri: 2009 Bakhoda ve çalışma arkadaşlarının ayrıntılı bir GPU simülatörüyle CUDA iş yüklerini çözümlemesi. kaynak

FPGA hızlandırmalı sistem simülasyonu

Bir çip tasarımı, onu megahertz hızlarında çevrim hassasiyetiyle çalıştıran birçok yeniden yapılandırılabilir devreye yüklenir; bütün sunucuları ve bunların ağlarını simüle eder.

Yanıtladığı soru: Bu işlemci ve kümesi, üretilmeden önce gerçek yazılımı çalıştırırken nasıl davranacak?

Dışarıda bıraktığı: Gerçek çipten çok daha yavaştır ve devrelere sığmayan bir tasarım çalıştırılamaz.

Çalıştığı yer: yaklaşık 10¹⁵ FLOPS yaklaşık yüzlerce yeniden yapılandırılabilir devreden oluşan bir bulutta günler.Şu tarihten beri: 2018 Karandikar ve çalışma arkadaşlarının FireSim'i, kamu bulutunda FPGA hızlandırmalı, döngü hassasiyetli, ölçeklenen sistem simülasyonu. kaynak

Tam sistem simülasyonu

İşlemcileri, belleği, diskleri ve ağ kartlarıyla bütün bir bilgisayar, değiştirilmemiş bir işletim sistemini açıp programlarını çalıştıracak kadar iyi simüle edilir.

Yanıtladığı soru: Gerçek yazılım, henüz var olmayan ya da istenildiğinde durdurulup yeniden oynatılabilen bir makinede nasıl davranır?

Dışarıda bıraktığı: Zamanlama hız için yaklaşık ele alınır; bu yüzden kesin performansı değil, yalnızca işlevsel davranışı verir.

Çalıştığı yer: yaklaşık 10¹¹ FLOPS yaklaşık simüle edilen makine başına bir sunucuda neredeyse gerçek zamanlı.Şu tarihten beri: 2002 Magnusson ve çalışma arkadaşlarının Simics'i, tam sistem simülasyon platformu. kaynak

Hafif ağ emülasyonu

Düzinelerce ya da yüzlerce sanal ana bilgisayar ve anahtar, hızı ve gecikmesi belirlenmiş emüle edilmiş kablolarla bağlı olarak tek bir dizüstü bilgisayarda gerçek ağ yazılımı çalıştırır.

Yanıtladığı soru: Bu ağ denetim programı yayımlanmadan önce bütün bir topolojide çalışacak mı?

Dışarıda bıraktığı: Ana makinenin kendi işlemcisi tüm sanal düğümler arasında paylaşılır; bu yüzden hızlı bağlantılar yavaşlar.

Çalıştığı yer: yaklaşık 10¹⁰ FLOPS yaklaşık tek bir iş istasyonunda gerçek zamanlı.Şu tarihten beri: 2010 Lantz, Heller ve McKeown'ın 'A network in a laptop' çalışması, yazılım tanımlı ağlar için hızlı prototipleme. kaynak

Benzetimli tavlama

Bir bilgisayar, zor bir eniyileme problemine iyi bir çözüm bulmak için bir atom ya da tasarım modelini yavaşça soğutur; arada daha kötü düzenlemeleri de kabul eder.

Yanıtladığı soru: Astronomik sayıda olasılık arasında en iyiye yakın yerleşim ya da takvim nedir?

Dışarıda bıraktığı: En iyi yanıt için hiçbir garanti vermez ve sonuçlar soğutma çizelgesine bağlıdır.

Çalıştığı yer: yaklaşık 10¹² FLOPS yaklaşık bir çip yerleşimi için bir iş istasyonunda saatler.Şu tarihten beri: 1983 Kirkpatrick, Gelatt ve Vecchi'nin benzetimli tavlamayla eniyileme çalışması. kaynak

Yaklaşık Bayesci hesaplama

Bir simülatör birçok deneme parametre değeriyle çalıştırılır ve gözlenen veriye yakın veri üretenler tutulur; hangi değerlerin makul olduğuna dair bir tablo verir.

Yanıtladığı soru: Karmaşık bir modelin hangi ayarları gözlediğimiz veriyi üretebilirdi?

Dışarıda bıraktığı: Sonuç, verinin hangi özetlerinin kullanıldığına ve bir eşleşmenin sayılması için ne kadar yakın olması gerektiğine bağlıdır.

Çalıştığı yer: yaklaşık 10¹³ FLOPS yaklaşık bir kümede milyonlarca simülatör çalışması.Şu tarihten beri: 1997 Tavaré ve arkadaşlarının DNA dizisi verisinden simülasyonla birleşme zamanlarını çıkarması. kaynak