James Bornholt

Képezhet-e ideghálózatot SMT-megoldóval?

2018. augusztus 2

Igen, és megtettem, de nem szabad.

Hacsak nem későn éltél, tudod, hogy a gépi tanulás átalakítja a számítástechnikát. Az egyik saját kutatási területem, a programszintézis - az az ötlet, hogy automatikusan létrehozhatunk egy programot annak specifikációjából, hogy mit kell tennie?.

A gépi tanulás és a programszintézis feltűnően hasonló. Gépi tanulási problémaként keretezhetjük a programszintézist: keressünk meg néhány modellt (programszintaxist) egy modellhez (programszemantika), amelyek minimalizálják a veszteségfüggvényt (programhelyesség). A programszintézis-kutatás legutóbbi idők legizgalmasabb eredményei ezt a megfigyelést használják fel, gépi tanulási technikákat alkalmazva a hagyományos szintézisalgoritmusok kibővítésére, sőt helyettesítésére. A gépi tanulás megközelítései különösen jól alkalmazhatók például a példa-alapú szintézishez, amelyben a specifikáció olyan input-output példák összessége, amelyeknek a szintetizált programnak meg kell felelnie.

De a hasonlóságok mindkét irányban futnak. A gépi tanulás programszintézis problémának tekinthető, amelyben megpróbálunk néhány lyukat (súlyt) kitölteni egy vázlatban (modellben), hogy kielégítsük a specifikációt (minimális veszteség). Használhatunk-e programszintézis technikákat gépi tanuláshoz? Ez az irány büntetőjogi szempontból kevéssé ismert a szakirodalomban, ezért gondoltam, hogy lövést adok neki egy osztályprojekt részeként.

Gépi tanulás programszintézis segítségével

A szintézis eszközök a legjobban ismerik a munkát, ha logikai kényszereket oldanak meg SMT-megoldóval. A gépi tanulás programszintézis alkalmazásával a gépi tanulási problémát szintézisproblémává kódoljuk, és megoldjuk az ebből adódó logikai korlátokat.

Miért kipróbálnánk ezt a megközelítést, amikor a gradiens süllyedés és annak jellege olyan jól működik a nagy gépi tanulási modellek képzéséhez? Úgy gondolom, hogy a szintézisnek négy lehetséges erőssége van:

Természetesen van néhány jelentős kihívás is. A legkiemelkedőbb a méretezhetőség lesz. A modern mély tanulási modellek mind a képzési adatok (példák milliói, mindegyik ezer dimenzióval), mind a modell mérete (a megtanulandó súlyok milliói) szempontjából óriásiak. Ezzel szemben a programszintézis kutatás általában több tíz vagy száz művelet nagyságrendű programokkal foglalkozik, kompakt specifikációkkal. Ez nagy rés a híd áthidalására.

Hogyan képezzünk egy modellt szintézissel

Ebben a bejegyzésben a (teljesen összekapcsolt) ideghálózatok képzésére fogunk összpontosítani, mert most nagyon dühösek. Az ideghálózat szintézis segítségével történő kiképzéséhez megvalósítunk egy vázlatot, amely leírja az előre haladást (azaz kiszámítja a hálózat kimenetét egy adott bemenetre), de a súlyokhoz lyukakat használunk (amelyeket ? jelölünk) (amelyeket meg fogunk kérdezni a szintetizátor, hogy megpróbálja kitölteni):

Ideghálózati szintetizátorunkat Rosette-ben fogjuk megvalósítani. Az előremenő lépés megvalósításához csak arra van szükség, hogy leírjuk egyetlen idegsejt aktiválását - kiszámítva a bemenetek és a súlyok ponttermékét, majd alkalmazva a ReLU aktiválási függvényét:

Most kiszámolhatjuk az egész 1 réteg aktiválását:

És végül számítsa ki a teljes hálózat kimenetét, figyelembe véve annak bemeneteit:

Az XOR szintetizálása. Az XOR függvény a kanonikus példa arra, hogy rejtett rétegekre van szükség egy ideghálózatban. Egy rejtett réteg elegendő szabadságot ad a hálózatnak az ilyen nemlineáris függvények elsajátításához. Használjuk egyszerű neurális hálózati megvalósításunkat az XOR szintetizálására.

Először létre kell hoznunk egy vázlatot a kívánt ideghálózati topológiához. Minden réteghez létrehozunk egy ismeretlen (egész) tömegű, megfelelő méretű mátrixot:

Köztudott, hogy egy 2-2-1 topológiájú hálózat (azaz 2 bemenet, egy rejtett 2 neuronréteg, 1 kimenet) elegendő az XOR megtanulásához, ezért készítsünk egy ilyen alakú vázlatot, és majd állítsa, hogy a hálózat megvalósítja az XOR-t:

Végül megkérhetjük Rosette-t, hogy oldja meg ezt a problémát:

Az eredmény egy olyan modell, amely értékeket ad a súlyaink számára, amelyet az értékelés segítségével ellenőrizhetünk:

előállítja a súlyokat:

vagy vizuális formában:

Infrastruktúránkat felhasználhatjuk az ideghálózatok tulajdonságainak igazolására is. Például be tudjuk bizonyítani a fenti állítást, miszerint nem lehet hálózatot megtanulni az XOR számára rejtett réteg nélkül. A vázlat definíciójának megváltoztatásával kizárja a rejtett réteget:

és újra megpróbálva a szintézist, azt találjuk, hogy M kielégíthetetlen megoldás; más szóval, nincs hozzárendelve (egész) súly ehhez a topológiához, amely helyesen valósítja meg az XOR-t.

Macskafelismerő kiképzése

Térjünk át az XOR-ról korunk talán legfontosabb informatikai problémájára: a macskaképek felismerésére. A képfelismerés több szempontból is hangsúlyozza a szintézis alapú képzési folyamatunkat. Először is, a képek jóval nagyobbak, mint az XOR egybites bemeneteinek ezernyi képpontja, egyenként három 8 bites színes csatornával. Sokkal több képzési példára lesz szükségünk, mint az XOR-nál használt négynél. Végül meg akarjuk vizsgálni az egyszerűbbnél nagyobb topológiákat az XOR neurális hálózatunk számára.

Optimalizálás és szintézis

XOR példánkban egy tökéletes ideghálózatot kerestünk, amely minden edzésbemenetünknél helyes volt. A képek besorolása szempontjából nem valószínű, hogy ilyen hálózatot találunk. Ehelyett minimalizálni szeretnénk néhány veszteségfüggvényt, amely rögzíti a jelölt hálózat által elkövetett osztályozási hibákat. Ez kvantitatívvá teszi szintézisproblémánkat: keresse meg azt a megoldást, amely minimalizálja a veszteségfüggvényt.

A kvantitatív szintézisprobléma megoldásának kifinomult módjai vannak, de tapasztalatom szerint az alábbi naiv megoldás meglepően hatékony lehet. Példaként tegyük fel, hogy egy klasszikus kuka-csomagolási problémát akarunk megoldani: öt olyan tárgyunk van, amelyek a, b, c, d és e súlyúak, és minél többet kell csomagolni egy zacskóba anélkül, hogy túllépnénk a T súlyhatárt. Létrehozunk egy szimbolikus logikai változót annak jelzésére, hogy minden objektum csomagolva van-e, és meghatározzuk a megfelelő súlyokat:

Most meghatározunk egy költségfüggvényt az optimalizáláshoz, megadva nekünk a csomagolásunk teljes tömegét:

Az optimális objektumkészlet megtalálásához először meg kell találnunk egy kezdeti halmazt, majd rekurzív módon arra kérjük a megoldót, hogy találjon jobb megoldást, amíg ez már nem sikerül: 2

Ennek a példának a futtatása 80-as T értékkel a következő kimenetet kapja:

Három megoldást találtunk, 60, 70 és 75 költségekkel. Az optimális megoldás az a, b és e tárgyakat tartalmazza, össztömegük 75.

A macskák felismerése metaszkettekkel

A POPL 2016 cikkünkben szereplő értékelés részeként szintetizáltunk egy neurális hálózatot, amely egyszerű bináris osztályozó volt a macskák felismerésére, ugyanazzal az optimalizálási technikával, mint fent. A cikkben bemutatott metaszketch-absztrakciónkat rácskutatásra használtuk a lehetséges neurális hálózati topológiák felett. Képzési adataink 40 példát vettek fel a CIFAR-10 adatkészletből. 20 kép macskáról és 20 kép repülőgépről, amelyek mindegyike 32-32 színes pixel.

Mintha egy ilyen kicsi, alacsony felbontású edzőkészlet használata nem lenne elegendő engedmény a skálázhatósághoz, az edzésképeket 8 × 8 szürkeárnyalatosra csökkentettük.

35 perces edzés után szintézis eszközünk olyan neurális hálózatot generált, amely 95% -os pontosságot ért el a képzési példákon. Azt is bebizonyította, hogy a képzési készlet további pontosságának javítása lehetetlen: a hálózati topológia (a rácskeresés határain át) vagy a súlyok megváltoztatása nem javíthatja az edzéskészlet pontosságát. A teszt által beállított pontosság sokkal rosszabb volt, mint amire csak 40 példával számíthatunk.

Ez az eredmény nyilvánvalóan nem fogja forradalmasítani a gépi tanulás területét. Célunk ennek a kísérletnek a végrehajtása volt annak bemutatása, hogy a metaszketchek képesek megoldani az összetett költségfüggvényeket (vegye figyelembe, hogy a neurális hálózat szintetizálásának költségfüggvénye magában foglalja-e az ideghálózat futtatását az edzésadatokon - ez nem csak a szintetizált program statikus funkciója) . De tehetünk-e jobban?

Bináris ideghálózatok

A macskafelismerő szintézisünk nem nagyon skálázható az ideghálózatban részt vevő számtani és aktiválási funkciók miatt. 8 bites fixpontos aritmetikát használtunk, amelyhez nagy szintû problémakódolások létrehozásához és megoldásához szükséges a szintetizátor kényszermegoldónk. ReLU aktiválást is alkalmaztunk, amelyek köztudottan kóros viselkedést okoznak az SMT megoldók számára.

Kiderült, hogy ezek a kihívások nem egyedülállóak a szintetizátorunk modern gépi tanulási kutatásaival, ugyanazokkal a kérdésekkel néznek szembe. Nagy az érdeklődés az ideghálózatok kvantálása iránt, amelyek során a hálózat számításait nagyon alacsony pontossággal hajtják végre a tárhely és a számítási idő megtakarítása érdekében. A kvantálás legszélsőségesebb formája egy bináris ideghálózat, ahol a súlyok és az aktivációk mindegyike csak egy bit!

Ezeknek a technikáknak jól illeszkedniük kell szintézis alapú képzési megközelítésünkhöz. A kisebb súlyok skálázhatóbbá teszik szintézisünket, lehetővé téve számunkra a nagyobb hálózatok és több képzési példa használatát. Ennek a hipotézisnek a teszteléséhez megpróbáltunk egy XNOR-Net-t kiképezni az MNIST kézzel írott számjegyű osztályozási feladatra. Az XNOR-Net egy bináris neurális hálózati tervezés, amely az aktiválások (vagyis a fenti aktiválási függvényünk) számításának aritmetikáját hatékony bitenkénti műveletekkel helyettesíti. Az új aktiválási függvényünk így néz ki, ahol a bemenetek és a súlyok most már bitvektorok (azaz gépi egész számok), elemenként egy bitdel, nem pedig numerikus elemek listájával:

A popcount függvény egyszerűen megszámolja a bitek számát egy bit-vektorban (az eredményt egy másik bit-vektorként adja vissza). Ez az aktiválási funkció hatékonyabb, mint a szorzat, amely szorzást igényel.

Egy kezdeti kísérlet

Az MNIST adatkészletből vett 100 példa alapján szintetizáltunk egy XNOR-Net osztályozót, 8-8 pixelre csökkentve. Ehhez a kísérlethez kijavítottunk egy 64-32-32-10 ideghálózati topológiát, amely sokkal nagyobb, mint a fenti macskafelismerő. Annak ellenére, hogy arra számítottunk, hogy a kisebb súlyok segítenek a skálázhatóságban, eredményeink elég rosszak voltak: a szintézis eszköz 100% -os pontosságot ért el a kis edzéskészleten, de 7 nap kellett a kiképzéshez! Rosszabb, hogy a tesztkészlet pontossága mélységes 15% volt, alig jobb, mint a véletlenszerű, amikor 10 számjegyet különböztettek meg.

A legnagyobb kérdés itt az, hogy az aktiválási függvényünkben a popcount művelet kódolása drága egy SMT-megoldó számára. Okos bináris trükköket kell használnunk a popcount kódolásához, de ezek drágák és megnehezítik a veszteségfüggvény optimalizálását. Az osztályozás eredményeihez egy forró kódolást is használunk - a hálózat 10 bitet ad ki, ami megfelel az egyes potenciális számok előrejelzéseinek. Ez a kódolás bonyolítja a szintézis eszközünk keresését; a 10 kimeneti bit legtöbb értéke érvénytelen (minden olyan érték, amelyiknek nincs pontosan egy a beállított 10 bitből), így a keresési terület nem eredményes területeit hozza létre.

Hackelés utunk a győzelemhez

Az eredeti XNOR-Net problémáinak megoldása érdekében ostoba csapkodást és engedményt tettünk. Aktiválási függvényünkben a popcountot sokkal naivabb művelettel helyettesítettük. ”Az nn bites xnor értéket felosztottuk a felső és az alsó felére, majd az aktiválás kiszámítja, hogy a felső fél nagyobb-e, mint az alsó fele, amikor a kettőt értelmezzük. n/2 bites gépi egész számokként. Ennek az aktiválási funkciónak nincs okalapja, de mint sok jó aktiválási funkció, ez kényelmes az edzésünk számára is. Ezután a bináris osztályozók képzésére szorítkoztunk, megpróbálva megkülönböztetni a k számjegyet a nem k számjegyektől.

Utolsó kísérletünkhöz 250 példára emeltük az edzéskészlet méretét, a cél k számjegyből 125-t, a többit véletlenszerűen, nem k-ból. Itt van négy különböző bináris osztályozó (négy különböző k számjegyre) teszt-beállított pontossága az edzésidő függvényében:

Minden edzéssor akkor fejeződik be, amikor a szintetizátor bebizonyítja, hogy az edzéskészletnél nincs jobb eredmény ”, más szóval, a végső osztályozó az optimális az adott edzésadatokhoz. A teszt által beállított pontosság mind a négy esetben jobb, mint a véletlenszerű, ami nagy előrelépés az első erőfeszítésünkhöz képest, és egyes osztályozók 75% -os pontosságot kapnak. Számomra a legimpozánsabb, hogy a szintézis idő sokkal alacsonyabb, mint az eredeti 7 nap - mind a négy számjegyből álló osztályozó körülbelül 15 perc múlva a legjobb pontosságához közelít (szintézis standardok szerint ez nagyon jó!).

Mit tanultunk?

Az ideghálózat kiképzése SMT megoldóval nagyon rossz ötlet. Ennek a munkának az az elvonása, hogy ki kell dobnunk a TensorFlow-t, és egy szintézis alapú csővezetékre kell cserélnünk. ”Az MNIST 75% -os pontossága nem valószínű, hogy elnyernénk a legjobb papírdíjakat. Az érdekes ezekben az eredményekben, hogy az általunk használt eszközöket soha nem tervezték ilyesmi szem előtt tartásával, és mégis (egy kis finomhangolással) hiteles eredményeket kaphatunk. A probléma, amely végül megközelítésünket végzi, az edzésadatok: a szintetizátorunknak minden edzésadatot előre be kell látnia, állításként kódolva, és ez gyorsan megoldhatatlan problémaméretekhez vezet.

Azt hiszem, két izgalmas jövőbeli irány lehet a probléma körül. Az egyik az, hogy jobban összpontosítson az ellenőrzésre, mint a Reluplex. Az a tény, hogy egyáltalán bármilyen eredményt elérhetünk ennél a szintézisproblémánál, jót tesz az ellenőrzésnek, ami általában könnyebb az automatizált eszközök számára (az egyik gondolkodásmód az, hogy a szintézis az összes neurális hálózaton keresztül számszerűsít, míg a verifikáció csak egyetlen hálózat). Szintézis-infrastruktúránk még negatív eredmények bizonyítását is lehetővé teszi, mint az XOR-kísérleteink során.

A második irány szintézis technikák alkalmazása a gépi tanulás fokozására. Vannak izgalmas korai eredmények a szintézis felhasználásával értelmezhető programok létrehozására, amelyek leírják a fekete dobozos idegháló viselkedését. Képzett black-box hálózatot figyelembe véve nincs szükség a szintézis fázisra, hogy lássa az összes edzési adatot, ami segít elkerülni a korábban látott méretezési problémákat. Ez a megközelítés egyesíti mind a szintézis, mind a gépi tanulás erősségeit.

Hagyjuk az elfogultsági feltételeket a neurális hálózat megvalósításából, de könnyen hozzá lehetne adni őket

Az ebben a kódban szereplő (let loop ([a b]) expr.) Forma definiálja és azonnal meghívja a rekurzív függvényt; egyenértékű a következővel: (letrec ([hurok (lambda (a) kifejezés)]) (b hurok)) .В ↩