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.
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
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
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
Utafutaji wa hisabati ya majaribio
Utafutaji wa nguvu ghafi wa namba kupata mifumo, mifano ya kupinga au uhusiano kamili kati ya namba, unaoendeshwa mbali zaidi ya kinachoweza kukaguliwa kwa mkono.
Swali linalojibiwa: Je, dhana hii ni kweli kwa kila kisa ambacho mtu anaweza kumudu kukagua, na je, mfumo hujitokeza?
Inaacha nje: Hakuna kiasi cha visa vilivyokaguliwa ambacho ni uthibitisho, hata vikiwa vingi kiasi gani vinavyothibitika.
Huendeshwa kwenye: takriban 1011 FLOPS takriban kundi la kompyuta la chuo kikuu linaloendesha kwa siku kadhaa kwa utafutaji mmojaTangu: 1963 kufikia 1963, utafutaji wa kompyuta wa mahusiano ya namba kamili na mifumo ya namba tasa
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Utafutaji wa uboreshaji wa kikusanyaji na programu
Idadi kubwa ya tofauti ndogo za kipande cha msimbo hujaribiwa na kupimwa, kutafuta toleo la haraka au fupi zaidi linalofanya kazi ile ile.
Swali linalojibiwa: Kati ya njia zote sawa za kuandika kipande hiki kidogo cha msimbo, ipi ndiyo ya haraka zaidi kweli?
Inaacha nje: Programu zilizopatikana wakati mwingine ni za ajabu kiasi kwamba hakuna maelezo ya kwa nini zinafanya kazi.
Huendeshwa kwenye: takriban 1010 FLOPS takriban kundi la kompyuta linalotafuta katika nafasi kubwa ya matoleo ya msimboTangu: 2006 kufikia 2006, utafutaji wa uboreshaji-mkuu juu ya mfuatano mfupi wa amri
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
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
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
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
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
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
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