Dhana ya Uigaji
Uigajifani 12 kati ya 18

Hisabati na ukokotoaji

Namba, uthibitisho, grafu na mashine, zinazochunguzwa kwa ukokotoaji pamoja na kwa hoja ya kimantiki.

Hisabati na sayansi ya kompyuta sasa hujaribu mawazo yake kwa uigaji. Huzalisha mamilioni ya grafu nasibu kuona kipi ni cha kawaida. Huendesha mashine kuona algoriti hufanya nini kweli. Hushambulia msimbo wa siri mara kwa mara kujifunza jinsi unavyoshindwa. Hakuna kati ya haya kinachoelezea ulimwengu wa kimwili. Huchunguza nafasi ya nambari, miundo na ukokotoaji wenyewe. Mazoezi haya huanzia hisabati ya majaribio iliyofanywa kwa mkono kwa karne nyingi hadi zana za kisasa za uthibitishaji zinazokagua muundo dhidi ya kila hali inayofikika kabla haujajengwa.

Hisabati safi kwa kompyuta

Majaribio ya matriki za nasibu

Matriki makubwa yaliyojazwa nambari nasibu, yakigeuzwa kuwa diagonali mara kwa mara ili kusoma takwimu za thamani zake za eigen.

Swali linalojibiwa: Mchoro gani thamani-eigeni za matriki nasibu hutulia ndani yake, na unalingana na maeneo mengine ya hisabati na fizikia?

Inaacha nje: Huchukua sampuli ya kona ndogo tu ya nafasi isiyo na kikomo ya matriki zinazowezekana.

Huendeshwa kwenye: takriban 1012 FLOPS takriban kundi la kompyuta la chuo kikuu linalozalisha matriksi nyingi kubwa na kuzifanya diagonaliTangu: 1955 Kazi ya mapema ya Wigner kuhusu takwimu za thamani-eigeni za matriki nasibu

Monte Carlokiwango cha chini: Kanuni

Majaribio ya grafu za nasibu

Grafu zinazozalishwa kwa kanuni ya nasibu, nodi kwa nodi au kingo kwa kingo, ili kuona ni sifa zipi, kama muunganisho au ukusanyiko, hujitokeza kwa kawaida.

Swali linalojibiwa: Mtandao 'wa kawaida' unaonekanaje chini ya kanuni hii ya kuongeza nodi na kingo?

Inaacha nje: Mitandao ya ulimwengu halisi mara chache huwa safi kama kanuni inayozalisha modeli.

Huendeshwa kwenye: takriban 1010 FLOPS takriban huendeshwa kwenye kompyuta ya mezani kwa grafu hadi mamilioni ya nodiTangu: 1959 Modeli ya grafu nasibu ya Erdos na Renyi

Monte CarloModeli za mitandaokiwango cha chini: Kanuni

Uigaji wa upenyezaji

Kimiani au mtandao wenye maeneo au viungo vinavyofunguliwa kwa nasibu, ukitazamwa hadi pale njia iliyounganika inapovuka mfumo mzima ghafla.

Swali linalojibiwa: Kwa msongamano gani mtandao nasibu huunganika ghafla kutoka mwisho hadi mwisho?

Inaacha nje: Vimiani vya kimawazo hutenda kwa usafi zaidi kuliko nyenzo yoyote halisi yenye vinyweleo au mtandao.

Huendeshwa kwenye: takriban 1010 FLOPS takriban kompyuta ya mezani kwa upekuzi mkubwa wa kimianiTangu: 1957 Kuanzishwa kwa nadharia ya upenyaji na Broadbent na Hammersley

Monte CarloOtomata za selikiwango cha chini: Kanuni

Makadirio ya konstanti kwa Monte Carlo

Uchukuaji sampuli nasibu hutumika kukadiria konstanti ya kihisabati au kiintegrali, kama kutawanya nukta kukadiria eneo, kama zoezi badala ya modeli ya kimwili.

Swali linalojibiwa: Uchukuaji wa sampuli nasibu kwa upofu pekee unaweza kubainisha thamani kamili ya kihisabati kwa usahihi kiasi gani?

Inaacha nje: Hukaribia polepole zaidi kuliko karibu mbinu yoyote ya hali ya juu zaidi ya namba.

Huendeshwa kwenye: takriban 109 FLOPS takriban huendeshwa kwenye kompyuta mpakato kwa sekunde hadi dakikaTangu: 1946 Wazo la Ulam la 1946; von Neumann alipendekeza toleo la kompyuta ya kielektroniki Machi 1947, na mbinu ilichapishwa kwa mara ya kwanza mwaka 1949 chanzoKatika mti wa uigaji: Mbinu ya Monte Carlo

Endesha modeli shirikishi

Monte Carlokiwango cha chini: Kanuni

Utafutaji wa nadharia ya namba wa kikokotozi

Nambari kubwa zinazojaribiwa kama tasa, kuvunjwa vipengele, au kutafutwa sifa maalum kama nambari kamili, kwa algoriti zinazoendeshwa kwa kiwango kikubwa badala ya kwa mkono.

Swali linalojibiwa: Je, namba hii kubwa ina sifa tunayotafuta, na utafutaji unaweza kusukuma rekodi mbali kiasi gani?

Inaacha nje: Utafutaji wa kuvunja rekodi husema kidogo kuhusu nambari ambazo hakuna aliyefikiria kuzikagua bado.

Huendeshwa kwenye: takriban 1013 FLOPS takriban mradi wa ukokotoaji wa kujitolea uliosambazwa kupitia mashine nyingi zilizotolewa kwa hiariTangu: 1951 Jaribio la mkono la Lucas la nambari tasa za Mersenne, lililoendeshwa na kompyuta mara ya kwanza mwaka 1951

Kanuni na haliMonte Carlokiwango cha chini: Kanuni

Namba za kivutio cha mchafuko

Seti ndogo ya milinganyo isiyo ya mstari inayokokotolewa hatua kwa hatua kufichua utegemezi nyeti wa hali za mwanzo na kivutio cha fraktali.

Swali linalojibiwa: Kwa nini mfumo rahisi wa kidetaministiki huwa usiotabirika?

Inaacha nje: Kukata tarakimu za nambari humaanisha njia ndefu si obiti ya kweli, bali tu ile inayokaa karibu na moja.

Huendeshwa kwenye: takriban 103 FLOPS takriban milinganyo michache, sekunde kwenye kompyuta mpakato.Tangu: 1963 Mtiririko wa kidetaministiki usio wa kipindi wa Lorenz, modeli ya mzunguko wa joto iliyoendeshwa kwenye kompyuta. chanzoKatika mti wa uigaji: Mzunguko wa joto wa kimachafuko wa Lorenz

Milinganyo diferensialikiwango cha chini: Kanuni

Majaribio ya kimiani yasiyo ya mstari

Mnyororo wa mizigo yenye chemchemi zisizo za mstari ulioanzishwa katika hali moja na kufuatiliwa kuona kama nishati husambaa sawasawa, kama thermodynamiki ingependekeza.

Swali linalojibiwa: Je, mnyororo usio wa mstari hugawana nishati yake sawasawa kati ya mienendo yake yote?

Inaacha nje: Matokeo hutegemea mnyororo uliochaguliwa na hali ya awali.

Huendeshwa kwenye: takriban 103 FLOPS takriban ndogo kwa viwango vya kisasa; ya awali ilitumia misa makumi kadhaa tu.Tangu: 1955 Tafiti za Fermi, Pasta na Ulam za matatizo yasiyo ya mstari kwenye kompyuta ya awali ya kidijitali. chanzo

Majaribio ya kinumeri ya soliton

Mlinganyo wa wimbi usio wa mstari unaotatuliwa kwenye gridi kutazama mipigo ikipita kila mmoja na kuhifadhi umbo lake, jambo ambalo mawimbi ya mstari hayafanyi.

Swali linalojibiwa: Kwa nini baadhi ya mawimbi yasiyo ya mstari hupitana bila kubadilika?

Inaacha nje: Inaonyesha familia moja ya milinganyo, si tabia ya jumla ya mawimbi yasiyo ya mstari.

Huendeshwa kwenye: takriban 104 FLOPS takriban gridi ya kipimo kimoja, rahisi leo.Tangu: 1965 Mwingiliano wa solitoni katika plasma isiyo na mgongano na kujirudia kwa hali za awali wa Zabusky na Kruskal. chanzo

Uchoraji wa seti za fraktali

Fomula rahisi inayojirudia inayojaribiwa kila mahali kwenye ndege changamano kuona kama inatoroka, ikichora mpaka wa seti ya nukta thabiti.

Swali linalojibiwa: Umbo la seti ambapo urudiaji rahisi unabaki umefungwa ni lipi?

Inaacha nje: Majaribio ya kutoroka hupendekeza uanachama tu, na picha ni sampuli ya azimio lenye kikomo ya seti yenye undani usio na mwisho.

Huendeshwa kwenye: takriban 109 FLOPS takriban kukuza kwa kina kunahitaji kurudia kwa usahihi uliopanuliwa katika mamilioni ya pointi.Tangu: 1980 Mandelbrot, vipengele vya fraktali vya kurudia z kuwa lambda z(1-z), picha za kwanza za kompyuta za seti ya Mandelbrot. chanzo

Milinganyo diferensialikiwango cha chini: Kanuni

Hali muhimu ya kujipanga yenyewe ya rundo la mchanga

Chembe zinazodondoshwa kwenye gridi na kuporomoka zinapokuwa na mteremko mkali mno, zikitoa maporomoko ya kila ukubwa bila marekebisho, kama modeli ya jinsi mifumo inavyofikia hali ya kiwango muhimu.

Swali linalojibiwa: Kwa nini maporomoko ya kila ukubwa huonekana bila marekebisho yoyote?

Inaacha nje: Kama mifumo halisi inafuata mizani ileile ya ukuaji hubishaniwa.

Huendeshwa kwenye: takriban 109 FLOPS takriban miendo mirefu kwenye gridi kubwa kuona jinsi matokeo yanavyopanuka kadiri ukubwa unavyoongezeka.Tangu: 1987 Hali ya kiwango muhimu inayojipanga yenyewe ya Bak, Tang na Wiesenfeld: maelezo ya kelele ya 1/f. chanzo

Otomata za seliMichakato ya kinasibukiwango cha chini: Kanuni

Ukokotoaji wa sifuri za zeta ya Riemann

Thamani za kitendakazi cha zeta kando ya mstari wake muhimu hukokotolewa kupata na kuhesabu sifuri zake, kuthibitisha kuwa ziko pale dhana inaposema.

Swali linalojibiwa: Je, sifuri zote zisizo rahisi (non-trivial) za kitendakazi cha zeta ziko kwenye mstari mmoja?

Inaacha nje: Ukaguzi wenye kikomo, hata uwe mrefu kiasi gani, hauwezi kuthibitisha kuwa hakuna sifuri nje ya mstari zaidi ya hapo.

Huendeshwa kwenye: takriban 1018 FLOPS takriban miongo ya muda wa CPU katika utafutaji mkubwa zaidi.Tangu: 1953 Hesabu za Turing za kitendakazi cha zeta cha Riemann. chanzo

Tarakimu za pi kwa kompyuta

Mfululizo wa pi hujumlishwa hadi idadi kubwa ya tarakimu kwa hesabu kamili, kujaribu nambari na mashine.

Swali linalojibiwa: Je, tarakimu za pi zinaonekana nasibu, na mashine inaweza kuaminiwa kwa kiwango hiki?

Inaacha nje: Tarakimu hazijibu swali lolote lililo wazi, na ukaguzi hukamata makosa ya vifaa tu kama mbinu ni huru.

Huendeshwa kwenye: takriban 1017 FLOPS takriban miezi kwenye seva kwa mamia ya trilioni za tarakimu.Tangu: 1950 Ubainishaji wa ENIAC wa Reitwiesner wa pi na e hadi zaidi ya nafasi 2000 za desimali (ulichapishwa 1950, ulichapishwa tena katika Pi: A Source Book). chanzo

Ugunduzi wa dhana unaoongozwa na AI

Kujifunza kwa mashine kwenye majedwali makubwa ya vitu vya kihisabati hupata ni sifa zipi zinahusiana, kupendekeza dhana ambayo wanahisabati hujaribu kuithibitisha.

Swali linalojibiwa: Uhusiano gani usioonekana kati ya kiasi hiki cha hisabati unastahili kuthibitishwa?

Inaacha nje: Inapendekeza mifumo tu na haithibitishi chochote yenyewe, na baadhi ya mpangilio katika data unaweza kuwa makosa ya jinsi data zilivyotengenezwa.

Huendeshwa kwenye: takriban 1015 FLOPS takriban siku kwenye GPU chache kwa kila seti ya data.Tangu: 2021 Davies na wenzake: kuendeleza hisabati kwa kuongoza silika ya binadamu kwa AI. chanzo

Viigaji vilivyojifunzakiwango cha chini: Kanuni

Utafutaji wa algoriti na miundo uliojifunza

Mfumo wa kucheza michezo au wa modeli ya lugha hutafuta taratibu mpya au vitu vya hisabati, huku kompyuta ikikagua usahihi wa kila mteule.

Swali linalojibiwa: Je, programu inaweza kugundua algoriti ya haraka zaidi au mfano mkubwa zaidi kuliko watu walivyopata?

Inaacha nje: Kila matokeo ni mfano mmoja mpya, na utafutaji unafunika aina za vitu tu ambazo wabunifu wake waliviunda kama mchezo.

Huendeshwa kwenye: takriban 1017 FLOPS takriban siku hadi wiki kwenye makundi ya viharakishi.Tangu: 2022 AlphaTensor ya Fawzi na wenzake, ikigundua algoriti za haraka za kuzidisha matriksi kwa kujifunza kwa kuimarisha. chanzo

Viigaji vilivyojifunzaKimageuzikiwango cha chini: Kanuni

Uthibitisho, mantiki na usalama

Ukaguzi wa modeli

Kila hali inayoweza kufikiwa ya mfumo wenye kikomo, kama itifaki au muundo wa saketi, ikihesabiwa na kompyuta kukagua kwamba sifa inashikilia katika zote.

Swali linalojibiwa: Je, kuna hali yoyote inayofikika ambapo muundo huu unavunja kanuni zake wenyewe?

Inaacha nje: Nafasi za hali hulipuka kupita kinachoweza kukaguliwa, kwa hiyo miundo halisi hurahisishwa kwanza.

Huendeshwa kwenye: takriban 1012 FLOPS takriban kundi la kompyuta la chuo kikuu linalopitia kikamilifu nafasi kubwa lakini yenye kikomo ya haliTangu: 1981 Kuanzishwa kwa ukaguzi wa modeli na Clarke na Emerson

Kanuni na halikiwango cha chini: Kanuni

Utafutaji wa kiotomatiki wa uthibitisho wa nadharia

Utafutaji kupitia misururu ya makisio ya kimantiki, unaozalishwa na kompyuta hatua kwa hatua, kutafuta uthibitisho au ukanushaji wa kauli ya hisabati.

Swali linalojibiwa: Je, mfuatano halali wa hatua za kimantiki upo kutoka kanuni za msingi hadi kauli hii?

Inaacha nje: Hupata uthibitisho ambao binadamu hangechagua, na wakati mwingine hakuna hata mmoja unaoweza kufikiwa.

Huendeshwa kwenye: takriban 1011 FLOPS takriban kundi la kompyuta la chuo kikuu linalotafuta kwa saa hadi sikuTangu: 1956 Logic Theorist, programu ya mapema ya kutafuta uthibitisho kiotomatiki

Kanuni na haliMonte Carlokiwango cha chini: Kanuni

SAT na kutatua vikwazo

Mamilioni ya mchanganyiko wa thamani za kweli au uongo yakitafutwa kwa utaratibu ili kutimiza seti kubwa ya vikwazo vya kimantiki, hutumika kupanga ratiba, njia au kuthibitisha miundo.

Swali linalojibiwa: Je, kuna mgawo wowote wa thamani unaotimiza vikwazo hivi vyote kwa wakati mmoja?

Inaacha nje: Baadhi ya visa ni vigumu kiasi kwamba hakuna kitatuzi, hata kiwe bora kiasi gani, kinachomaliza kwa wakati.

Huendeshwa kwenye: takriban 1011 FLOPS takriban kituo cha kazi hadi kundi la kompyuta, kulingana na ukubwa wa tatizoTangu: 1962 utaratibu wa Davis-Putnam wa kutafuta kutosheleka

Kanuni na haliMonte Carlokiwango cha chini: Kanuni

Uundaji wa modeli ya mashambulizi ya kriptografia

Mpango wa msimbo au ubadilishanaji wa funguo unaoshambuliwa mamilioni ya mara katika uigaji, kwa nguvu ghafi, upendeleo wa kitakwimu au udhaifu uliobuniwa, ili kupima juhudi halisi za kuuvunja.

Swali linalojibiwa: Ingechukua operesheni ngapi kuvunja hili kweli, na je, nambari hiyo bado ni kubwa kwa usalama?

Inaacha nje: Hujaribu tu mashambulizi ambayo mchambuzi alifikiria kuyaiga, si lile ambalo hakuna aliyelipata bado.

Huendeshwa kwenye: takriban 1014 FLOPS takriban kundi lililosambazwa la mashine nyingi zinazoendesha majaribio ya mashambuliziTangu: 1976 kufikia 1976, uchambuzi wa kompyuta wa nguvu ya misimbo na ubadilishanaji wa funguo

Monte CarloKanuni na halikiwango cha chini: Kanuni

Uigaji wa uvujaji wa njia ya pembeni

Matumizi ya nguvu, wakati au utoaji wa sumakuumeme wa kifaa kinapoendesha operesheni ya usimbaji fiche, ili kuona ni nini msikilizaji wa nje anaweza kujifunza kutoka kwake.

Swali linalojibiwa: Kiasi gani cha ufunguo wa siri hutoka kupitia tabia ya kimwili ya kifaa, si hisabati?

Inaacha nje: Hali za maabara hunasa ishara safi zaidi kuliko kifaa halisi chenye kelele kwa kawaida hufichua.

Huendeshwa kwenye: takriban 1010 FLOPS takriban kituo cha kazi kinachoiga rekodi ya matumizi ya nguvu au ya muda ya kifaa kimojaTangu: 1996 Onyesho la Kocher la mashambulizi ya muda dhidi ya utekelezaji wa usimbaji fiche

Milinganyo diferensialiMonte Carlokiwango cha chini: Kanuni

Uthibitishaji wa itifaki za usalama

Kila ujumbe ambao mshambuliaji angeweza kutuma, kurudia au kughushi katika itifaki ya mawasiliano, ukihesabiwa na kompyuta kukagua kama siri au utambulisho unaweza kulazimishwa kutoka kwake.

Swali linalojibiwa: Je, mfuatano wowote wa ujumbe unaweza kuhadaa itifaki hii kuvujisha siri au kukubali utambulisho bandia?

Inaacha nje: Huthibitisha itifaki kama ilivyobainishwa, si njia za mkato ambazo utekelezaji halisi huchukua.

Huendeshwa kwenye: takriban 1011 FLOPS takriban kituo cha kazi hadi kundi la kompyuta linalokagua nafasi ya ujumbe ya itifaki mojaTangu: 1989 kielelezo cha Dolev-Yao, msingi wa uthibitishaji wa itifaki

Kanuni na haliModeli za mitandaokiwango cha chini: Kanuni

Uthibitisho unaosaidiwa na kompyuta kwa kukagua kila kisa

Nadharia iliyopunguzwa hadi orodha yenye kikomo ya visa, kila kimoja kikithibitishwa na programu, kwa sababu hakuna binadamu angeweza kuvikagua vyote.

Swali linalojibiwa: Je, uthibitisho unaweza kukamilishwa na mashine inayokagua kila kisa?

Inaacha nje: Uaminifu huhamia kwenye programu, vifaa na hoja ya kupunguza visa.

Huendeshwa kwenye: takriban 109 FLOPS takriban takriban saa elfu moja kwenye mainfremu kwa ya asili; chini zaidi sasa.Tangu: 1977 Uthibitisho wa Appel na Haken kwamba kila ramani tambarare inaweza kupakwa rangi nne, kwa kutumia upunguzi uliokaguliwa na kompyuta. chanzo

Kanuni na haliMilinganyo diferensialikiwango cha chini: Kanuni

Hesabu zilizothibitishwa

Hesabu zinazofanywa kwa mipaka ya uhakika, hivyo matokeo ya namba yanathibitisha kauli ya hisabati, kama kuwepo kwa kivutio cha mchafuko.

Swali linalojibiwa: Je, jibu lililokokotolewa linaweza kuthibitishwa kuwa sahihi, si tu sahihi kwa uwezekano?

Inaacha nje: Mipaka inaweza kulipuka kwa muda mrefu, ikizuia uthibitisho kwa matatizo mafupi au yenye tabia nzuri.

Huendeshwa kwenye: takriban 109 FLOPS takriban hesabu ya vipindi huzidisha gharama kwa kigezo cha wastani.Tangu: 2002 Kitatuzi madhubuti cha ODE cha Tucker na tatizo la 14 la Smale, kuthibitisha kwamba kivutio cha Lorenz kipo. chanzo

Milinganyo diferensialikiwango cha chini: Kanuni

Uorodheshaji wa mashine za Turing

Kila programu ndogo ya mashine ndogo kabisa ikiendeshwa kuona ipi inakoma na ipi inaendelea milele, kupata ile inayokoma iliyoendeshwa muda mrefu zaidi ya kila ukubwa.

Swali linalojibiwa: Programu ndogo sana inaweza kuendeshwa kwa muda gani kabla haijasimama?

Inaacha nje: Kutoweza kuamuliwa kunamaanisha mashine fulani haziwezi kamwe kuainishwa, haijalishi zinaendeshwa kwa muda gani.

Huendeshwa kwenye: takriban 1015 FLOPS takriban mabilioni ya mashine, pamoja na uthibitisho kwa zile ambazo hazikomi.Tangu: 1965 Tafiti za kompyuta za Lin na Rado kuhusu matatizo ya mashine za Turing. chanzo

Kanuni na haliMilinganyo diferensialikiwango cha chini: Kanuni

Ukaguzi wa kielelezo wa kitakwimu

Mfumo wenye tabia nasibu unaoigwa mara nyingi kukadiria kwa uhakika wa kitakwimu uwezekano wa kukiuka sifa.

Swali linalojibiwa: Mfumo wa nasibu una uwezekano gani wa kuvunja kanuni ya usalama?

Inaacha nje: Uendeshaji wa kitakwimu hutoa uwezekano wenye kiwango cha uhakika, si uthibitisho, na hitilafu adimu zinahitaji uchukuaji sampuli wa umuhimu.

Huendeshwa kwenye: takriban 109 FLOPS takriban maelfu hadi mamilioni ya utekelezaji uliochukuliwa sampuli.Tangu: 2002 Uthibitishaji wa uwezekano wa mifumo ya matukio diskreti wa Younes na Simmons kwa kutumia uchukuaji sampuli wa kukubali. chanzo

Monte CarloMichakato ya kinasibukiwango cha chini: Kanuni

Upimaji wa fuzz

Programu hulishwa idadi kubwa ya pembejeo nasibu au zilizobadilishwa kupata zile zinazoifanya ianguke, kwa kweli ikiiga ulimwengu wenye uadui au uzembe.

Swali linalojibiwa: Ingizo gani litafanya programu hii ishindwe?

Inaacha nje: Hupata tu hitilafu ambazo pembejeo za nasibu hufikia, na programu inaweza kupita kwa miaka huku ikificha mdudu nyuma ya kisa adimu.

Huendeshwa kwenye: takriban 1014 FLOPS takriban miaka-mashine ya muda wa CPU kwa msimbo mkubwa.Tangu: 1990 Utafiti wa kimajaribio wa Miller, Fredriksen na So wa uaminifu wa zana za UNIX. chanzo

Utekelezaji wa kialama

Programu huendeshwa na pembejeo zisizojulikana zilizoandikwa kama alama, ikikusanya masharti ya kila njia, kisha kitatuzi hupata thamani zinazochukua kila tawi.

Swali linalojibiwa: Ingizo gani huendesha kila njia ya programu hii, na je, yoyote hufikia hitilafu?

Inaacha nje: Idadi ya njia hukua kwa kipeo kadiri programu inavyokua, hivyo kubwa hufunikwa kwa sehemu tu.

Huendeshwa kwenye: takriban 1012 FLOPS takriban saa za muda wa kitatuzi kwa kila programu, zikiongezeka kwa kasi kadiri idadi ya njia inavyoongezeka.Tangu: 1976 Utekelezaji wa kialama na majaribio ya programu ya King. chanzo

Kanuni na haliKanuni za kwanzakiwango cha chini: Kanuni

Ufasiri wa kidhahania

Programu huendeshwa kwa seti za thamani zinazowezekana, kama masafa, badala ya thamani moja moja, kuthibitisha sifa zinazoshikilia kwa kila pembejeo.

Swali linalojibiwa: Je, programu hii inaweza kugawanya kwa sifuri au kuzidi kikomo, kwa pembejeo yoyote?

Inaacha nje: Makadirio salama huleta tahadhari za uongo, kwa hiyo watu bado lazima wakague kila onyo.

Huendeshwa kwenye: takriban 1011 FLOPS takriban saa kwenye kituo cha kazi kwa msimbo mkubwa wa avioniki.Tangu: 1977 Ufasiri wa kidhahania wa Cousot na Cousot, modeli ya kimiani iliyounganishwa ya uchambuzi tuli wa programu. chanzo

Kanuni na haliKanuni za kwanzakiwango cha chini: Kanuni

Ukaguzi wa modeli wenye mipaka

Tabia ya muundo hadi idadi isiyobadilika ya hatua huandikwa kama fomula ya mantiki na kukabidhiwa kitatuzi cha kutosheleka ili kupata njia yoyote fupi hadi hitilafu.

Swali linalojibiwa: Je, saketi au programu hii inaweza kufikia hali ya kosa ndani ya idadi fulani ya hatua?

Inaacha nje: Haithibitishi chochote zaidi ya kikomo cha hatua isipokuwa hoja nyingine ionyeshe kuwa kinatosha.

Huendeshwa kwenye: takriban 1013 FLOPS takriban saa kwenye seva kwa kila mali.Tangu: 1999 Ukaguzi wa modeli ya ishara wa Biere, Cimatti, Clarke na Zhu bila BDD. chanzo

Kanuni na haliKanuni za kwanzakiwango cha chini: Kanuni

Majaribio ya nasibu yanayotegemea sifa

Kanuni inayopaswa kushikilia daima hutajwa, na kompyuta huzalisha visa vingi nasibu na kupunguza kila kushindwa hadi mfano mdogo wa kupinga.

Swali linalojibiwa: Je, msimbo huu unatii maelezo yake yenyewe kwa pembejeo pana?

Inaacha nje: Visa vya nasibu huenda visifikie kamwe hali adimu, na sifa iliyoandikwa inaweza isiwe ile muhimu.

Huendeshwa kwenye: takriban 109 FLOPS takriban dakika kwenye kompyuta mpakato kwa maelfu ya visa.Tangu: 2000 QuickCheck ya Claessen na Hughes, zana nyepesi ya kupima nasibu ya programu za Haskell. chanzo

Monte CarloKanuni na halikiwango cha chini: Kanuni

Uthibitishaji wa mtandao wa neva

Vitatuzi vya vikwazo huthibitisha kwamba kwa kila pembejeo katika eneo, matokeo ya mtandao wa neva hubaki ndani ya mipaka, badala ya kujaribu sampuli.

Swali linalojibiwa: Je, badiliko dogo la pembejeo linaweza kuufanya mtandao utoe jibu lisilo sahihi?

Inaacha nje: Uthibitisho hufanya kazi tu kwa mitandao midogo, na seti ya usumbufu unaoweza kukaguliwa ni finyu.

Huendeshwa kwenye: takriban 1013 FLOPS takriban saa hadi siku kwenye seva kwa mtandao mdogo.Tangu: 2017 Reluplex ya Katz na wenzake, kitatuzi cha SMT cha kuthibitisha mitandao ya neva ya kina. chanzo

Kanuni na haliKanuni za kwanzakiwango cha chini: Kanuni

Mifumo na mashine

Uigaji wa usanifu wa kompyuta

Mkondo wa hatua za uchakataji (pipeline), kumbukumbu fiche na kitabiri cha matawi cha kichakataji kilichopendekezwa huigwa amri kwa amri, ili kukadiria kasi ya chipu kabla ya kujengwa.

Swali linalojibiwa: Muundo huu wa kichakata ungeendesha programu halisi kwa kasi gani, kabla silikoni yoyote haijakatwa?

Inaacha nje: Hurahisisha vya kutosha chipu halisi hivi kwamba silikoni ya mwisho daima hutofautiana kidogo na modeli.

Huendeshwa kwenye: takriban 1011 FLOPS takriban kundi la kompyuta la chuo kikuu linaloendesha programu za kupima kupitia modeliTangu: 1990 kufikia 1990, viigaji vya kichakataji vinavyofuata kila mzunguko wa saa kwa usahihi kwa utafiti wa usanifu

Tukio diskretiKanuni na halikiwango cha chini: Kanuni

Uigaji wa mifumo iliyosambazwa na makubaliano

Kompyuta nyingi zikiigwa zikitumiana ujumbe kwa ucheleweshaji, kupotea na kushindwa, kujaribu kama algoriti iliyosambazwa bado inakubaliana juu ya jibu sahihi.

Swali linalojibiwa: Je, algoriti hii bado hufikia makubaliano sahihi ujumbe unapopotea, kuchelewa au nodi kuanguka?

Inaacha nje: Hitilafu zinazodungwa ni zile alizotarajia mbunifu, si zile zinazojitokeza bila kutarajiwa katika matumizi halisi.

Huendeshwa kwenye: takriban 1010 FLOPS takriban kundi la kompyuta linaloiga mamia ya nodi pepeTangu: 1978 Kazi ya mapema ya Lamport kuhusu mpangilio na kushindwa katika mifumo iliyosambazwa

Tukio diskretiModeli za mitandaokiwango cha chini: Kanuni

Uigaji wa mifumo ya hifadhi

Diski, hifadhi na mifumo ya faili ikiigwa kuhusu jinsi inavyopanga data, kushindwa na kupona, kujaribu muundo wa hifadhi kabla ya kununua na kujaza hifadhi halisi.

Swali linalojibiwa: Muundo huu wa hifadhi hufanyaje kazi na kuhimili kushindwa, kwa kiwango ambacho ni ghali mno kujaribu kwa kweli kwanza?

Inaacha nje: Diski halisi hushindwa kwa njia zenye fujo na zinazohusiana zaidi kuliko kiwango cha modeli cha kushindwa kwa nasibu.

Huendeshwa kwenye: takriban 1010 FLOPS takriban kituo cha kazi hadi kundi dogo la kompyuta linaloiga safu ya hifadhiTangu: 1988 kufikia 1988, modeli za uigaji za kuaminika kwa safu ya diski

Tukio diskretiMichakato ya kinasibukiwango cha chini: Kanuni

Uigaji wa kipanga ratiba cha mfumo endeshi

Mfululizo wa kazi za ukokotoaji unaoigwa ukifika na kushindania kichakataji, ukiendeshwa dhidi ya kanuni tofauti za upangaji ratiba kuona ipi ni ya haki au ya haraka zaidi.

Swali linalojibiwa: Njia gani ya kupanga foleni ya kazi hukamilisha kazi nyingi zaidi, au ni ya haki zaidi kwa kila kazi?

Inaacha nje: Mzigo wa kazi bandia mara chache hulingana na mchanganyiko usio na mpangilio wa kazi ambazo mashine halisi hukutana nazo.

Huendeshwa kwenye: takriban 109 FLOPS takriban huendeshwa kwenye kompyuta mpakato au kituo cha kazi kwa sekunde hadi dakikaTangu: 1968 kufikia 1968, tafiti za uigaji wa sera za upangaji ratiba ya kichakataji

Tukio diskretikiwango cha chini: Kanuni

Upimaji wa kimajaribio wa utendaji wa algoriti

Algoriti inayoendeshwa maelfu ya mara juu ya pembejeo zilizozalishwa nasibu au halisi za ukubwa unaoongezeka, ikipima jinsi muda wake wa kuendesha unavyokua kwa kweli badala ya kuthibitisha kwenye karatasi.

Swali linalojibiwa: Muda wa kuendesha wa algoriti hii hukua vipi kiuhalisia, kwenye pembejeo zitakazotumika kweli?

Inaacha nje: Hali mbaya kabisa isiyokuwemo kwenye pembejeo za majaribio hubaki bila kugunduliwa hadi itokee.

Huendeshwa kwenye: takriban 109 FLOPS takriban huendeshwa kwenye kituo cha kazi kwa pembejeo nyingi za majaribio zilizozalishwaTangu: 1970 kufikia 1970, majaribio ya kiuzoefu yenye mpangilio ya muda wa kuendesha wa algoriti

Monte CarloMichakato ya kinasibukiwango cha chini: Kanuni

Utekelezaji wa programu kwa modeli za lugha

Modeli ya lugha huandika hatua za kati moja baada ya nyingine inapofuatilia kile programu ingekokotoa.

Swali linalojibiwa: Je, modeli ya lugha inaweza kuiga kuendesha msimbo?

Inaacha nje: Matokeo hayahakikishiwi kuwa sahihi, na programu ndefu hushindwa.

Huendeshwa kwenye: takriban 1014 FLOPS takriban Makisio kwa kila swaliTangu: 2021 Show your work: scratchpads for intermediate computation with language models (2021) chanzo

Viigaji vilivyojifunzakiwango cha chini: Kanuni

Uigaji wa makubaliano ya mnyororo wa vitalu

Mtandao wa nodi zinazozalisha na kushiriki vitalu chini ya ucheleweshaji, kujaribu jinsi ukubwa wa kitalu, muda na washambuliaji vinavyoathiri usalama na upitishaji.

Swali linalojibiwa: Blockchain ni salama na ya haraka kiasi gani chini ya ucheleweshaji wa mtandao na mashambulizi?

Inaacha nje: Tabia halisi ya nodi na mpangilio wa mitandao hupimwa kwa sehemu tu.

Huendeshwa kwenye: takriban 108 FLOPS takriban uendeshaji wa maelfu ya nodi unaoongozwa na matukio.Tangu: 2016 Uchambuzi wa usalama na utendaji wa Gervais na wenzake wa mnyororo wa vitalu wa uthibitisho-wa-kazi kwa kiigaji. chanzo

Tukio diskretiKutegemea mawakalaModeli za mitandaokiwango cha chini: Idadi za viumbe

Uigaji wa matukio diskreti sambamba

Uigaji wa matukio kwa wakati hugawanywa kwenye vichakataji vingi ambavyo kila kimoja huendeleza saa yake na kurudi nyuma ikiwa kimoja kimechelewa kufika.

Swali linalojibiwa: Uigaji mkubwa unaoendeshwa na matukio, kama mtandao au uwanja wa vita, unawezaje kuendeshwa haraka kwenye mashine nyingi?

Inaacha nje: Kurudishwa nyuma kunaweza kuenea mfululizo, na kuongezeka kwa kasi hutegemea sana jinsi matukio yalivyofungamana kwa karibu.

Huendeshwa kwenye: takriban 1014 FLOPS takriban saa kwenye kompyuta kuu kwa mabilioni ya matukio.Tangu: 1985 Muda pepe wa Jefferson, utaratibu wa Time Warp wa usawazishaji wa kimatumaini. chanzo

Tukio diskretikiwango cha chini: Kanuni

Uigaji wa usanifu wa kichakata picha

Viini, warp na kumbukumbu za kichakataji cha picha huigwa mzunguko kwa mzunguko, zikiendesha programu halisi kutathmini muundo kabla ya kujenga.

Swali linalojibiwa: Mabadiliko ya muundo yangeathirije kasi ya programu sambamba kwenye chipu ya picha?

Inaacha nje: Maelezo ya chipu halisi ni siri au hayajulikani, kwa hivyo modeli inalingana na namba za miundo iliyopo kwa makadirio tu.

Huendeshwa kwenye: takriban 1012 FLOPS takriban saa hadi siku za muda wa mwenyeji kwa kila sekunde ya utekelezaji ulioigwa.Tangu: 2009 Uchambuzi wa Bakhoda na wenzake wa mizigo ya CUDA kwa kutumia kiigaji cha kina cha GPU. chanzo

Tukio diskretiKanuni na halikiwango cha chini: Kanuni

Uigaji wa mfumo ulioharakishwa na FPGA

Muundo wa chipu hupakiwa kwenye saketi nyingi zinazoweza kupangwa upya zinazouendesha mzunguko kwa mzunguko kwa kasi ya megahertz, zikiiga seva nzima na mitandao yake.

Swali linalojibiwa: Kichakata hiki na kundi lake vitafanyaje kazi vikiendesha programu halisi, kabla hakijatengenezwa?

Inaacha nje: Ni polepole zaidi kuliko chipu halisi, na muundo usiotoshea kwenye saketi hauwezi kuendeshwa.

Huendeshwa kwenye: takriban 1015 FLOPS takriban siku kwenye wingu la mamia ya saketi zinazoweza kupangwa upya.Tangu: 2018 FireSim ya Karandikar na wenzake, uigaji wa mifumo ya kiwango kikubwa unaoharakishwa na FPGA, sahihi hadi mzunguko, kwenye wingu la umma. chanzo

Uigaji wa mfumo mzima

Kompyuta nzima, yenye vichakataji, kumbukumbu, diski na kadi za mtandao, huigwa vizuri vya kutosha kuwasha mfumo wa uendeshaji usiobadilishwa na kuendesha programu zake.

Swali linalojibiwa: Programu halisi hutendaje kwenye mashine ambayo bado haipo, au inayoweza kusimamishwa na kuchezwa tena upendavyo?

Inaacha nje: Muda unakadiriwa ili kuongeza kasi, hivyo hauwezi kutoa utendaji kamili, tabia ya kiutendaji tu.

Huendeshwa kwenye: takriban 1011 FLOPS takriban karibu wakati halisi kwenye seva kwa kila mashine iliyoigwa.Tangu: 2002 Simics ya Magnusson na wenzake, jukwaa la uigaji wa mfumo mzima. chanzo

Uigaji mwepesi wa mtandao

Makumi au mamia ya wenyeji pepe na swichi huendesha programu halisi ya mtandao kwenye kompyuta mpakato moja, zikiunganishwa na nyaya zilizoigwa zenye kasi na ucheleweshaji uliowekwa.

Swali linalojibiwa: Je, programu hii ya kudhibiti mtandao itafanya kazi kwenye mpangilio mzima kabla ya kusambazwa?

Inaacha nje: Kichakataji cha mwenyeji hushirikiwa na nodi zote pepe, hivyo viungo vya haraka hupunguzwa kasi.

Huendeshwa kwenye: takriban 1010 FLOPS takriban wakati halisi kwenye kituo kimoja cha kazi.Tangu: 2010 'A network in a laptop' ya Lantz, Heller na McKeown, utengenezaji wa haraka wa mifano ya mitandao inayofafanuliwa na programu. chanzo

Kupoza kwa kuigwa (simulated annealing)

Kompyuta hupoza modeli ya atomu au muundo polepole, ikikubali mpangilio mbaya zaidi mara kwa mara, ili kupata suluhisho zuri la tatizo gumu la uboreshaji.

Swali linalojibiwa: Mpangilio au ratiba iliyo karibu na bora zaidi ni ipi kati ya uwezekano mwingi mno?

Inaacha nje: Haitoi hakikisho la jibu bora, na matokeo hutegemea ratiba ya kupoa.

Huendeshwa kwenye: takriban 1012 FLOPS takriban saa kwenye kituo cha kazi kwa uwekaji wa chipu.Tangu: 1983 Uboreshaji kwa kupoza kwa kuigwa wa Kirkpatrick, Gelatt na Vecchi. chanzo

Monte CarloMichakato ya kinasibukiwango cha chini: Kanuni

Ukokotoaji wa kadirio wa Bayesian

Kiigaji huendeshwa kwa thamani nyingi za vigezo vya majaribio, na zile zinazotoa data karibu na data zilizoonekana huhifadhiwa, zikitoa picha ya thamani zipi zinazowezekana.

Swali linalojibiwa: Mipangilio gani ya kielelezo changamano ingeweza kuzalisha data tunayoona?

Inaacha nje: Matokeo hutegemea ni muhtasari gani wa data unaotumika na ulinganifu unapaswa kuwa wa karibu kiasi gani ili kuhesabiwa.

Huendeshwa kwenye: takriban 1013 FLOPS takriban mamilioni ya miendo ya kiigaji kwenye kundi la kompyuta.Tangu: 1997 Ukisiaji wa Tavaré na wenzake wa nyakati za muungano kutoka data ya mfuatano wa DNA kwa kutumia uigaji. chanzo

Monte CarloMichakato ya kinasibukiwango cha chini: Kanuni