» »

Računalnik (končno) dovolj dober za pravoveren matematični dokaz

Računalnik (končno) dovolj dober za pravoveren matematični dokaz

New Scientist - Leta 1976 sta dva matematika, Appel in Haken, dokazala več kot sto let star problem barvanja zemljevidov (zanima nas najmanj koliko barv moramo uporabiti, da za vsako "državo" velja, da se z nobeno izmed sosed ne ujema v barvi, torej da se nikjer ne stikata dve enako obarvani). No, skoraj dokazala. Težava je bila v tem, da sta pravzaprav le omejila prostor rešitev in nato nad preostanek nagnala računalnik. Čudo tehnike je mlelo in mlelo ter na koncu izplunilo 4 (zavedam se, da do 42 manjka samo ena 2, ampak vseeno se pretvarjajmo, da je podobnost povsem naključna).

Vse lepo in prav, če se v dvatisoč in še nekaj letih matematika ne bi že malo izrodila in začela težiti k (platonski) popolnosti. Po svoje imajo puristi prav. "Zavihajmo rokave in upajmo na najboljše" pristop se vsekakor ne more meriti z eleganco nekajvrstičnih dokazov. Ako bi to novico pisal nekaj dni nazaj, bi mi preostalo le še, da zapadem v že tisočkrat prežvečene debate, češ, je indukcija sprejemljivo orodje? Smo lahko gotovi, da dani program kje ne skriva enklave ščurkov? In tako naprej, nazaj, okoli ovinka in po hribu navzgor vse do zgodnjih jutranjih ur.

Ampak vse to je preteklost! Gonthier in Werner sta dokaz, torej algoritem uporabljen za preiskovanje prostora rešitev, prenesla ("prenesla" se morda ne sliši kot kdo ve kakšen dosežek, ampak v resnici zahteva popolno abstrakcijo tako problema kot rešitve, kar ni mačji kašel) v Coq, jezik za preverjanje logičnih izjav. Pravovernejšega dokaza od povsem abstraktnega formalno-logičnega sistema si težko zaželimo. V kolikor v njunem delu ne najdejo kakšne resne napake, s tem kritikom računalnikov ne ostane več veliko streliva.

Rezultat sam ni pretirano presunljiv, Appel in Haken sta imela prav. Precej bolj presunljive so možnosti, ki jih orodja kot je Coq odpirajo. Microsoft (Gonthier je zaposlen v njihovem raziskovalnem centru na Cambridgu) tako namerava s formalizacijo programske logike zdesetkati populacijo hroščev v svojih izdelkih še preden jih prvič prevedejo.

Na novico nas je opozoril snow. Naj mu vsi hrošči v kodi poginejo!

67 komentarjev

«
1
2

nicnevem ::

Področja, ki so bila še nedavno v domeni biološkega computinga se vztrajno krčijo...

...nasledja "žrtev" bo?

Nekaj sm moral napisat, ko sm ravno prvi ;)

Matev ::

udo tehnike je mlelo in mlelo ter na koncu izplunilo 4


štiri barve še za slovenijo ne bi bile zadosti

OwcA ::

Bi bile. Ni treba, da so vse sosede različnih barv, le enako pobarvane se ne smejo dotikati.
Otroška radovednost - gonilo napredka.

nicnevem ::

Če se ne motim izhaja problem barv iz teorije grafov. Gledaš torej samo 2 sosednji državi - abstraktno si to predstavljamo kot vozlišča (predstavljajo države) in povezave med njimi (ki pomeni da državi mejita ena na drugo)....zdaj pa "barvamo" vozlišča, in gledamo da sta vedno različni barvi na dveh sosednjih, torej takih, ki sta med sabo povezani...

..nekaj takega (direktno iz glave)...


Aja, pozabil sm pohvaliti OwcA-o za odlično novico :)

Zgodovina sprememb…

  • spremenilo: nicnevem ()

WarpedGone ::

Microsoft (Gonthier je zaposlen v njihovem raziskovalnem centru na Cambridgu) tako namerava s formalizacijo programske logike zdesetkati populacijo hroščev v svojih izdelkih še preden jih prvič prevedejo.


Men se tole zdi le prenos problemov/napak na en abstraktni nivo više. Zakaj bi bil pa opis programa v kakšnem višjem/bolj abstraktnem nivoju kej bol odporn na napake? Ko bo to delal si bodo pač omislil še en višji nivo ki bo kontroliral tega etc. Profita pa dejansko ni nobenega.

Rad bi videl človeka ki bo kar na hitro logično pravilno opisal delovanje recimo kakega drajverja etc. Vsak, ki je kdaj kak bol resn program pisal/dizajniral, ve, da hudič tiči v detajlih. Abstrakcija pa velikokrat pomeni ravno odstranjevanje detajlov, ki ti potem povsem nepričakovano skačejo v hrbet.
Zbogom in hvala za vse ribe

OwcA ::

Nekaj napak tako gotovo odkriješ, četudi so povečini tako očitne, da bi jih tudi kartkotrajno testiranje odkrilo, imaš s tem še vedno ta proces vsaj do neke mere avtomatiziran in standariziran.
Otroška radovednost - gonilo napredka.

WarpedGone ::

Owca, se strinjam, sigurno se najde kej. Ampak problem pa je da tem ko sestavš takšen abstraktni opis sistema, kompleksnost celga sistema le še povečaš. In kar naenkrat nucaš še močnejša orodja da vse skup kontroliraš. Vsekakor se najdejo področja kjer je to koristno ampak za splošen softver (ala MS stuff) se počasi kaže da pretirana formalizacija ne prinaša nekega profita (hint: agilne metode).
Zbogom in hvala za vse ribe

Matev ::

potemtakem bi 4 barve bile kar verjetna rešitev
sicer se pa da to v zelo kratkem času čisto praktično preizkusiti

Utk ::

Aja? Kako pa?

Ziga Dolhar ::

Pred dvema tednoma sem v The Economistu ( klik) zasledil članek, ki obravnava to tematiko.

Owca, sicer kul novica, ampak se bojim, da iz nje ni jasno razvidno, kaj točno sploh želiš do-povedat, kakšen pomen ima to "odkritje". Priporočam v branje.
https://dolhar.si/

Matev ::

ja pobarval bi jih

Microsoft ::

Zgleda, da bi bilo kar dosti dela. No, za Avstalijo, Novo Zelandjio, pa se kaj ze ves, da lahko izberes, kar hoces.

Sicer pa, zdaj ko vemo, da je resitev 4. A bi se dalo to resiti z rekurzijo, da bi sel pac od Protugalske proti vzhodu, na voljo bi si vzel 4 barve, in poskusal priti cim dlje. Ce prides do konca, pol je 4 dovolj.:\


by Miha
s8eqaWrumatu*h-+r5wre3$ev_pheNeyut#VUbraS@e2$u5ESwE67&uhukuCh3pr

OwcA ::

Mnja, saj je samo neskončno mnogo mogočih grafov. ;)
Barvaš lahko šele, ko se prebiješ do generatorjev.
Otroška radovednost - gonilo napredka.

Utk ::

In kako bi znal da si jih pobarval optimalno? Tako na blef bi sigurno vsaj nekaj barv več porabu kot je potrebno. Še pri dost manjših grafih ni to tako enostavno.

Matev ::

Očitno se nikjer na svetu ne stika pet držav skupaj.

OwcA ::

Morda velja poudariti, da je sta zemljevid in države dandanes le še prispodobi. Formalno gledano govorimo o ravninskih grafih.
Otroška radovednost - gonilo napredka.

Microsoft ::

Caki, gre se za to, da pobarvas vsako drzavo z eno od 4 barv. Zdej, s katero zacnes je vseeno. Recimo, Portugalska naj bo rumena, potem Spanija zelena, naprej Andora spet rumena. Pride Francija, je rdeca. Potem pa gledas poti naprej. Recimo, da se drzis serverne obale. Tam gor je pol menda Nizozemska, v eno barvo, ki ni enaka Franciji, potem naprej je menda Nemcija, in tako naprej. Recimo, do Rusije. Pa se vrnes nazaj na Francijo in poskusa tiste drzave ob severu, ki se niso pobarvane. In barvas tako navzdol. Ce ne gre vec, se pa vracas. Mogoce bi slo, no.:\


by Miha
s8eqaWrumatu*h-+r5wre3$ev_pheNeyut#VUbraS@e2$u5ESwE67&uhukuCh3pr

Zgodovina sprememb…

CCfly ::

Barvanje grafov z rekurzijo je sizifovo delo.
"My goodness, we forgot generics!" -- Danny Kalev

64202 ::

Ce koga na sploh zanimajo taki vsevrazji jeziki, je tole taprav link: Lambda the Ultimate | Programming Languages Weblog
Sam so dokaj hardkor, ene 50% razumem kaj se tam menijo ;)

nicnevem ::

Zigga, IMHO je bistven pri tej novici dokaz da je dejansko ena mašina sposobna česa takega...da gre za nek napredek tudi na tem področju, ki predstavlja težak posel celo običajnim glavam, kaj šele "butastim" mašinam.

Tistih nekaj potencialnih bugov, ki jih ima pa bo sčasoma zginilo na poti k univerzalni mašini za dokazovanje izrekov...

... malo optimizma ne škodi :)

64202 ::

> Men se tole zdi le prenos problemov/napak na en abstraktni nivo više. Zakaj bi bil pa opis programa v kakšnem višjem/bolj abstraktnem nivoju kej bol odporn na napake? Ko bo to delal si bodo pač omislil še en višji nivo ki bo kontroliral tega etc. Profita pa dejansko ni nobenega.

Ja res, C#/python/... je cisto brezveze, gremo nazaj na 1010011101. ;)

nevone ::

Evo en tak "lep zemljevid" za pobarvat.



o+ nevone
Either we will eat the Space or Space will eat us.

Zgodovina sprememb…

  • zavarovalo slike: OwcA ()

nevone ::

Either we will eat the Space or Space will eat us.

Microsoft ::

In tule je resitev lepega zemljevida. Sm sel na pamet. "Rekurzivno".




by Miha
s8eqaWrumatu*h-+r5wre3$ev_pheNeyut#VUbraS@e2$u5ESwE67&uhukuCh3pr

Zgodovina sprememb…

  • zavarovalo slike: OwcA ()

metalc ::

In ko prideš do držav a la ZDA, Rusija, Azerbajdžan, Hrvaška itd., ki imajo dele ozemlja odrezane od matice (Aljaska, Kaliningrad, Naxičevan, Dubrovnik)? Da kake Francije (Gvajana, en otoček pri Kanadi, Tahiti, Nova Kaledonija, kos Antarktike....) niti ne omenjamo....

Thomas ::

> Dubrovnik

A si ti mau za hece? :\

Thomas ::

Mašina, ki dokaže teorem, da bi nek njen del boljš laufov, če bi bil kako drugačen, se prepiše in recompilira ... se imenuje Goedlova mašina.

No ja, jest zaenkrat še vedno prisegam na probabilistične Goedlove mašine, ampak dopuščam pa tudi, da jih bodo "absolutne" prehitele. Možno je tudi.

Thomas ::

> A si ti mau za hece?

Ne, ti si čisto resen, mene matra nekej. Sem kar pozabil na izhod Bosne na morje!

Silly myself!

Posip, posip, posip ... z bukovim pepelom!

poweroff ::

Avtorji poročila "CyberInsecurity: The Cost of Monopoly" so mnenja, da bodo neuspešni tudi poiskusi podjetja Microsoft da izboljša varnost svojih sistemov, če bo stranski učinek tega še večje priklepanje uporabnikov nanje. Problem je namreč monokultura.

Poleg tega s kompleksnostjo sistema narašča število napak v njemu. Odpravljanje napak pa kompleksnost še poveča. Zato izboljševanje varnosti ni linearno - potrebno je več sredstev za izboljšanje varnosti bolj kompleksnega sistema.

Primer: SP2, kjer je odpravljanje napak povzročilo nove.
sudo poweroff

Thomas ::

> Poleg tega s kompleksnostjo sistema narašča število napak v njemu.

To sploh ni nujno res. Kompleksnost NIKAKOR ne pomeni nujno, da je napak več, lahko jih je tudi precej manj. Zelo kompleksni sistemi so poljubno verjetno brez napake.

Sej to si ni tako težko predstavljat. Poleg osnovnega sistema še en kup skrutinerjev, ki lovijo vsako napako in zaustavijo sistem, kakor hitro se kakšna pojavi.

Spontani splav v zgodnji nosečnosti recimo, je živ primer tega principa.

WarpedGone ::

Sej to si ni tako težko predstavljat. Poleg osnovnega sistema še en kup skrutinerjev, ki lovijo vsako napako in zaustavijo sistem, kakor hitro se kakšna pojavi.


In od kje se vzamejo ti skrutinerji?
Če je to avtomatika, je takoj del sistema in dodatna kompleksnost, ki jo je treba vzdrževat.
Edin učinkovit poznan način za zmanjšanje napak, je zmanjšanje kompleksnosti in primeren pristop k delu.

Software is cheap, reliable and fast. Pick two.
Zbogom in hvala za vse ribe

Thomas ::

Po tvoji logiki bolj komplicirane molekule sploh ne bi mogle obstajati. Bi takoj razpadle v atome.

Ampak ni tako. Očitno je DNA kar stabilna stvar.

BBB ::

> OwcA,
> Mnja, saj je samo neskončno mnogo mogočih grafov.

Kako ti prideš to neskončno mnogo grafov, ko pa jaz dojemam le enega in edinega. Namreč gre za graf tipa planarne topologije, ki se jo povzame iz geometrijskih relacij, za katere velja pogoj, da se sosednji državi stikata ob meji, meja pa je lahko tudi meddržavna stoječa površinska voda. To se prevede na logične relacije med elementi grafa, geometrijo pa se popolnoma odpiše. Ostane le topološki opis relacij med elementi grafa, tj. med vozlišči, vejami in ploskvami (node, edge, face). Lege ploskev, ki jih obdajajo veje, so opredeljene glede na stran veje, pri čemer mora imeti veja opredeljeno usmerjenost. Vozlišče predstavlja tro- ali večmejo (ali točko mejitve para držav na vodno površino ), veja razmejuje par držav ali meddržavno vodno površino. Ploskev pa je ali država ali pa meddržavna vodna površina (identitete držav oz. meddržavnih vodnih površin referenciramo na ploskve). V primeru države Vatikan je veja dejansko zaključena same vase (ima eno vozlišče). Dejansko dobimo preprost logični model, ki matematično nima povsem nič skupnega z geometrijo. To je povsem nekaj običajnega pri modeliranju prostorskih podatkov v sistemih GIS (navadno se še vedno ločeno ohranijo geometrijski zapisi, če že ne zaradi drugega, pa zaradi grafičnega uporabniškega vmesnika za prikaz in urejanje vektorskih podatkov). Torej, množica držav in meddržavnih vodnih površin je povezana lahko le na en in edini možen s planarno topologijo opredeljen način.

Za rešitev naloge je potrebno izdelati primeren algoritem, ki podatke jemlje iz tega topološkega modela.

OwcA, morda razpoznaš ti še kakšno drugo planarno topologijo, torej planarni graf?

OwcA ::

Če hočeš nekaj induktivno dokazati moraš preiskati cel prostor rešitev. Topološko je to seveda samo en genus 0 prostor, ampak razrezov (kart) je pa neskončno in pregledati moraš vse.
Otroška radovednost - gonilo napredka.

Zgodovina sprememb…

  • spremenilo: OwcA ()

BBB ::

Abstrakcija problema je dvorezen meč. Na eni razsloji problem v nekakšno hierarhijo laže obvladljivih podproblemov, po drugi pa zakoliči strukturo hierarhije. Tako se poenostavi problem hkrati pa omeji maneverski prostor. Na takšni osnovi je bil izveden razslojen komunikacijskim odel ISO OSI, znotraj programskih jezikov objektno programiranje, opisni jeziki (npr. za programiranje central, kjer se lahko na pol grafično napiše SPECIFIČEN!!! algoritem), upravljanje avtomobila, državno upravne ureditve ...

Tako ministru za gospodarstvo ni potrebno skrbeti, iz kakšnega materiala mora biti šrauf (vem, da zalše zveni vijak, a se šrauf navadno lepše zateguje) in s kakšnim navorom ga mora zategniti nek delavec v strojnem podjetju. Bo pa usoda tega delavca precej odvisna od kritičnih odločitev ministrov, pa tudi ali bo povprečen delavec zategoval šraufe v tanke ali v turbine hidroelektrarn. Na višjem abstrakcijskem sloju imaš bolj posreden in manj določen vpliv na spodnje sloje. Ravno zato minister ne bo mogel neposredno odločati o zategovanju šraufuv - omejitev manevrskega prostora le na njegovo domeno. Dispečer v logističnem centru govori, kam naj šoferji dostavijo robo, ne ukvarja pa se s tem, kdaj naj kdo pritisne na gas, kuplungo ali žlajf. S tem pa se zagotovi, da vsak proces deluje le v svoji domeni in v interakciji z njemu podrejeno in nadrejeno domeno - nič dlje. Ugotavljanje napak v takšnem sistemu je veliko lažje, nadzorovati pa je seveda potrebno vse sloje, pri čemer državna ureditev navadno odpove.

Pri programiranju so zadeve z abstrakcijo zelo podobne. Nizkonivojske funkcije, ki so neposredni ukazi procesorju, ne smejo biti neposredno povezani s funkcijami, ki jih vnaša programer. Prav tako je mogoče ustvarjati skulpture struktur, podobno kot iz lego kock. Večja kot je abstrakcija, enostavno zapišemo porblem, a imamo na razpolago manj izraznih sredstev - pride do večjega vpliva vkalupljanja v standardne spodne sloje. Detajlov izvedbe ne bomo mogli opredeliti, za to bo poskrbelo razvojno okolje ali izvajalni sistem. Če malce osvetlim primerjavo: primer neabstraktnosti s popolno neposrednostjo bi bil, če bi Janša vsaki čistilki posebej rekel, da naj npr. z dvigom pokrova školjke in z uporabo ščetke s krožnibi gibi spuca školjo, vsakemu zidarju, kako naj se loti zidave itd. Seveda bi tako vodil državo kot celoto, a vendar sigurno precej manj uspešno kot sedaj, napak pa bi kar mrgolelo. To je podobno kot bi operacijski sistem napisali v strojnem jeziku z neposredno obravnavo vseh sodelujočih komponent - totalna zbrka. Velik del k abstrakciji je pripomoglo ločevanje strojne od programske opreme z vmesnim softverom - drajverji. Tudi jedro operacijskega sistema je ločeno od programov. Primer je tudi uporaba objektnega koncepta - očitno vzeto iz koncepta legic.

poweroff ::

V bistvu lahko tudi v kompleksnem sistemu zmanjšaš št. napak. Vendar je potrebno nesorazmerno večje število energije za odpravo enakega števila napak kot v nekompleksnem sistemu.

K MSju pa prištejemo še marketinški boj (izdelke hitro ven, brez obsežnih priskusov) in priklepanje uporabnikov - dva velika minusa za varnost.
sudo poweroff

d20 ::

mathai kwa se gres to en politicn aktivizm in kvaris dobro novico?!? mislm ce nimas kej pametnga povedat bod tih!

:\
http://www.worldjumpday.org

Thomas ::

Pomembno je vedeti, da večja kompleksnost lahko pomeni večjo zanesljivost delovanja sistema, celo ob manjši porabi virov.

To je kontraintuitivno, ampak resnično.

B-D_ ::

Sej je dokej na izi skapirat, da so 4 barve zadosti...

če ima država samo 2 sosedi rabiš 3 barve: levo, desno pa sebe
če ma država 3 sosede rabiš 4 barve: prvo, drugo, tretjo pa sebe
če pa ima 4 sosede pa rabiš spet samo 3 barve: zgornja+spodnja, leva+desna in sebe
itd...

Ni ravno velka znanost, sam mašinerija ki to pofarba mora biti dokaj ;) vztrajna. Hitrost itaq samo mi ljudje hočemo, compu se jebe kolk mileniumov računa, da je odgovor življenja, vesolja in vsega... 42 :D

Matev ::

če ma država 3 sosede rabiš 4 barve: prvo, drugo, tretjo pa sebe


če ima država tri sosede lahko potrebuješ samo tri barve... eno zate in eno za dve sosedi, tretja soseda ima pa tretjo barvo

edit: ker je lahko morje med posameznima sosedima

Zgodovina sprememb…

  • spremenil: Matev ()

B-D_ ::

Oziroma v primeru vatikana... 2 barvi - 1 soseda, ki obkroža državo

drejc ::

No, ob vsem tem pompu je nekdo pozabil link do matematičnega dokaza tega izreka.
"Rise above oneself and grasp the world"
- Archimedes of Syracuse

drejc ::

bidi: Izrek gre tkole

Vsak ravninski graf lahko pofarbamo z največ štirimi barvami.

Tole dokazat pa ni lih arašid.
"Rise above oneself and grasp the world"
- Archimedes of Syracuse

nicnevem ::

64202 ::

Fijavz? Hehe, sem ga imel. Pa je dostikrat tako zgledalo, da on rece "no, imamo A in potem se jasno vidi kako se dobi B". Jaz sem pa med A in B videl samo en klif pa morje polno morskih psov do obzorja. Sem pa vseeno spacal devetko 8-)

Microsoft ::

Fijavz zdej predava, ce ma pa vaje, pa nevem.


by Miha
s8eqaWrumatu*h-+r5wre3$ev_pheNeyut#VUbraS@e2$u5ESwE67&uhukuCh3pr

Matev ::

Vsak ravninski graf lahko pofarbamo z največ štirimi barvami.


lahko ga pobarvamo tudi z eno sama barvo če je treba

drugače pa izrek ni točen - kaj se nampreč zgodi če je v eni točki meja petih držav

tako kot tromeja - samo da namesto slovenije, avstrije in madžarske ali italije je tam pet držav - ki se stikajo v točki

B-D_ ::

Kako pa ti misliš, da je bilo najenostavneje dokazat, da so 4 barve dovolj? You guessed it. Nobena država nima "pet-meje". Trivialen dokaz, pa vseeno deluje.

OwcA ::

Nepopisno mi je žal, da sem uporabil izraz zemljevid. :\
Otroška radovednost - gonilo napredka.
«
1
2


Vredno ogleda ...

TemaSporočilaOglediZadnje sporočilo
TemaSporočilaOglediZadnje sporočilo
»

Prihodnost JavaScripta

Oddelek: Novice / Brskalniki
93766 (3061) M.B.
»

MySQL 5.0 zrel za delovno okolje

Oddelek: Novice / Ostala programska oprema
183515 (2665) krho
»

DIY HPC

Oddelek: Zvok in slika
375226 (4736) Eboran
»

Računalnik (končno) dovolj dober za pravoveren matematični dokaz (strani: 1 2 )

Oddelek: Novice / --Nerazporejeno--
677889 (6259) Thomas

Več podobnih tem