Matematika at pagkukuwenta

Mga eksperimento sa random matrix

Malalaking matrix na puno ng random na numero, paulit-ulit na dina-diagonalise para pag-aralan ang estadistika ng kanilang mga eigenvalue.

Tanong na sinasagot nito: Anong padron ang kinahihinatnan ng mga eigenvalue ng random na matrix, at tumutugma ba ito sa ibang larangan ng matematika at pisika?

Hindi kasama: Isang maliit na sulok lang ng walang hanggang espasyo ng mga posibleng matrix ang kinukuha.

Tumatakbo sa: mga 10¹² FLOPS magaspang isang university cluster na bumubuo at nagdi-diagonalise ng maraming malalaking matrixMula: 1955 Ang maagang gawa ni Wigner sa istatistika ng eigenvalue ng random matrix

Mga eksperimento sa random graph

Mga graph na binuo sa pamamagitan ng random na tuntunin, node por node o edge por edge, para makita kung anong mga katangian, tulad ng koneksyon o clustering, ang karaniwang lumilitaw.

Tanong na sinasagot nito: Ano ang hitsura ng isang 'tipikal' na network sa ilalim ng tuntuning ito sa pagdaragdag ng mga node at edge?

Hindi kasama: Bihirang kasing-linis ng tuntuning lumilikha sa modelo ang mga tunay na network.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang tumatakbo sa isang desktop para sa mga graph hanggang milyun-milyong nodeMula: 1959 Ang random graph na modelo nina Erdos at Renyi

Simulasyon ng percolation

Isang lattice o network na may mga site o bond na binubuksan nang random, binabantayan hanggang sa punto kung kailan biglang sumasaklaw sa buong sistema ang isang konektadong landas.

Tanong na sinasagot nito: Sa anong densidad biglang nagiging magkakakonekta mula dulo hanggang dulo ang isang random na network?

Hindi kasama: Mas malinis ang kilos ng mga idealisadong lattice kaysa sa anumang tunay na porous na materyal o network.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang isang desktop na makina para sa malalaking lattice sweepMula: 1957 Ang pagpapakilala nina Broadbent at Hammersley sa percolation theory

Mga paghahanap sa experimental mathematics

Brute-force na numerikal na paghahanap ng mga pattern, counterexample o eksaktong ugnayan sa pagitan ng mga numero, pinatakbo nang higit pa sa kayang suriin ng kamay.

Tanong na sinasagot nito: Totoo ba ang haka-hakang ito sa bawat kasong kayang suriin ng sinuman, at lumilitaw ba ang padron?

Hindi kasama: Walang dami ng nasuring kaso ang patunay, gaano man karami ang lumabas na totoo.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang isang university cluster na tumatakbo nang ilang araw sa iisang paghahanapMula: 1963 pagsapit ng 1963, mga paghahanap ng kompyuter sa mga integer relation at pattern ng prime

Monte Carlo na pagtataya ng mga konstante

Random sampling na ginagamit para tantiyahin ang mathematical constant o integral, tulad ng pagbuhos ng mga punto para tantiyahin ang isang area, bilang ehersisyo at hindi para sa pisikal na modelo.

Tanong na sinasagot nito: Gaano katumpak matutukoy ng bulag na random sampling lamang ang isang eksaktong mathematical na dami?

Hindi kasama: Mas mabagal ang convergence kaysa sa halos anumang mas sopistikadong numerikal na paraan.

Tumatakbo sa: mga 10⁹ FLOPS magaspang tumatakbo sa isang laptop sa loob ng segundo hanggang minutoMula: 1946 ideya ni Ulam noong 1946; nagmungkahi si von Neumann ng bersyong electronic-computer noong Marso 1947, at unang nailathala ang pamamaraan noong 1949 pinagmulanSa simulations tree: Pamamaraang Monte Carlo

Patakbuhin ang interactive na modelo

Mga paghahanap sa computational number theory

Malalaking numerong sinusubok kung prime, pinag-aaralang i-factor, o hinahanapan ng espesyal na katangian tulad ng mga perpektong numero, gamit ang mga algorithm na pinatatakbo nang malakihan sa halip na mano-mano.

Tanong na sinasagot nito: May katangiang hinahanap ba natin ang napakalaking numerong ito, at hanggang saan maitutulak ng paghahanap ang rekord?

Hindi kasama: Kaunti ang sinasabi ng mga paghahanap na nakabasag ng rekord tungkol sa mga numerong wala pang nag-isip suriin.

Tumatakbo sa: mga 10¹³ FLOPS magaspang isang distributed na proyekto ng volunteer computing sa maraming ipinagkaloob na makinaMula: 1951 Mano-manong pagsubok ni Lucas para sa mga Mersenne prime, unang pinatakbo ng kompyuter noong 1951

Numerika ng chaotic attractor

Isang maliit na hanay ng mga nonlinear na equation na iniintegrate hakbang por hakbang para ipakita ang sensitibong pagdepende sa mga paunang kondisyon at isang fractal na attractor.

Tanong na sinasagot nito: Bakit nagiging hindi mahulaan ang isang simpleng deterministikong sistema?

Hindi kasama: Dahil sa numerical rounding, hindi tunay na orbit ang mahabang trajectory, kundi isang nananatiling malapit sa isa.

Tumatakbo sa: mga 10³ FLOPS magaspang ilang equation, ilang segundo sa isang laptop.Mula: 1963 Deterministic nonperiodic flow ni Lorenz, isang convection model na pinatakbo sa kompyuter. pinagmulanSa simulations tree: Magulong convection ni Lorenz

Mga nonlinear na lattice experiment

Isang kadena ng mga masa na may nonlinear na spring, sinimulan sa isang mode at sinusundan para makita kung pantay-pantay bang kakalat ang enerhiya, gaya ng ipinahihiwatig ng termodinamika.

Tanong na sinasagot nito: Pantay bang ibinabahagi ng isang nonlinear na kadena ang enerhiya nito sa lahat ng galaw nito?

Hindi kasama: Nakasalalay ang mga resulta sa napiling chain at paunang estado.

Tumatakbo sa: mga 10³ FLOPS magaspang maliit sa pamantayan ngayon; ilang dosenang masa ang ginamit ng orihinal.Mula: 1955 Ang mga pag-aaral nina Fermi, Pasta at Ulam sa mga nonlinear na problema sa isang maagang digital na kompyuter. pinagmulan

Mga numerikal na eksperimento sa soliton

Isang nonlinear na wave equation na nilulutas sa isang grid para mapanood ang mga pulso na nagtatawid sa isa't isa at nananatili ang hugis, na hindi ginagawa ng mga linear na alon.

Tanong na sinasagot nito: Bakit nagdadaanan nang walang pagbabago ang ilang nonlinear na alon?

Hindi kasama: Isang pamilya ng mga ekwasyon ang ipinapakita nito, hindi ang pangkalahatang kilos ng mga nonlinear na alon.

Tumatakbo sa: mga 10⁴ FLOPS magaspang isang one-dimensional na grid, madali ngayon.Mula: 1965 Ang interaksyon ng mga soliton sa collisionless na plasma at ang pag-ulit ng mga panimulang estado nina Zabusky at Kruskal. pinagmulan

Pag-render ng fractal-set

Isang simpleng iterated na pormula na sinusubok sa bawat lokasyon sa complex plane para makita kung tumatakas ito, na iginuguhit ang hangganan ng hanay ng mga matatag na punto.

Tanong na sinasagot nito: Ano ang hugis ng hanay kung saan nananatiling may hangganan ang isang simpleng iteration?

Hindi kasama: Pahiwatig lang ng pagiging miyembro ang mga escape test, at ang larawan ay finite-resolution na sampling ng isang hanay na walang hanggan ang detalye.

Tumatakbo sa: mga 10⁹ FLOPS magaspang ang malalalim na pag-zoom ay nangangailangan ng extended-precision na iteration sa milyun-milyong punto.Mula: 1980 Mandelbrot's fractal aspects of the iteration of z to lambda z(1-z), first computer images of the Mandelbrot set. pinagmulan

Sandpile na self-organised criticality

Mga butil na ibinabagsak sa isang grid at gumuguho kapag masyadong matarik, na nagbibigay ng mga pagguho ng bawat laki nang walang pag-aayos, bilang modelo kung paano umaabot ang mga sistema sa kritikal na estado.

Tanong na sinasagot nito: Bakit lumilitaw ang mga avalanche sa bawat laki nang walang anumang pag-aayos?

Hindi kasama: Pinagtatalunan kung iisa ang scaling ng mga tunay na sistema.

Tumatakbo sa: mga 10⁹ FLOPS magaspang mahahabang takbo sa malalaking grid para makita ang scaling.Mula: 1987 Ang self-organised criticality nina Bak, Tang at Wiesenfeld: paliwanag sa 1/f noise. pinagmulan

Pagkalkula ng zero ng Riemann zeta

Kinukuwenta ang mga halaga ng zeta function sa kahabaan ng kritikal na linya nito para hanapin at bilangin ang mga zero nito, at tiyaking nasa lugar na sinasabi ng hypothesis ang mga ito.

Tanong na sinasagot nito: Nasa iisang linya ba ang lahat ng hindi-trivial na zero ng zeta function?

Hindi kasama: Hindi mapapatunayan ng isang may hangganang pagsusuri, gaano man kahaba, na walang zero sa labas ng linya na lampas dito.

Tumatakbo sa: mga 10¹⁸ FLOPS magaspang mga dekada ng oras ng CPU sa pinakamalalaking paghahanap.Mula: 1953 Ang mga kuwenta ni Turing ng Riemann zeta function. pinagmulan

Mga digit ng pi sa pamamagitan ng kompyuter

Sinusuma ang mga serye para sa pi hanggang sa napakaraming digit gamit ang eksaktong aritmetika, na sinusubok kapwa ang numero at ang makina.

Tanong na sinasagot nito: Mukha bang random ang mga digit ng pi, at mapagkakatiwalaan ba ang makina sa ganitong sukat?

Hindi kasama: Walang sinasagot na bukás na tanong ang mga digit, at nahuhuli lang ng mga pagsusuri ang mga error ng hardware kung malaya ang pamamaraan.

Tumatakbo sa: mga 10¹⁷ FLOPS magaspang buwan sa isang server para sa daan-daang trilyong digit.Mula: 1950 Reitwiesner's ENIAC determination of pi and e to more than 2000 decimal places (published 1950, reprinted in Pi: A Source Book). pinagmulan

Pagtuklas ng conjecture na ginagabayan ng AI

Natutukoy ng machine learning sa malalaking talahanayan ng mga mathematical na bagay kung aling mga katangian ang magkakaugnay, para magmungkahi ng haka-haka na susubukan namang patunayan ng mga matematiko.

Tanong na sinasagot nito: Aling hindi pa nakikitang ugnayan sa pagitan ng mga dami sa matematika ang sulit patunayan?

Hindi kasama: Nagmumungkahi lang ito ng mga padron at wala itong napatutunayan, at ang ilang regularidad sa datos ay maaaring artifact ng paraan ng paggawa ng datos.

Tumatakbo sa: mga 10¹⁵ FLOPS magaspang mga araw sa ilang GPU bawat dataset.Mula: 2021 Ang pagpapaunlad ng matematika sa paggabay sa intuwisyon ng tao gamit ang AI nina Davies at mga kasamahan. pinagmulan

Pag-aaral ng learned algorithm at construction search

Isang sistemang naglalaro ng laro o language model ang naghahanap ng mga bagong pamamaraan o bagay na matematikal, at sinusuri ng kompyuter ang kawastuhan ng bawat kandidato.

Tanong na sinasagot nito: Makatutuklas ba ang isang programa ng mas mabilis na algorithm o mas malaking halimbawa kaysa sa natagpuan ng mga tao?

Hindi kasama: Bawat resulta ay iisang bagong halimbawa, at saklaw lang ng paghahanap ang mga uri ng bagay na inilarawan ng mga nagdisenyo nito bilang laro.

Tumatakbo sa: mga 10¹⁷ FLOPS magaspang mga araw hanggang linggo sa mga accelerator cluster.Mula: 2022 Ang AlphaTensor nina Fawzi at mga kasamahan, na tumutuklas ng mas mabibilis na matrix multiplication algorithm gamit ang reinforcement learning. pinagmulan

Model checking

Bawat maaabot na estado ng isang may hangganang sistema, gaya ng protocol o disenyo ng circuit, inililista nang isa-isa ng kompyuter para tingnan kung totoo ang isang katangian sa lahat ng ito.

Tanong na sinasagot nito: May naaabot bang estado kung saan nilalabag ng disenyong ito ang sarili nitong mga tuntunin?

Hindi kasama: Sumasabog ang mga state space nang higit sa kayang suriin, kaya pinasisimple muna ang mga tunay na disenyo.

Tumatakbo sa: mga 10¹² FLOPS magaspang isang university cluster na umuubos sa malaki ngunit may hangganang state spaceMula: 1981 Ang pagpapakilala nina Clarke at Emerson sa model checking

Paghahanap ng awtomatikong theorem proving

Isang paghahanap sa mga kadena ng lohikal na hinuha, binubuo ng kompyuter hakbang por hakbang, naghahanap ng patunay o pagpapabulaan sa isang pahayag na matematikal.

Tanong na sinasagot nito: May umiiral bang wastong kadena ng lohikal na hakbang mula sa mga axiom hanggang sa pahayag na ito?

Hindi kasama: Nakakahanap ng mga patunay na walang taong pipili, at kung minsan ay wala talagang mahanap na kaya nitong abutin.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang isang university cluster na naghahanap sa loob ng mga oras hanggang arawMula: 1956 ang Logic Theorist, isang maagang programang awtomatikong naghahanap ng patunay

SAT at constraint solving

Milyun-milyong kumbinasyon ng totoo o hindi totoong halaga na sistematikong hinahanap para matugunan ang malaking hanay ng lohikal na limitasyon, na ginagamit sa pag-iiskedyul, pagruruta o pagberipika ng disenyo.

Tanong na sinasagot nito: May anumang pagtatalaga ba ng mga halaga na sabay-sabay na tumutupad sa lahat ng limitasyong ito?

Hindi kasama: May mga instance na sapat ang hirap kaya walang solver, gaano man kahusay, ang matatapos sa tamang oras.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang isang workstation hanggang cluster, depende sa laki ng problemaMula: 1962 ang pamamaraang Davis-Putnam para sa paghahanap ng satisfiability

Pagmomodelo ng cryptographic na atake

Isang code o key-exchange scheme na inaatake nang milyun-milyong beses sa simulation, sa pamamagitan ng brute force, statistical bias o isang imodelong kahinaan, para masukat kung gaano talaga kalaking pagsisikap ang kailangan para basagin ito.

Tanong na sinasagot nito: Ilang operasyon ang aktuwal na kakailanganin para mabasag ito, at ligtas pa rin bang malaki ang bilang na iyon?

Hindi kasama: Sinusubok lang ang mga atakeng naisip imodelo ng analyst, hindi ang wala pang nakakahanap.

Tumatakbo sa: mga 10¹⁴ FLOPS magaspang isang distributed na cluster ng maraming makina na nagpapatakbo ng mga pagsubok sa pag-atakeMula: 1976 pagsapit ng 1976, computational na pagsusuri sa lakas ng cipher at key-exchange

Simulasyon ng side-channel leakage

Ang konsumo ng kuryente, tiyempo o electromagnetic na emisyon ng isang device habang nagsasagawa ng cryptographic na operasyon, na minomodelo para makita kung ano ang matututuhan ng nakikinig sa labas.

Tanong na sinasagot nito: Gaano karami sa lihim na susi ang tumatagas sa pisikal na kilos ng device, hindi sa matematika?

Hindi kasama: Mas malinis na signal ang nahuhuli ng kondisyon sa laboratoryo kaysa karaniwang ibinibigay ng maingay na tunay na device.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang isang workstation na nagmomodelo ng power o timing trace ng isang aparatoMula: 1996 Pagpapakita ni Kocher ng mga timing attack sa mga cryptographic na implementasyon

Beripikasyon ng security protocol

Bawat mensaheng maaaring ipadala, ulitin o pekein ng umaatake sa isang communication protocol, inililista nang isa-isa ng kompyuter para tingnan kung maaaring pilitin ang paglabas ng sikreto o pagkakakilanlan mula rito.

Tanong na sinasagot nito: Maloloko ba ng anumang sunud-sunod na mensahe ang protocol na ito para ilabas ang sikreto o tumanggap ng pekeng pagkakakilanlan?

Hindi kasama: Bineberipika ang protocol ayon sa tinukoy, hindi ang mga shortcut ng tunay na implementasyon.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang isang workstation hanggang cluster na sumusuri sa message space ng isang protocolMula: 1989 ang modelong Dolev-Yao, isang pundasyon ng beripikasyon ng protocol

Computer-assisted na patunay sa pamamagitan ng ubos-kasong pagsusuri

Isang teorema na pinaliit sa may hangganang listahan ng mga kaso, bawat isa ay sinusuri ng programa, dahil walang tao ang makakasuri sa lahat ng ito.

Tanong na sinasagot nito: Makukumpleto ba ng isang makina ang isang patunay sa pagsuri sa bawat kaso?

Hindi kasama: Lumilipat ang tiwala sa programa, hardware at argumento ng case-reduction.

Tumatakbo sa: mga 10⁹ FLOPS magaspang mga isang libong oras sa mainframe para sa orihinal; mas kaunti na ngayon.Mula: 1977 Ang patunay nina Appel at Haken na ang bawat planar na mapa ay maaaring kulayan ng apat na kulay, gamit ang reducibility na sinuri ng kompyuter. pinagmulan

Validated numerics

Mga kalkulasyong isinasagawa na may garantisadong mga hangganan, kaya pinatutunayan ng numerikal na resulta ang isang pahayag na matematikal, gaya ng pag-iral ng chaotic attractor.

Tanong na sinasagot nito: Mapapatunayan bang tama ang isang sagot na kinompyut, hindi lang malamang na tumpak?

Hindi kasama: Maaaring lumobo ang mga hangganan sa mahahabang panahon, kaya nalilimitahan ang mga patunay sa maikli o maayos na mga problema.

Tumatakbo sa: mga 10⁹ FLOPS magaspang pinararami ng interval arithmetic ang gastos sa katamtamang salik.Mula: 2002 Ang mahigpit na ODE solver ni Tucker at ang ika-14 na problema ni Smale, na nagpapatunay na umiiral ang Lorenz attractor. pinagmulan

Pagbilang ng Turing machine

Bawat maliit na programa ng isang minimal na makina ay pinatakbo para makita kung alin ang humihinto at alin ang tumatakbo magpakailanman, para mahanap ang pinakamatagal tumakbong humihinto sa bawat laki.

Tanong na sinasagot nito: Gaano katagal tatakbo ang isang maliit na programa bago ito huminto?

Hindi kasama: Ang undecidability ay nangangahulugang may mga makinang hindi kailanman maiuuri, gaano man katagal tumakbo.

Tumatakbo sa: mga 10¹⁵ FLOPS magaspang bilyun-bilyong makina, na may mga patunay para sa mga hindi humihinto.Mula: 1965 Mga pag-aaral sa kompyuter nina Lin at Rado ng mga problema ng Turing machine. pinagmulan

Statistical model checking

Isang sistemang may random na kilos na sini-simulate nang maraming beses para matantiya nang may kumpiyansa kung gaano kalamang nitong labagin ang isang katangian.

Tanong na sinasagot nito: Gaano kalamang lumabag sa tuntunin ng kaligtasan ang isang random na sistema?

Hindi kasama: Ang mga istatistikal na takbo ay nagbibigay ng probabilidad na may antas ng kumpiyansa, hindi patunay, at ang mga bihirang pagkabigo ay nangangailangan ng importance sampling.

Tumatakbo sa: mga 10⁹ FLOPS magaspang libu-libo hanggang milyun-milyong sinampol na pagpapatakbo.Mula: 2002 Ang probabilistic verification ng discrete event system gamit ang acceptance sampling nina Younes at Simmons. pinagmulan

Fuzz testing

Isang programang pinapakain ng napakaraming random o binagong input para hanapin ang mga nagpapa-crash dito, sa katunayan ay nagsi-simulate ng isang mapanganib o pabayang mundo.

Tanong na sinasagot nito: Anong input ang magpapabigo sa software na ito?

Hindi kasama: Natutukoy lang nito ang mga pagkabigong naaabot ng mga random na input, at maaaring pumasa ang programa sa loob ng mga taon habang nagtatago ng bug sa likod ng bihirang kaso.

Tumatakbo sa: mga 10¹⁴ FLOPS magaspang machine-year ng CPU time para sa isang malaking code base.Mula: 1990 Pag-aaral nina Miller, Fredriksen at So na empirikal sa pagiging maaasahan ng mga UNIX utility. pinagmulan

Symbolic execution

Isang programang pinatatakbo na may mga di-alam na input na isinusulat bilang mga simbolo, kinokolekta ang mga kondisyon sa bawat landas, saka naghahanap ang isang solver ng mga halagang tatahak sa bawat sangay.

Tanong na sinasagot nito: Anong mga input ang nagpapatakbo sa bawat landas ng programang ito, at may aabot ba sa bug?

Hindi kasama: Eksponensiyal na lumalaki ang bilang ng mga landas kasabay ng laki ng programa, kaya bahagi lang ng malalaki ang nasasaklaw.

Tumatakbo sa: mga 10¹² FLOPS magaspang oras ng solver bawat programa, na tumataas nang matarik kasabay ng bilang ng path.Mula: 1976 King's symbolic execution and program testing. pinagmulan

Abstract interpretation

Isang programang pinatatakbo sa mga hanay ng posibleng halaga, gaya ng mga saklaw, sa halip na iisang halaga, para patunayan ang mga katangiang totoo sa bawat input.

Tanong na sinasagot nito: Maaari bang mag-divide by zero o mag-overflow ang programang ito, para sa anumang input?

Hindi kasama: Nagdudulot ng maling alarma ang ligtas na approximation, kaya dapat pa ring suriin ng mga tao ang bawat babala.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang oras sa isang workstation para sa malaking code base ng avionics.Mula: 1977 Ang abstract interpretation nina Cousot at Cousot, isang pinag-isang lattice model para sa static analysis ng mga programa. pinagmulan

Bounded model checking

Isinusulat bilang logic formula ang kilos ng isang disenyo hanggang sa takdang bilang ng hakbang at ibinibigay sa satisfiability solver para humanap ng anumang maikling landas patungo sa bug.

Tanong na sinasagot nito: Makararating ba ang circuit o programang ito sa estado ng error sa loob ng takdang bilang ng hakbang?

Hindi kasama: Wala itong napatutunayan lampas sa hangganan ng hakbang maliban kung ipinapakita ng hiwalay na argumento na sapat ito.

Tumatakbo sa: mga 10¹³ FLOPS magaspang oras sa isang server bawat ari-arian.Mula: 1999 Ang symbolic model checking nina Biere, Cimatti, Clarke at Zhu nang walang BDD. pinagmulan

Property-based na random testing

Isang tuntuning dapat laging totoo ang itinatakda, at gumagawa ang kompyuter ng maraming random na kaso at pinaliliit ang anumang pagkabigo tungo sa maliit na counterexample.

Tanong na sinasagot nito: Sinusunod ba ng code na ito ang sarili nitong espesipikasyon sa malawak na hanay ng input?

Hindi kasama: Maaaring hindi kailanman maabot ng mga random na kaso ang bihirang kondisyon, at maaaring hindi ang nakasulat na katangian ang mahalaga.

Tumatakbo sa: mga 10⁹ FLOPS magaspang minuto sa isang laptop para sa libu-libong kaso.Mula: 2000 Ang QuickCheck nina Claessen at Hughes, isang magaan na kagamitan para sa random na pagsubok ng mga programang Haskell. pinagmulan

Beripikasyon ng neural network

Pinatutunayan ng mga constraint solver na para sa bawat input sa isang rehiyon, nananatili sa loob ng hangganan ang output ng neural network, sa halip na subukan ang mga sample.

Tanong na sinasagot nito: Maaari bang magbigay ng maling sagot ang network dahil sa maliit na pagbabago sa input?

Hindi kasama: Para lang sa maliliit na network ang mga patunay, at makitid ang hanay ng mga perturbation na masusuri.

Tumatakbo sa: mga 10¹³ FLOPS magaspang oras hanggang araw sa isang server para sa maliit na network.Mula: 2017 Ang Reluplex nina Katz at mga kasamahan, isang SMT solver para sa pagberipika ng mga deep neural network. pinagmulan

Simulation ng computer architecture

Ang pipeline, cache at branch predictor ng isang iminungkahing processor ay imodelo instruksyon por instruksyon, para tantiyahin ang bilis ng isang chip bago ito gawin.

Tanong na sinasagot nito: Gaano kabilis tatakbo ang disenyo ng processor na ito sa mga tunay na programa, bago pa mag-ukit ng silicon?

Hindi kasama: Sapat ang pagpapasimple sa tunay na chip kaya laging bahagyang iba ang huling silicon sa modelo.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang isang university cluster na nagpapatakbo ng mga benchmark program sa modeloMula: 1990 pagsapit ng 1990, mga cycle-accurate na processor simulator para sa pananaliksik sa arkitektura

Simulation ng distributed system at consensus

Maraming kompyuter na ginawang modelo, nagpapadala ng mensahe sa isa't isa na may delay, pagkawala at pagkabigo, para subukin kung nagkakasundo pa rin ang isang distributed algorithm sa tamang sagot.

Tanong na sinasagot nito: Naaabot pa rin ba ng algorithm na ito ang tamang kasunduan kapag nawala o naantala ang mga mensahe o nag-crash ang mga node?

Hindi kasama: Ang mga ini-inject na pagkabigo ay ang mga inasahan ng nagdisenyo, hindi ang mga biglang lumilitaw sa produksiyon.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang isang cluster na nagsi-simulate ng daan-daang virtual na nodeMula: 1978 Maagang gawa ni Lamport sa pagkakasunud-sunod at pagkabigo sa mga distributed system

Simulasyon ng mga sistema ng imbakan

Mga disk, drive at file system na imodelo kung paano nila inilalatag ang datos, nabibigo at bumabawi, para subukan ang disenyo ng storage bago bumili at punuin ng totoong drive.

Tanong na sinasagot nito: Gaano kahusay at katibay sa pagkabigo ang disenyo ng imbakang ito, sa laking masyadong mahal para subukan muna nang totoo?

Hindi kasama: Mas magulo at mas magkakaugnay ang pagkabigo ng mga tunay na drive kaysa sa random na rate ng pagkabigo ng modelo.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang isang workstation hanggang maliit na cluster na nagmomodelo ng storage arrayMula: 1988 pagsapit ng 1988, mga simulation model ng pagiging maaasahan ng disk array

Simulasyon ng scheduler ng operating system

Isang daloy ng mga gawaing pangkompyut na imodelo habang dumarating at nakikipagpaligsahan para sa isang processor, pinatakbo laban sa iba't ibang tuntunin sa pag-iiskedyul para makita kung alin ang pinakamakatarungan o pinakamabilis.

Tanong na sinasagot nito: Aling paraan ng pag-aayos ng pila ng mga gawain ang pinakamaraming natatapos, o pinakapatas sa bawat gawain?

Hindi kasama: Bihirang tumugma ang mga sintetikong workload sa hindi pantay na halo ng gawaing nakakaharap ng tunay na makina.

Tumatakbo sa: mga 10⁹ FLOPS magaspang tumatakbo sa laptop o workstation sa loob ng segundo hanggang minutoMula: 1968 pagsapit ng 1968, mga simulation study ng mga patakaran sa pag-iiskedyul ng processor

Paghahanap sa pag-optimize ng compiler at programa

Napakaraming maliliit na pagkakaiba ng isang piraso ng code ang sinubukan at sinukat, naghahanap ng pinakamabilis o pinakamaikling bersyon na ginagawa pa rin ang parehong trabaho.

Tanong na sinasagot nito: Sa lahat ng katumbas na paraan ng pagsulat ng maliit na piraso ng code na ito, alin ang aktuwal na pinakamabilis?

Hindi kasama: Minsan kakaiba nang husto ang mga programang nahahanap kaya walang paliwanag kung bakit gumagana ang mga ito.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang isang cluster na naghahanap sa malawak na espasyo ng mga bersyon ng codeMula: 2006 pagsapit ng 2006, superoptimisation search sa mga maikling sunud-sunod na instruksyon

Empirikal na pagsubok sa pagganap ng algorithm

Isang algorithm na pinatatakbo nang libu-libong beses sa mga random na nabuo o totoong input na lumalaki ang sukat, sinusukat kung paano talaga lumalaki ang oras ng pagtakbo nito sa halip na patunayan ito sa papel.

Tanong na sinasagot nito: Paano aktuwal na lumalaki sa praktika ang oras ng pagtakbo ng algorithm na ito, sa mga input na talagang makikita nito?

Hindi kasama: Ang pinakamasamang kaso na wala sa mga test input ay nananatiling hindi natutuklasan hanggang sa mangyari ito.

Tumatakbo sa: mga 10⁹ FLOPS magaspang tumatakbo sa isang workstation sa maraming nalikhang test inputMula: 1970 pagsapit ng 1970, sistematikong empirikal na pagsubok ng oras ng pagtakbo ng algorithm

Pagpapatakbo ng programa gamit ang language model

Isang language model ang nagsusulat ng sunud-sunod na pansamantalang estado habang sinusundan nito ang ikokompyut ng isang programa.

Tanong na sinasagot nito: Maaari bang gayahin ng isang language model ang pagtakbo ng code?

Hindi kasama: Hindi garantisadong tama ang output, at pumapalya ang mahahabang programa.

Tumatakbo sa: mga 10¹⁴ FLOPS magaspang Inference bawat queryMula: 2021 Show your work: scratchpads for intermediate computation with language models (2021) pinagmulan

Simulation ng blockchain consensus

Isang network ng mga node na gumagawa at nagbabahagi ng mga bloke sa gitna ng mga pagkaantala, para subukan kung paano nakakaapekto sa seguridad at throughput ang laki ng bloke, tiyempo at mga umaatake.

Tanong na sinasagot nito: Gaano kaligtas at kabilis ang isang blockchain sa ilalim ng delay at atake sa network?

Hindi kasama: Bahagya lang nasusukat ang tunay na kilos ng node at topolohiya ng network.

Tumatakbo sa: mga 10⁸ FLOPS magaspang mga event-driven na takbo ng libu-libong node.Mula: 2016 Ang pagsusuri nina Gervais at mga kasamahan sa seguridad at pagganap ng mga proof-of-work na blockchain gamit ang simulator. pinagmulan

Parallel discrete-event simulation

Isang simulation ng mga pangyayari sa oras na hinahati sa maraming processor na bawat isa ay nagpapausad ng sariling orasan at umaatras kapag may dumating na huli.

Tanong na sinasagot nito: Paano mapapatakbo nang mabilis sa maraming makina ang isang napakalaking event-driven na simulation, gaya ng network o larangan ng digmaan?

Hindi kasama: Maaaring mag-cascade ang mga rollback, at lubhang nakasalalay ang bilis sa kung gaano kahigpit ang pagkakabit ng mga pangyayari.

Tumatakbo sa: mga 10¹⁴ FLOPS magaspang oras sa isang supercomputer para sa bilyun-bilyong pangyayari.Mula: 1985 Virtual time ni Jefferson, ang mekanismong Time Warp para sa optimistikong pag-synchronise. pinagmulan

Simulasyon ng arkitektura ng graphics processor

Ang mga core, warp at memorya ng isang graphics processor ay imodelo cycle por cycle, nagpapatakbo ng totoong programa para suriin ang disenyo bago ito itayo.

Tanong na sinasagot nito: Paano makaaapekto ang pagbabago sa disenyo sa bilis ng mga parallel na programa sa isang graphics chip?

Hindi kasama: Lihim o hindi alam ang mga detalye ng totoong chip, kaya tinatayang tumutugma lamang ang modelo sa mga numero ng umiiral na disenyo.

Tumatakbo sa: mga 10¹² FLOPS magaspang oras hanggang araw ng host time bawat segundo ng simulate na pagpapatakbo.Mula: 2009 Pagsusuri nina Bakhoda at mga kasamahan sa mga workload ng CUDA gamit ang detalyadong GPU simulator. pinagmulan

FPGA-accelerated na system simulation

Ikinakarga ang disenyo ng isang chip sa maraming reconfigurable na circuit na nagpapatakbo nito nang eksakto sa bawat cycle sa bilis na megahertz, na nagsi-simulate ng buong server at mga network ng mga ito.

Tanong na sinasagot nito: Paano kikilos ang processor na ito at ang cluster nito habang nagpapatakbo ng tunay na software, bago ito gawin?

Hindi kasama: Mas mabagal ito nang husto kaysa sa tunay na chip, at hindi mapapatakbo ang disenyong hindi kasya sa mga circuit.

Tumatakbo sa: mga 10¹⁵ FLOPS magaspang mga araw sa isang cloud ng daan-daang reconfigurable na circuit.Mula: 2018 Ang FireSim nina Karandikar at mga kasamahan, FPGA-accelerated na cycle-exact na scale-out system simulation sa pampublikong cloud. pinagmulan

Full-system simulation

Isang buong kompyuter, may mga processor, memorya, disk at network card, na sini-simulate nang sapat para mag-boot ng hindi binagong operating system at patakbuhin ang mga programa nito.

Tanong na sinasagot nito: Paano kumikilos ang tunay na software sa isang makinang wala pa, o na maaaring i-pause at i-replay anumang oras?

Hindi kasama: Tinatantiya ang tiyempo para sa bilis, kaya hindi nito maibibigay ang eksaktong performance, kundi ang functional na kilos lang.

Tumatakbo sa: mga 10¹¹ FLOPS magaspang halos real time sa isang server bawat simulate na makina.Mula: 2002 Ang Simics nina Magnusson at mga kasamahan, isang full-system simulation platform. pinagmulan

Magaang network emulation

Dose-dosena o daan-daang virtual na host at switch na nagpapatakbo ng totoong network software sa isang laptop, magkakaugnay ng mga emulated na kable na may itinakdang bilis at pagkaantala.

Tanong na sinasagot nito: Gagana ba sa buong topolohiya ang programang ito sa pagkontrol ng network bago i-deploy?

Hindi kasama: Ibinabahagi ng lahat ng virtual node ang sariling processor ng host, kaya bumabagal ang mabibilis na link.

Tumatakbo sa: mga 10¹⁰ FLOPS magaspang real time sa isang workstation.Mula: 2010 Lantz, Heller and McKeown's 'A network in a laptop', rapid prototyping for software-defined networks. pinagmulan

Simulated annealing

Dahan-dahang pinalalamig ng kompyuter ang isang modelo ng mga atomo o ng isang disenyo, kung minsan ay tumatanggap ng mas masamang ayos, para makahanap ng magandang solusyon sa isang mahirap na optimization problem.

Tanong na sinasagot nito: Ano ang halos pinakamahusay na ayos o iskedyul sa gitna ng napakaraming posibilidad?

Hindi kasama: Walang garantiya ng pinakamahusay na sagot, at nakasalalay ang mga resulta sa iskedyul ng paglamig.

Tumatakbo sa: mga 10¹² FLOPS magaspang oras sa isang workstation para sa paglalagay ng chip.Mula: 1983 Kirkpatrick, Gelatt and Vecchi's optimisation by simulated annealing. pinagmulan

Approximate Bayesian computation

Isang simulator ang pinatatakbo sa maraming trial na halaga ng parameter, at itinatago ang mga nagbubunga ng datos na malapit sa nakitang datos, na nagbibigay ng larawan kung aling mga halaga ang kapani-paniwala.

Tanong na sinasagot nito: Aling mga setting ng masalimuot na modelo ang maaaring gumawa ng datos na nakikita natin?

Hindi kasama: Nakadepende ang resulta sa kung aling buod ng datos ang ginamit at kung gaano kalapit ang tugma para mabilang.

Tumatakbo sa: mga 10¹³ FLOPS magaspang milyun-milyong takbo ng simulator sa isang cluster.Mula: 1997 Ang inference nina Tavaré at mga kasamahan ng mga oras ng coalescence mula sa datos ng pagkakasunod-sunod ng DNA gamit ang simulasyon. pinagmulan