Sintetiziranje specifikacija za robote
Obećanje dano ljudskom rodu je da će uskoro doći vrijeme kad će roboti raditi naporne poslove, a mi ćemo biti zabavljeni igrama, umjetnošću, intelektualnim i tjelesnim užitcima.¹ Kako bi osigurali da se roboti ponašaju točno onako kako mi želimo, mnogi znanstvenici radili su na automatskoj sintezi robotskog koda iz (formalne) specifikacije.² Dakle, za danu specifikaciju automatski se generira programski kod koji (dokazano) poštuje tu specifikaciju. Na taj način, sinteza koda eliminira mogućnost pogreške pri programiranju. Također, omogućuje svakome da daje robotu nove zadatke (i onima koji nisu vični programiranju). Ipak, postoji jedan problem: odakle dolazi specifikacija?
Popularan izbor za jezik specifikacije je LTL (Linear Temporal Logic): jezik kojim možemo opisati vremenske odnose između događaja (na primjer: “prvo X, onda Y” ili “sve dok nije A, bit će B”). Poznato je da je vrlo lako pogriješiti pri specifikaciji u LTL-u, pogotovo nestručnjacima. Jesmo li onda išta dobili prelaskom sa programa na LTL specifikacije, ili smo samo problemu promijenili ime? U svom radu pokušavam olakšati korištenje LTL specifikacija nestručnjacima.
Promotrimo jednostavni svijet na Slici 1: robot (siva kocka) se kreće po suhim ili mokrim poljima i može sakupljati predmete različitih boja i oblika. Jezik koji robot razumije je LTL. Međutim, što ako se čovjek izrazi na neki prirodniji način, na primjer “uzmi jedan crveni predmet s polja (7,4)”? Naše rješenje je da robot pokuša zaključiti koja je odgovarajuća specifikaciju kroz interakciju s čovjekom. Prvo će robot zatražiti primjer. (Na slici, čovjek daje primjer u kojem robot dolazi do lokacije (7,4) i zatim uzima crveni krug.)
Iz danog primjera i naredbe u prirodnom jeziku, robot će zatim kreirati skup kandidata za specifikaciju. Budući da je broj specifikacija konzistentnih s primjerom jako velik, korištenjem teksta originalne naredbe (dane prirodnim jezikom) fokusiramo se samo na one relevantne. Svejedno, u skupu kandidata i dalje je nekoliko specifikacija, na primjer: a) skupiti crveni predmet, ili b) skupiti sve crvene predmete, ili c) skupiti crveni krug, ili d) prvo ući u vodu, a zatim skupiti crveni predmet. Zato u idućem koraku robot generira novi, simulirani, svijet i pokazuje primjer svog ponašanja u njemu te traži od svog čovjeka da odluči slažu li se primjeri sa zadatkom koji mora biti izvršen. Primjeri su generirani tako da eliminiraju neke od kandidata za specifikaciju. (Na Slici 2 robot kupi samo jedan od dva crvena kruga, bez prethodnog ulaska u vodu. Time eliminira kandidate b i d.)
Naposljetku, kroz nekoliko interakcija s čovjekom, robot dolazi do točne specifikacije. Iz te specifikacije i originalne naredbe, robot generalizira i proširuje svoj jezik: tako će idući put razumjeti naredbu “uzmi sve trokute s polja (10,8)”.
Ovaj pristup omogućuje da robot uvijek zadrži formalni jezik (sa svim prednostima formalnog jezika: jednoznačnost, objašnjivost akcija i slično), ali se taj formalni jezik proširuje kroz interakciju. On nikada ne će biti prirodni jezik, ali nakon duljeg korištenja može konvergirati dovoljno dobroj aproksimaciji prirodnog jezika formalnim jezikom.
Demo sustava dostupan je na ltltalk.mpi-sws.org. Ako vas zanima više, pogledajte 15-minutnu prezentaciju ili pročitajte cijeli rad³.
Ivan Gavran
https://people.mpi-sws.org/~gavran/
gavran@mpi-sws.org
1: Sadašnjost nam se ruga: roboti igraju šah, go, starcraft, pa čak i nogomet, a ljudi i dalje rade
2: Specifikacija opisuje što mora biti izvršeno, bez ulaženja u detalje kako da se to učini. Ipak, svi ti detalji moraju biti prisutni u programskom kodu. Specifikacija je obično puno kraća nego kod. Dobar pregled dosadašnjeg rada na generiranju koda za robote iz specifikacija dan je u članku Synthesis for Robots: Guarantees and Feedback for Robot Behavior
3: Vrijedi spomenuti da se ovaj rad bavi sintezom LTL specifikacija, a primjer s robotima služi kao motivacija. To mu daje poželjnu općenitost: isti se sustav može primijeniti na različite robotske sustave (ne samo na robota koji sakuplja plave i crvene predmete). Bitno je naglasiti i da većina robota (izvan istraživačkih laboratorija) još uvijek ne koristi LTL specifikacije pa je i ovaj rad daleko od primjene u takozvanom stvarnom svijetu :)
