Bakalaŭra tezo pri programado per limigoj
junio 2019
Superrigardo
Kiel bakalaŭra studento pri komputiko, mia esploro komenciĝis per praktika demando: kiam simulilo amasigas multajn eblajn kondiĉojn, kiel oni igas ĝin ĉesi rekonsideri tiujn, kiuj jam ne povas okazi? Mi ellaboris kaj taksis por HydLa metodon, kiu uzas la direkton, en kiu valoro ŝanĝiĝas, por forigi el la serĉo la kondiĉojn perdintajn sian sencon. En la referenca modelo, la tuta simulada tempo malpliiĝis al proksimume duono.
Ĉi tiu laboro estas unu el la plej fruaj fundamentoj de mia dezajna filozofio. La programado per limigoj instruis al mi, ke kompleksaj rezultoj ne ĉiam devas esti rekte difinitaj: ili povas aperi el zorge difinita spaco de reguloj, prioritatoj kaj limoj. Tiu pensmaniero subtenas hodiaŭ mian manieron dezajni el limigoj en la epoko de artefarita inteligenteco — dezajni la kondiĉojn, ene de kiuj generanta sistemo rajtas libere agi.
Resumo
HydLa estas modeliga lingvo por hibridaj sistemoj: sistemoj, en kiuj kontinua ŝanĝo kaj diskretaj eventoj interagas. Ĝia sur limigoj bazita konstruo permesas priskribi tiajn sistemojn koncize kaj simuli ilin kun alta precizeco. La prezo estas, ke granda modelo povas lasi la simulilon kontroli grandegan nombron da kondiĉaj reguloj eĉ post kiam kelkaj el ili jam perdis ĉian gravecon.
Ĉi tiu esploro proponis redukti tiujn gardatajn limigojn dum la rulado. Rekonante monotonan konduton — valoron, kiu daŭre moviĝas en unu direkto — la simulilo povas konstati, ke certaj gardoj neniam plu iĝos veraj estonte, kaj sekure ĉesi kontroli ilin. La aliro montriĝis precipe efika ĉe modelo kun multaj simile gardataj objektoj, kie la mezurita rultempo falis al proksimume duono de la origina.
1. Enkonduko
Hibrida sistemo kunigas kontinuan konduton kun diskretaj eventoj. Saltanta pilko estas simpla ekzemplo: ĝia pozicio kaj rapido ŝanĝiĝas kontinue dum ĝi estas en la aero, sed la momento, kiam ĝi trafas surfacon, kreas diskretan eventon, kiu ŝanĝas ĝian direkton. Termostatoj, veturiloj kaj robotoj enhavas la saman miksaĵon en pli konsekvencaj formoj.
HydLa permesas priskribi tiajn sistemojn per matematikaj kaj logikaj limigoj anstataŭ elskribi ununuran proceduran sinsekvon. Ĝia simulilo HyLaGI kapablas kalkuli simbole sen rondiga eraro kaj labori kun necertaj parametroj. Tiu esprimpovo tamen kreas problemon de skalo: kiam modelo enhavas multajn regulojn, kiuj aktiviĝas nur sub apartaj kondiĉoj, la simulilo devas ree kaj ree demandi pri ĉiu kondiĉo, ĉu ĝuste ĝi okazos sekve.
2. Gardataj limigoj en la simulado
Gardata limigo estas regulo, kiu aktiviĝas nur kiam ĝia garda kondiĉo plenumiĝas. En la supra referenca modelo ĉiu sekcio de la surfaco havas propran regulon: se la pilko atingas alton nulo dum ĝia horizontala pozicio troviĝas ene de tiu sekcio, validas la resalta regulo. Dividi la surfacon en pli da pecoj do donas al la simulilo pli da gardoj por trarigardi.
La eksperimento variigis la nombron de sekcioj de 10 ĝis 200. La origina simulilo malrapidiĝis proksimume laŭ la kvadrato de tiu nombro. Tio gravas preter la ludila ekzemplo: pli granda modelo povas prezenti multajn fizikajn objektojn, kontaktajn regionojn aŭ eblajn eventojn ĝuste en tiu gardata formo.
3. Kie kuŝas la mallarĝejo
Profilado montris, ke la malrapidiĝo ne disvastiĝis egale tra la simulilo. Kun 100 surfacaj sekcioj, 96 % de la mezurita rultempo pasis en FindMinTime, la operacio, kiu serĉas la plej fruan eblan sekvan eventon. Ĝi ree kaj ree taksis la gardojn de ĉiu kandidata limigo.
Tiu rezulto konkretigis la celon de la optimumigo: malpliigi la nombron de gardoj, kiujn FindMinTime devas konsideri, konservante precize la saman simulatan konduton.
4. Redukto de gardataj limigoj
Imagu pilkon, kiu saltante malsupreniras ŝtuparon. Post kiam la pilko preterpasis ŝtupon kaj daŭre moviĝas antaŭen, tiu ŝtupo jam ne povas influi ĝin. Homo, kiu rigardas la desegnon, tuj forlasas la ŝtupojn malantaŭ la pilko; la origina algoritmo daŭre kontrolis ĉiun el ili.
La malfacila parto estas pruvi, ke forĵetita gardo ne estos bezonata poste. Forigi ĝin nur ĉar ĝi nun estas malvera povus silente doni malĝustan rezulton, se ĝi denove iĝus vera. La propono do apogas sin sur monotoneco: ĉu estas garantiite, ke variablo daŭre kreskas aŭ daŭre malkreskas dum tempa intervalo.
4.1 Aliro al unuforma monotoneco
La unua aliro validas, kiam variablo moviĝas en unu direkto dum la tuta simulado. En la modelo kun dividita surfaco la horizontala pozicio de la pilko ĉiam kreskas. Post kiam ĝi transiris sekcion, la kondiĉo de tiu sekcio neniam plu povas plenumiĝi. Teknikoj de modelkontrolado povas establi tiun econ antaŭ la simulado, tiel ke la gardoj, kiuj perdis sian sencon, forigeblas sekure dum la rulado progresas.
4.2 Aliro al alterna monotoneco
Multaj realaj sistemoj ne moviĝas en unu direkto por ĉiam. Variablo povas kreski, turniĝi kaj poste malkreski. La artikolo do skizis duan aliron: komenci per supozita direkto, kontroli tiun supozon per asertoj, kaj rekomenci la reduktan logikon de la punkto, kie la direkto ŝanĝiĝas. La gardoj forigitaj por unu monotona intervalo estas restarigitaj, kiam komenciĝas la sekva.
5. Eksperimentaj rezultoj
Mi realigis la aliron de unuforma monotoneco kaj taksis ĝin per la modelo kun dividita surfaco. Kaj la origina, kaj la proponita algoritmo plu bezonis pli da tempo, ju pli kreskis la nombro de sekcioj, sed la proponita versio konstante faris malpli da laboro. Komparante la adaptitajn kurbojn, la ĉefa koeficiento falis de 1,1463 al 0,6083; por ĉi tiu referenca kazo la tuta simulada tempo proksimume duoniĝis.
La rezulto ne asertas, ke ĉiu modelo en HydLa iĝas duoble pli rapida. Ĝi montras, kie la metodo helpas: ĉe modeloj kun multaj gardataj objektoj kaj pruvebla direkto de ŝanĝo, kie la gardoj iĝas por ĉiam sensignifaj dum la rulado.
6. Konkludo kaj estonta laboro
La esploro montris, ke scio pri la modelo — ne nur pli rapida malaltnivela kalkulado — povas fari simuladon pli efika. Uzante monotonecon por rekoni, kiuj eblecoj iĝis neeblaj, HyLaGI povas malgrandigi sian aron da aktivaj limigoj sen ŝanĝi la rezulton.
La realigita eksperimento kovris la unuforman monotonecon. La artikolo lasis du direktojn por poste: taksi la aserto-bazitan metodon por alterna konduto, kaj uzi aliajn invariantojn ol la monotoneco por trovi pliajn limigojn, kiuj forigeblas sekure.
Takafumi Horiuchi kaj Kazunori Ueda. “Dynamic Reduction of Guarded Constraints for the Hybrid Systems Modeling Language HydLa”. La 33-a Jarkonferenco de la Japanese Society for Artificial Intelligence, 2019. DOI: 10.11517/pjsai.JSAI2019.0_1E3OS3b02.