Komputery na wyścigi dowodzą twierdzenia matematyczne

150 informatyków z Europy, Stanów Zjednoczonych, Indii i Australii spotkało się we Wrocławiu na CADE - najważniejszej na świecie konferencji poświęconej automatycznemu dowodzeniu twierdzeń przy pomocy programów komputerowych.

W środę twórcy 11 najlepszych, najbardziej zaawansowanych programów do dowodzenia twierdzeń matematycznych rywalizowali między sobą w Instytucie Informatyki Uniwersytetu Wrocławskiego. Przyglądali się zmaganiom swoich programów, z których każdy musiał rozwiązać 300 zadań matematycznych.

Ludzie byli tylko obserwatorami, główkowały same komputery. To one musiały wnioskować i rozstrzygać o tym, co jest lub nie jest prawdą. Ośmiogodzinne zawody były na bieżąco relacjonowane w sieci, zwycięzca będzie ogłoszony w czwartek.

- Takie programy mają praktyczne zastosowanie, służą między innymi do sprawdzania poprawności innych programów komputerowych. Zainteresowani śledzą je w sieci, żeby dowiedzieć się, na którym z nich można szczególnie polegać - tłumaczy Jean-Marie de Nivelle, profesor informatyki na UWr, organizator konferencji. - Od ponad pół wieku buduje się programy, które mają zastąpić człowieka w myśleniu. Nasza konferencja pokazuje, do jakiego etapu doszliśmy - dodaje informatyk.

Czy to maszyna, czy to człowiek?

W latach 50. Alan Turing, uważany za ojca informatyki (pracował m.in. nad maszyną do łamania kodu Enigmy,) stworzył test, który ma pokazać, że maszyna myśli podobnie jak człowiek: ekspert prowadzi rozmowę z drugą stroną, nie wiedząc, z kim ma do czynienia. Jeśli nie jest w stanie określić, czy to maszyna, czy człowiek, wówczas uznaje się, że maszyna przeszła test. Dotąd żaden komputer nie zaliczył testu Turinga.

- Ale jesteśmy coraz bliżej momentu, gdy komputery zaczną same myśleć. Już wygrywają w partiach szachowych, poległ nawet sam Kasparow. I potrafią znajdować w programach błędy, których ludzie nie wyłapują - mówi profesor.

Właśnie o takich błędach rozmawiano na wrocławskiej konferencji. Xavier Leroy z Airbusa opowiadał o katastrofie samolotu w 1992 pod Strasburgiem, kiedy zginęło 87 osób. Zdaniem informatyków zawinił program wspomagający pilota.

John Harrison z Intela, największego na świecie producenta układów scalonych, mówił, jak uniknąć powtórzenia błędu, który zdarzył się w jednym z ich procesorów. - Okazało się, że błędnie zaprojektowano w nim funkcję dzielenia. W latach 90. kosztowało to Intel pół miliarda dolarów strat - mówi Tomasz Wierzbicki z Instytutu Informatyki UWr. - Odtąd firmy przykładają wielką wagę do automatycznego weryfikowania procesorów.

Przedstawiciele Microsoft z Cambridge, Seattle i Bangalore mówili o Boogie, systemie do sprawdzania oprogramowania. W czwartek Aarne Ranta, Estończyk współpracujący z Google, pokaże swój program, który tłumaczy na 26 języków, sprawniej niż obecne programy translatorskie.

Uczelnia jako fabryka programisów

CADE, czyli International Conference on Automated Deduction, konferencja na temat automatycznego dowodzenia, od 35 lat odbywa się w różnych miejscach globu. W Polsce gości po raz pierwszy, potrwa do piątku. - Zaproponowałem międzynarodowej radzie naukowej Wrocław, bo to okazja, żeby wypromować miasto, gdzie dużo się dzieje - mówi prof. de Nivelle. Holender, pracuje we Wrocławiu od 2007 roku i planuje osiąść tu na stałe.

- Żyje mi się tu dobrze, ale uciążliwa jest przerośnięta, nieprzyjazna biurokracja na uczelni - uważa. - Wrocławska uniwersytecka informatyka jest w pierwszej polskiej trójce, obok Krakowa i Warszawy. Szkoda tylko, że zbyt często traktuje się nas jako fabrykę taniej siły roboczej, która masowo wypuszcza programistów. Staram się, żeby większy nacisk położyć na badania, ale nie jest to proste w sytuacji, gdy brakuje młodych zmotywowanych naukowców. Utalentowani absolwenci albo idą do biznesu, gdzie na starcie zarabiają 7 tys. zł, albo robią doktoraty w Oxfordzie, MIT czy Kopenhadze, gdzie otrzymują stypendia kilka razy wyższe od naszych.

Podczas kilkudniowej konferencji wręczono nagrodę Herbranda (wyjątkowo zdolny matematyk, zginął jako 23-latek w Alpach) - otrzymał ją Nachum Dershowitz z Izraela (Polak z pochodzenia, wszyscy jego dziadkowie przed wojną wyemigrowali do Nowego Jorku). Uroczystości w Oratorium Marianum towarzyszył koncert: na fortepianie zagrała Asya Kireeva, teściowa profesora de Nivelle. On sam również muzykuje w wolnych chwilach: ostatnio w klubie Łykend grał na gitarze oraz śpiewał francuskie, polskie i rosyjskie pieśni. W czwartek wieczorem prawdopodobnie zagra na pikniku w Ogrodzie Botanicznym z przyjaciółmi z The Dixie Tigers Band.