Wiadomości » Wrocław »
W zawodach informatycznych zwyciężyły Vampire i E
W zawodach informatycznych zwyciężyły Vampire i E
W piątek we Wrocławiu zakończyła się najważniejsza na świecie konferencja o automatycznym dowodzeniu twierdzeń przy pomocy programów komputerowych
Przez kilka dni informatycy z Europy, Stanów Zjednoczonych, Indii i Australii zajmowali się na Uniwersytecie Wrocławskim systemami, które dowodzą twierdzenia, czyli potrafią same przeprowadzić rozumowanie. Jeden z gości konferencji, Estończyk Aarne Ranta, wykorzystał taki system w programie tłumaczącym teksty w 26 językach. Trudność automatycznego przekładu tekstów polega na tym, że to samo słowo może mieć wiele znaczeń. Np. angielskie słowo "go" zwykle tłumaczymy na polskie "iść". Jednak zdania "I go to London" nie przetłumaczymy na "Idę do Londynu", tylko "Jadę do Londynu". Program Grammatical Framework Aarne Ranty używa systemu dowodzenia twierdzeń, by odrzucić pierwsze tłumaczenie jako niepoprawne. Program przeprowadza rozumowanie, z którego wynika, że nie można "pójść" do Londynu, gdyż leży ponad 1000 km stąd, a po drodze mamy ponadto kanał La Manche, którego piechotą nie przekroczymy. Jakość takiego tłumaczenia jest znacznie lepsza niż w przypadku prostych translatorów, gdyż program w pewnym sensie "rozumie" tekst, który tłumaczy.
Twórcy 11 programów do dowodzenia twierdzeń matematycznych rywalizowali między sobą: ich systemy musiały rozwiązać 300 zadań matematycznych.
W głównych kategoriach zwyciężył program Vampire, stworzony przez Andrieja Woronkowa z uniwersytetu w Manchester, oraz E, autorstwa Stephana Schulza. Vampire jest jednym z najbardziej znanych systemów dowodzenia twierdzeń, rozwijanym od ponad 10 lat (stale pracuje nad nim dwóch programistów na pełnym etacie). - Vampire zwyciężał już wielokrotnie, nie było więc zaskoczeniem, że i w tym roku znalazł się na podium - mówią organizatorzy.
Stephan Schulz tworzy oprogramowanie dla centrum kontroli lotów w Karlsruhe, a system E napisał w wolnym czasie.
- Jednym z popularnych i znanych w świecie systemów jest Mizar rozwijany w Polsce, w Białymstoku, od 1973 roku. Mizar nie brał jednak udziału w zawodach. Jego twórcy wykorzystują go obecnie do sprawdzenia poprawności dowodów w niemal 400-stronicowej książce matematycznej "A Compendium of Continuous Lattices". Do tej pory nie wykryli na szczęście żadnego błędu. Grupa w Białymstoku posiada największą na świecie kolekcję twierdzeń matematycznych sprawdzonych przez komputer - mówi Tomasz Wierzbicki z Instytutu Informatyki UWr. - Od ponad pół wieku buduje się programy, które mają zastąpić człowieka w myśleniu i ta konferencja pokazuje do jakiego etapu doszliśmy - mówi prof. Jean-Marie de Nivelle z UWr, organizator wrocławskiej konferencji. W latach 50. Alan Turing stworzył test, który ma pokazać, że maszyna myśli podobnie jak człowiek. Dotąd żaden komputer nie zaliczył testu Turinga.
- Ale najbliżej jego rozwiązania jest chyba zbudowany i zaprogramowany przez IBM w technologii DeepQA komputer Watson, który z sukcesem wygrywa w telewizyjnej grze "Jeopardy" - mówi prof. Leszek Pacholski, dyrektor Instytutu Informatyki Uniwersytetu Wrocławskiego. - W zespole, który przygotował Watsona do quizu, kluczową rolę odegrał Włodek Zadrożny, mój doktorant z 1980 roku. Gra "Jeopardy" to bardzo zaawansowana gra "na inteligencję". Zadaje się pytania, ale żeby na nie odpowiedzieć, nie wystarczy wiedza, potrzebne są także nietypowe skojarzenia - dodaje. Na konferencji jest także inny jego doktorant Michał Moskal, o którym pisaliśmy przed pięciu laty. Jako jedyny z Polski, wówczas 25-latek, został zaproszony do jednego z najlepszych informatycznych centrów naukowych na świecie -Microsoft Research w Redmond w stanie Waszyngton, w głównej siedzibie Microsoftu. - Michał jest jednym z głównych autorów programu "Hypervisor", który umożliwia jednoczesne uruchomienie na jednym komputerze kilku systemów operacyjnych, można na przykład jednocześnie korzystać z Windows i z Linuxa - dodaje profesor Pacholski. 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ła po raz pierwszy.
Źródło: Gazeta Wyborcza Wrocław
http://wroclaw.gazeta.pl/wroclaw/1,35751,10068727,W_zawodach_informatycznych_zwyciezyly_Vampire_i_E.htmlDodano: 05-08-2011 13:15Odsłon: 215
Dodano: 05-08-2011 13:15
Odsłon: 215