Loading...
Series: Tsitreɖoɖo Ƒomevi Ɖaseɖigbalɛ Ƒe Series · Akpa 1 le 3 me Ame siwo wòŋlɔ na: Ame siwo wɔ dzeɖoɖo gbãtɔ. Womedi mathematics, mɔ̃ɖaŋlɔ̃ alo cryptography ƒe nyanya ŋgɔ o. Nu si nàdzo kplee: Nyagɔme fɛfɛ si ana nàse nyuie nu si wònye be wòaɖo ɖase be software le nyuie, nu ka ta esia to vovo tso dodokpɔ tso gɔme, nu si nye machine-checked ɖaseɖigbalɛ, kple teƒe siwo dzi ɖase ma ate ŋu adzɔ ɖaa hã.
Woxɔ se na software geɖe elabena wodoe kpɔ: míetsɔe wɔ dɔ kple emenyawo geɖe eye míekpɔ ale si wɔa nu. Tsitreɖoɖo ƒomevi Ɖaseɖigbalɛ [Formal verification] bia biabia si sesẽ wu. Miate ŋu aɖo ɖase, kple mathematics ƒe kaɖedzi bliboa, be system a wɔ nu si wòle be wòawɔ na emenu siawo katã si ate ŋu anɔ anyi, hã esiwo ame aɖeke mebu be yeadɔ kpɔ o? Nuŋɔŋlɔ sia atu susu ma tso gɔmedzeƒe. Gɔmesese gbã, dzesi aɖeke va se ɖe esi woɖo ƒe xa.
Esia nye nya si dzɔ vavã, eye eyae nye ta si ta series sia li.
Le 2022 me, ɣaɣla-crypto ga Zcash ɖe gaƒuƒoƒo ɣaɣla yeye aɖe si woyɔ be Orchard kpe, si na ameawo wɔ asitsɔtsɔ kple gaƒe siwo woɣla. Ƒe ene megbe la, eƒe dɔ wɔ nyuie fũ, eye wodo professional audit geɖe kpɔe. Ke le May 2026 me la, dedienyawo ƒe nudzɔdzɔla aɖe si bu susu nyuie tso mathematics si le te la ŋu (kple kpekpeɖeŋu si tso AI dɔwɔnuwo gbɔ) kpɔ teƒe ɖeka si womeɖo nudzraɖoɖo de eme akpa blibo o le system a ƒe mathematics me. Teƒe ɖeka ma ate ŋu ana atacatɔ aɖe wɔ ga maɖiɖi si meɖoɖo aɖeke mele o, eye elabena woɣla gaƒeawo la, ame aɖeke mate ŋu akpɔe be edzɔ o. Vodada la nɔ afi ma le ɣeyiɣi bliboa me.
Womekpɔe to dodokpɔ me o. Dodokpɔ siawo katã va yi nyuie le ƒe ene me. Ame aɖe bu susu tso mathematics la ŋu he kpɔe. Eye esi team la trɔe la, womede patch de eme ko eye wodzo o. Woŋlɔ machine-checked mathematics ƒe ɖaseɖigbalɛ, si ƒe theorem 2,700 kple afɔ aɖe, be nusɔɔ yeye la mate ŋu anɔ vodada ƒomevi ma o.
Eyae nye tsitreɖoɖo ƒomevi ɖaseɖigbalɛ, eye esiae wòna wò: menye "mído dzesi geɖe kpɔ eye wowɔ dɔ" o, ke boŋ "míeɖo ɖase be ewɔ dɔ na dzesi siawo katã." Na system siwo me dzesi ɖeka si womekpɔ o ate ŋu ana gbegblẽ gã ava (ga, dzikpɔlawo, kɔkɔe dɔwɔnuwo, cryptography), vovototo sia nye nu katã.
Edsger Dijkstra, computer scientist, yɔ teƒe si dodokpɔ mete ŋu akpɔ o ƒe ŋkɔ xoxotɔ, eye eganye vavã va se egbe:
Dodokpɔ ate ŋu afi vodada ƒe nɔnɔ fia, ke wòmate ŋu afi woƒe manganɔnɔ fia gbeɖe o.
Ne dodokpɔ aɖe yi nyuie la, nèsrɔ be system la wɔ dɔ le emenu ma dzi. Mesrɔ naneke tso emenyawo siwo mèdo kpɔ o ŋu o, eye vodada vɔ̃wo le dzesi siwo ame aɖeke medo kpɔ o me zi geɖe.
Bu be wòe nye ame si kpɔa aƒe gã aɖe si ƒe agbo akpe le ŋu, eye wòƒe dɔe nye be nàɖo kpeɖeŋu be agbo siawo katã ƒo le zã me.
Vovototo le vavã ƒe kpɔkpɔ le akpa aɖe dzi kple ŋɔnɔ ƒe nɔnɔ aɖe ƒe ɖaseɖoɖo dome. Dodokpɔ ƒe akpa aɖewo koe wòkpɔa. Tsitreɖoɖo ƒomevi ɖaseɖigbalɛ ɖoa ɖase. Eyae nye susu bliboa, eye nu bubu siawo katã nye mɔnu siwo ana wòawɔe kple dzodzro nyuie.
Tsitreɖoɖo ƒomevi ɖaseɖigbalɛ siawo katã, togbɔ be eƒe sesẽ le aleke o, wotu wo tso nu etɔ pɛ me. Ɖe asi ɖe esiawo ŋu nyuie eye nu bubu la nye nyatakakadzraɖoɖo pɛ.
| Tikpɔtɔ | Gɔmesese bɔbɔe | Aƒetoto ƒe kpɔɖeŋu |
|---|---|---|
| Nudzraɖoɖo | Nya si me tsitotsito le le nu si "nyuie" gɔmee ŋu | "Agbo siawo katã le be woaƒo le zã me" |
| System | Nu vavã si wole kpɔm (mɔ̃ɖaŋlɔ̃, circuit, alo protocol) | Aƒe la kple eƒe agboƒoƒe mɔnu |
| Ɖaseɖigbalɛ | Ɖoɖo sesẽ si fia be system la dea nudzraɖoɖo la eme ɣesiaɣi | Ɖoɖo si me logic le, si fia be ne wozi "ƒo" la agbo siawo katã ƒoa |
Eye nu eneawo aɖe si meɖe gbe na o na nu bliboa xɔa nane:
Ɖaseɖigbalɛ ƒe kpeɖeŋu siwo ƒe ŋkɔ wòase la ƒe dometɔe nye Lean, Rocq (tsã be Coq), kple Isabelle. Wo nye logic-dodokpɔ ƒe engine siwo me tsitotsito le vevie. Zcash ƒe ɖaseɖigbalɛ si le míatɔgbi ƒe nya me la woŋlɔe le Lean me. Le esia ŋu la, wotsɔ AI model yeyeawo le ɣeyiɣi sia me kpekpeɖeŋu na wo be woaŋlɔ ɖaseɖigbalɛ siawo, eye amewo hea wo, si tsɔ dɔ si xɔa ƒe geɖe va zu kɔsiɖa aɖewo. Machine la hã doa afɔ ɖeka ɖeka katã kpɔ, eyata mɔaƒoƒo sia meɖea kaɖedzi aɖeke le eme o.
Nya "ɖaseɖigbalɛ" ate ŋu ana ame nakpɔ vɔvɔ̃, eyata míana wòagakpɔa eƒe ɣeɣe kple kpɔɖeŋu si wòate ŋu ado kpɔ. Cryptography aɖeke mele o, school arithmetic ko.
Nya si míeɖoa ɖase: Na whole number n siawo katã, ƒoƒo 0 + 1 + 2 + ... + n sɔ kple n(n+1)/2.
Àte ŋu ado esia kpɔ. n = 5 nana 0+1+2+3+4+5 = 15, eye 5 × 6 / 2 = 15. ✓ Esɔ. Do n = 10 hã kpɔ: ƒoƒo la nye 55, eye formula la nana 10 × 11 / 2 = 55. ✓ (Woxɔ wo ƒe nɔnɔ eye wodo ɖase na wo; nya la ɖoa anyi na n siawo katã tso 0 yi 999 me ne wodoe kpɔ tẽ.)
Ke dzesiwo dodokpɔ, togbɔ be wonye akpe, mate ŋu ayi "na whole number siawo katã" o. Woƒe xexlẽ mele nu o. Ɖaseɖigbalɛ ƒoa gap si menɔ gbegbe o ma le ɖoɖo ƒe ɣeyiɣi kpui aɖe me, kple mɔnu si woɣe dɔ be induction:
n = 0, ƒoƒo la nye 0 ko, eye formula la nana 0 × 1 / 2 = 0. Wosɔ. ✓k. Azɔ tsɔ number si kplɔe ɖo, k+1. Ƒoƒo yi k+1 nye (sum up to k) + (k+1) = k(k+1)/2 + (k+1). Algebra ƒe fli ɖeka trɔ esia zu (k+1)(k+2)/2, si nye formula la tututu kple k+1 le k teƒe. ✓Elabena eɖoa anyi le gɔmedzeƒe (0) eye afɔ ɖeka ɖeka tsɔe yia number si kplɔe gbɔ la, eɖoa anyi na whole number siawo katã, ɣesiaɣi, le ɖoɖo kpui ɖeka me. Eyae nye ɖaseɖigbalɛ. Ɖaseɖigbalɛ ƒe kpeɖeŋu wɔa susu ma ke, ke wòkpa doa ɖase be afɔ ɖeka ɖeka, hã "algebra ƒe fli" la, va tso nu si va doŋgɔ me vavã.
Nudzɔdzɔ si wòle be nàxɔ: ɖaseɖigbalɛ trɔa "nɔnɔ siwo me xexlẽ mele o" zu ɖoɖo kpui si wòate ŋu ado kpɔ. Eyae nye ŋusẽ si dodokpɔ metrɔa gbɔgbɔme o.
Tsitreɖoɖo ƒomevi ɖaseɖigbalɛ xɔ ŋusẽa, le akpa aɖe me, tso gɔmesese si klẽ nu tso teƒe si vodadawo tsoe vɛ le gɔmedzeƒe la ŋu. Vodada ɖe sia ɖe si le rule-checking system me tsoa teƒe etɔ dometɔ ɖeka:
| Vodada ƒe teƒe | Nu si wògɔmee | Miate ŋu aɖo ɖase be mele o? |
|---|---|---|
| Nudzraɖoɖo | Mathematics alo rulewo ŋutɔ le vodada (nɔnɔ aɖe bɔ, gɔgɔme vɔ̃ aɖe) | Ɛ̃, tẽ, afi siae tsitreɖoɖo ƒomevi ɖaseɖigbalɛ ƒe dɔƒe le |
| Dɔwɔwɔ | Code la mewɔ nudzraɖoɖo si le nyuie la ɖe vavã o | Le akpa aɖe me; zi geɖe vodada mawo dea dzesi si wòate ŋu akpɔ ɖe megbe |
| Bubu si gbã | Nu si system bliboa ɖo ƒe eŋu la va zu dzodzro vɔ̃ | Ao; bubuwo nye teƒe si womeate ŋu akpɔ ɖe eme o |
Mame sia le vevie wu ale si wòɖe fia, eye Akpa 2 kple 3 ƒe tatɔ le eŋu. Vodada siwo le tsitsini, siwo wɔa vɔ̃ vevie, siwo ate ŋu aɣla ɣesiaɣi, zi geɖe le nudzraɖoɖo me: mathematics ƒe numeɖeɖe si gblɔa nu si system la le be wòawɔ. Eye nudzraɖoɖo lae machine-checked ɖaseɖigbalɛ ate ŋu akpɔ tẽ, nɔnɔ siawo katã ɣeyiɣi ɖeka. Esiae ta tsitreɖoɖo ƒomevi ɖaseɖigbalɛ ƒe dɔ gãwo dea ta ɖe afi ma gbã.
Tsitreɖoɖo ƒomevi ɖaseɖigbalɛ xɔ ŋusẽ, ke eƒe ŋugbedodo me tsitotsito le, eye ne ame mese esia gɔme o la, wòatsɔ ame ayi mɔ vɔ̃ dzi. Eyata míagblɔe kple dzodzro:
Ɖaseɖigbalɛ ɖoa kpeɖeŋu be system la dea nudzraɖoɖo la eme, le bubuwo si woɖo ɖa me. Nu bubu aɖeke o.
Nu ene doa ɖe esia ŋu, eye wo katã le vevie:
Nu si wɔna tsitreɖoɖo ƒomevi ɖaseɖigbalɛ ƒe ŋusẽ va sesẽ wu menye be esia ɖea eƒe ŋusẽ le eme o. Efia wò tututu nu si nèxɔm. Ale si míakpɔe le Akpa 3 me la, Zcash ƒe team si gblɔ wɔnɔƒe kple bubuwo kple nyateƒe ("míeɖo ɖase be supply le nyuie, le bubu siwo woŋlɔ ŋkɔ na me, eye menye ɣaɣla o") nye nyateƒe ma ƒe kpɔɖeŋu.
Be nuŋɔŋlɔ sia nanɔ bɔbɔe na nuxlẽ la, míede wɔwɔ sue. Woaŋlɔa nudzraɖoɖo vavãwo le gbegbɔgblɔ siwo me tsitotsito le me, menye English ƒe nyagblɔɖiwo me o; tsitreɖoɖo ƒomevi ɖaseɖigbalɛ ƒe styles geɖe le (interactive theorem proving, model checking, SMT-based methods) si sɔ na kuxi vovovowo; eye ɖaseɖigbalɛ siawo ŋlɔŋlɔ hã nye dɔ si bia ŋutifafa kple dɔ sesẽ, hã ne AI kpe ɖe ŋu. Míedzo ale si ɖaseɖigbalɛ ƒe kpeɖeŋu wɔa logic le eŋutilã me hã. Esia aɖeke metrɔa nu vevi la o: nudzraɖoɖo, system, kple machine-checked ɖaseɖigbalɛ si fia be wo sɔ, le bubu siwo woɖo ɖa me. Nyatakakadzraɖoɖo la atrɔ gbɔ ne míahi afi si míehiaa.
| Nyagɔme | English ƒe gɔmesese bɔbɔe |
|---|---|
| Formal verification | Ɖoɖo ɖase, to mathematics me, be system aɖe dea nudzraɖoɖo aɖe eme na nɔnɔ siawo katã |
| Specification | Nya si me tsitotsito le si gblɔa nu si "wɔwɔ nyuie" gɔmee |
| System | Mɔ̃ɖaŋlɔ̃, circuit, alo protocol vavã si wole kpɔm |
| Proof | Logic ƒe afɔwo ƒe ɖoɖo kpui si ɖoa nya aɖe ɖase na nɔnɔ siawo katã |
| Proof assistant / theorem prover | Software (Lean, Rocq, Isabelle) si doa ɖaseɖigbalɛ ƒe afɔ ɖeka ɖeka kpɔ |
| Machine-checked | Computer doa kpɔe afɔ ɖeka ɖeka, menye ame ƒe nuxlẽ ko o |
| Induction | Ɖaseɖoɖo ƒe mɔnu: enye vavã le gɔmedzeƒe, eye afɔ ɖeka ɖeka tsɔe yia si kplɔe gbɔ |
| Assumption | Nɔnɔ si ɖaseɖigbalɛ ɖoa eŋu; ne menye vavã o la, kaɖedzi la ate ŋu mado anyi o |
Tsitreɖoɖo ƒomevi ɖaseɖigbalɛ tea dodokpɔ teƒe?
Ao. Woƒoa nu kple wo nɔewo. Dodokpɔ kpɔa dɔ siwo dzɔa le agbe me kple bubu siwo le vodada kple ga sue; verification ɖea vodada ƒomevi blibo aɖewo si dodokpɔ mate ŋu akpɔ gbeɖe o ɖa.
Ne exɔ ŋusẽ alea la, nu ka ta wometsɔ tsitreɖoɖo ƒomevi ɖaseɖigbalɛ kpɔa nu siawo katã o?
Exɔ ga eye wòbia amedzraɖoɖo tɔxɛ, togbɔ be AI ƒe kpekpeɖeŋu le ga ma gbɔm. Woɖea eɖe system siwo me vodada sue aɖe ate ŋu ana gbegblẽ gã ava, afi si eƒe ga nɔa teƒe.
System si woɖo ɖase na le tsitreɖoɖo ƒomevi me ate ŋu ava gbã hã?
Ɛ̃, ne nudzraɖoɖo la le vodada, woɖe gɔgɔme aɖe fia vɔ̃, bubu aɖe meɖo anyi o, alo gbegblẽ la le nu si womeɖo ɖa o. Ɖaseɖigbalɛ la kpɔa nu si wògblɔ be yele kpɔm ko.
Machine-checked ɖaseɖigbalɛ xɔ kaɖedzi wu ame tɔ?
Na ɖaseɖigbalɛ gã siwo me nuwo tsɔ nɔewo me la, zi geɖe ɛ̃. Machine la makpɔ gap si mekpɔ o alo axɔ asiɖeɖe, togbɔ be wòkaɖe eɖokui ɖe nudzraɖoɖo kple gɔgɔme si wonae ŋu hã.
Ne AI kpe ɖe ɖaseɖigbalɛ ŋlɔŋlɔ ŋu la, nu ka ta míaxɔe ase?
Elabena ɖaseɖigbalɛ ƒe kpeɖeŋu la doa afɔ ɖeka ɖeka kpɔ kple machine. AI la tsɔa afɔwo vɛ; machine la kpa doa wo kpɔ. Afɔ si me nyateƒe mele o la, wogbea ɖe megbe ko, eyata AI le dɔ la ƒe kabakaba kpɔm, ke meɖea kaɖedzi la le eme o.
Èɖo ɖase be bank aɖe ƒe software "meɖea mɔ na account balance aɖeke be woayi le zero te o." Ƒe ɖeka megbe la, ga gale buɖum. Aleke wòate ŋu anye be nya eve siawo le vavã le ɣeyiɣi ɖeka me? (Ɖoɖo la le ete.)
Ɖaseɖigbalɛ la ɖo kpeɖeŋu na nɔnɔ ɖeka pɛ: balances mayi le zero te o. Ga ate ŋu abuɖu to mɔ siwo nɔnɔ ma mekpɔ o me, abe vodada si tsɔ funds yia account si mele be woayi o (ke eƒe balance hã mele zero te o), alo vodada le system la ƒe akpa si womeɖo ɖa gbeɖe o me ene. Verification la wɔ tututu nu si wògblɔ be yeawɔ, eye womewɔ nu bubu aɖeke o. Esia nye Akpa 6 ƒe nyakpɔkpɔ le dɔ wɔm: ɖaseɖigbalɛ kpɔa nudzraɖoɖo la, menye gɔgɔme sia ɖe sia ɖe si ate ŋu anɔ be "nyuie" o.
Akpa 2 · Orchard Vodada: Míatrɔ míade 2026 ƒe nya vavã la blibo me. Ɣaɣla system aɖe ɣla gaƒeawo kple cryptography ƒe ɖaseɖigbalɛwo, eye fli ɖeka si womeɖo nudzraɖoɖo de eme akpa blibo o le eƒe mathematics me na ɖaseɖigbalɛwo be woagblɔ alakpa, si na ga maɖiɖi si womeate ŋu akpɔ o wɔwɔ. Míakpɔ tututu nu si "circuit si womeɖo nudzraɖoɖo de eme akpa blibo o" gɔmee, nu ka ta vodada ƒomevi sia ate ŋu aɣla ɣesiaɣi, kple nu ka ta edzɔ kpɔ zi geɖe.
Enye akpa le Formal Verification series na ZecHub.