Можете ли да обучите невронна мрежа с помощта на SMT решател?

2 август 2018 г.

Да, и аз го направих, но не би трябвало.

обучите

Освен ако досега не сте живели под скала, знаете, че машинното обучение прекроява компютърните науки. Една от собствените ми области на изследване, синтез на програми - идеята, че можем автоматично да генерираме програма от спецификация на това, което тя трябва да прави - не е имунизирана.

Машинното обучение и програмният синтез са поразително сходни. Можем да оформим синтеза на програмата като проблем с машинно обучение: да намерим някои параметри (синтаксис на програмата) за модел (семантика на програмата), които минимизират функцията на загуба (коректност на програмата). Много от най-вълнуващите скорошни резултати в изследванията на програмния синтез използват това наблюдение, прилагайки техники за машинно обучение, за да увеличат и дори да заменят традиционните алгоритми за синтез. Подходите за машинно обучение са особено подходящи за например базиран синтез, при който спецификацията е набор от примери за вход-изход, които трябва да удовлетворява синтезираната програма.

Но приликите протичат и по двата начина - машинното обучение може да се разглежда като проблем за синтез на програма, при който се опитваме да запълним някои дупки (тежести) в скица (модел), за да задоволим спецификация (минимални загуби). Можем ли да използваме техники за синтез на програми за машинно обучение? Тази посока е криминално недостатъчно проучена в литературата, затова си помислих, че ще пробвам като част от проект за клас.

Машинно обучение с помощта на програмния синтез

Инструментите за синтез са най-запознати с работата ми чрез решаване на логически ограничения с помощта на SMT решател. За да направим машинно обучение, използвайки синтез на програми, ние ще кодираме проблема с машинното обучение като проблем на синтеза и ще решим възникналите логически ограничения.

Защо да пробваме този подход, когато градиентното спускане и подобните му работи толкова добре за обучение на големи модели за машинно обучение? Мисля, че има четири потенциални силни страни за синтез:

Разбира се, има и някои значителни предизвикателства. Най-видната ще бъде мащабируемостта - съвременните модели за дълбоко обучение са гигантски както по отношение на данните за обучение (милиони примери, всеки с хиляди измерения), така и по размер на модела (милиони тежести за учене). За разлика от това, изследването на програмния синтез обикновено се занимава с програми от порядъка на десетки или стотици операции, с компактни спецификации. Това е голяма разлика за преодоляване.

Как да тренирам модел, използвайки синтез

Ще се съсредоточим върху обучението (напълно свързани) невронни мрежи в тази публикация, защото в момента те са много яростни. За да обучим невронна мрежа, използвайки синтез, ние прилагаме скица, която описва прякото преминаване (т.е. изчисляване на изхода на мрежата за даден вход), но използвайки дупки (обозначени с ?) за тежестите (които ще попитаме синтезатора, който да се опита да попълни):

Ще внедрим нашия синтезатор на невронни мрежи в Розет. Внедряването на предаването напред изисква само да опишем активирането на един неврон - изчисляване на точковото произведение на входовете и тежестите и след това прилагане на функция за активиране на ReLU:

Сега можем да изчислим активациите за цял слой 1:

И накрая, изчислете изхода на цялата мрежа, като се имат предвид нейните входове:

Синтезира XOR. Функцията XOR е каноничният пример за необходимостта от скрити слоеве в невронна мрежа. Скритият слой дава на мрежата достатъчно свобода да научи такива нелинейни функции. Нека използваме нашата проста реализация на невронна мрежа, за да синтезираме XOR.

Първо, трябва да създадем скица за желана топология на невронната мрежа. За всеки слой създаваме матрица от неизвестни (цели числа) тегла с подходящ размер:

Добре известно е, че мрежа с топология 2-2-1 (т.е. 2 входа, един скрит слой от 2 неврона, 1 изход) е достатъчна, за да научи XOR, така че нека създадем скица на тази форма и след това твърдете, че мрежата прилага XOR:

И накрая, можем да помолим Розет да реши този проблем:

Резултатът е модел, даващ стойности за нашите тегла, който можем да проверим, използвайки оценка:

произвежда тежести:

или във визуална форма:

Също така можем да използваме нашата инфраструктура за доказване на свойства за невронни мрежи. Например можем да докажем твърдението, което направихме по-горе, че не е възможно да се научи мрежа за XOR без скрит слой. Чрез промяна на дефиницията на скицата, за да изключите скрития слой:

и опитвайки синтеза отново, откриваме, че М е незадоволително решение; с други думи, няма присвояване на (целочислени) тежести на тази топология, която правилно прилага XOR.

Обучение на разпознавател на котки

Нека преминем от XOR към може би най-важния проблем на компютърните науки в нашето време: разпознаване на снимки на котки. Разпознаването на изображения ще подчертае нашия синтезиран базов тръбопровод по няколко начина. Първо, изображенията са много по-големи от еднобитовите входове на XOR - хиляди пиксели, всеки с три 8-битови цветни канала. Ще ни трябват и много повече примери за обучение от четирите, които използвахме за XOR. И накрая, ще искаме да изследваме по-големи топологии от обикновената за нашата невронна мрежа XOR.

Оптимизация и синтез

В нашия XOR пример ние търсихме перфектна невронна мрежа, която да е правилна за всички наши обучения. За класификация на изображенията е малко вероятно да успеем да намерим такава мрежа. Вместо това ще искаме да сведем до минимум някои функции за загуби, улавящи грешките в класификацията, които прави мрежата кандидат. Това прави проблема със синтеза ни количествен: намерете решението, което минимизира функцията на загубите.

Има сложни начини за решаване на количествен проблем със синтеза, но според моя опит следващото наивно решение може да бъде изненадващо ефективно. Като пример, да предположим, че искаме да разрешим класически проблем с опаковането на контейнери: имаме пет обекта с тежести a, b, c, d и e и трябва да опаковаме колкото се може повече в торба, без да надвишаваме ограничението за тегло T Ще създадем символни булеви променливи, за да посочим дали всеки обект е опакован и да определим съответните им тегла:

Сега дефинираме функция за разходи, която да оптимизираме, като ни казва общото тегло на всичко, което сме опаковали:

За да намерим оптималния набор от обекти, които да включим, първо намираме първоначален набор и след това рекурсивно молим решаващия да намери по-добро решение, докато вече не може да го направи: 2

Изпълнението на този пример с T, зададено на 80, ни дава следния изход:

Открихме три решения, на разходи 60, 70 и 75. Оптималното решение включва обекти a, b и e, с общо тегло 75.

Разпознаване на котки с мета скици

Като част от оценката в нашата статия за POPL 2016, ние синтезирахме невронна мрежа, която беше прост двоичен класификатор за разпознаване на котки, използвайки същата техника за оптимизация, както по-горе. Използвахме нашата абстракция на metasketch, въведена в тази статия, за да извършим търсене в мрежа по възможни топологии на невронната мрежа. Данните ни за обучение бяха 40 примера, извлечени от набора от данни CIFAR-10 - 20 снимки на котки и 20 снимки на самолети, всяка от които 32 32 - 32 цветни пиксела.

Тъй като използването на такъв малък тренировъчен комплект с ниска разделителна способност не беше достатъчна отстъпка за мащабируемост, намалихме образците на тренировъчните изображения до 8Г-8 сиви скали.

След 35 минути обучение, нашият инструмент за синтез генерира невронна мрежа, която постигна 95% точност на примерите за обучение. Той също така доказа, че по-нататъшните подобрения на точността на тренировъчния набор са невъзможни: никаква промяна в топологията на мрежата (до границите на търсенето на мрежата) или тежестите не може да подобри точността на обученията. Точността на зададените тестове беше много по-лоша, както очаквахме само с 40 примера.

Очевидно този резултат няма да направи революция в областта на машинното обучение. Нашата цел при провеждането на този експеримент беше да покажем, че мета скиците могат да решават сложни разходни функции (обърнете внимание как разходната функция за синтезиране на невронна мрежа включва изпълнението на невронната мрежа върху данните за обучение - това не е просто статична функция на синтезираната програма) . Но можем ли да се справим по-добре?

Бинарни невронни мрежи

Синтезът ни за разпознаване на котки не се мащабира много добре поради аритметичните и активиращите функции, включени в невронната мрежа. Използвахме 8-битова аритметика с фиксирана точка, която изисква ограничителният инструмент на нашия синтезатор да генерира и решава кодиране на големи проблеми. Също така използвахме активирания на ReLU, за които е известно, че причиняват патологично поведение на SMT решавателите.

Оказва се, че тези предизвикателства не са уникални за нашия синтезатор - съвременните изследвания на машинното обучение са изправени пред същите проблеми. Има голям интерес към квантуването на невронни мрежи, при което изчисленията на мрежата се извършват с много ниска точност, за да се спести място за съхранение и време за изчисление. Най-екстремната форма на квантуване е двоична невронна мрежа, където теглата и активациите са само един бит!

Тези техники трябва да са подходящи за нашия подход, основан на синтеза на обучение. По-малките тегла правят нашия синтез по-мащабируем, което ни позволява да използваме по-големи мрежи и повече примери за обучение. За да проверим тази хипотеза, ние се опитахме да обучим XNOR-Net за задачата за класификация на ръкописни цифри MNIST. XNOR-Net е двоичен дизайн на невронна мрежа, който замества аритметиката за изчислителни активирания (т.е. нашата функция за активиране по-горе) с ефективни битови операции. Новата ни функция за активиране изглежда така, където входовете и теглото вече са битови вектори (т.е. машинни числа) с по един бит на елемент, а не списъци с числови елементи:

Функцията popcount просто отчита броя на битовете в битов вектор (връща резултата като друг битов вектор). Тази функция за активиране е по-ефективна от точков продукт, който изисква умножение.

Първоначален експеримент

Ние синтезирахме XNOR-Net класификатор от 100 примера, извлечени от набора от данни MNIST, дескретизирани до 8Г — 8 пиксела. За този експеримент фиксирахме 64-32-32-10 топология на невронната мрежа, много по-голяма от горната разпознавателна котка. Въпреки че очаквахме по-малките тежести да помогнат за мащабируемост, резултатите ни бяха доста лоши: инструментът за синтез постигна 100% точност на малкия набор от тренировки, но отне 7 дни, за да тренира! По-лошото е, че точността му на тестов набор беше ужасните 15%, едва по-добра от случайната при разграничаване на 10 цифри.

Най-големият проблем тук е, че кодирането на операцията popcount в нашата функция за активиране е скъпо за SMT решател. Трябва да използваме умни двоични трикове, за да кодираме popcount, но те са скъпи и затрудняват оптимизирането на функцията ни за загуби. Използваме и едно горещо кодиране за резултатите от класификацията - мрежата извежда 10 бита, съответстващи на прогнозите за всяка потенциална цифра. Това кодиране усложнява търсенето на нашия инструмент за синтез; най-възможните стойности на 10-те изходни бита са невалидни (всяка стойност, която няма точно един от 10-те бита), създавайки области от пространството за търсене, които не са плодотворни.

Хакване на пътя ни към победата

За да разрешим проблемите с нашия първоначален XNOR-Net, направихме глупав хак и отстъпка. Заменихме popcount в нашата функция за активиране с много по-наивна операция - разделихме n-битовата стойност xnor на горната и долната половина и след това активирането изчислява дали горната половина е по-голяма от долната половина, когато двете се интерпретират като n/2-битови машинни числа. Тази функция за активиране няма основание за разум, но като много добри функции за активиране е удобна за нашето обучение. След това се ограничихме да обучаваме двоични класификатори, опитвайки се да разграничим цифра k от цифри, които не са k.

За нашия последен експеримент увеличихме размера на обученията до 250 примера, 125 от целевата цифра k, а останалите бяха изтеглени произволно от цифри, различни от k. Ето точно зададената от теста точност на четири различни двоични класификатора (за четири различни цифри k) като функция от времето за обучение:

Всяка тренировъчна линия завършва, когато синтезаторът докаже, че не е възможен по-добър резултат за тренировъчния набор - с други думи, крайният класификатор е оптималният за дадените тренировъчни данни. Точността на зададените тестове е по-добра от случайната във всичките четири случая, което е голямо подобрение спрямо нашите първи усилия и някои класификатори получават над 75% точност. Най-впечатляващото за мен е, че времето за синтез е много по-ниско от първоначалните 7 дни - всички четирицифрени класификатори се доближават до най-добрата си точност след около 15 минути (това е доста добро според стандартите за синтез!).

Какво научихме?

Обучението на невронна мрежа с SMT решател е много лоша идея. Вземането от тази работа не е, че трябва да изхвърлим TensorFlow и да го заменим със синтетичен конвейер - 75% точност на MNIST едва ли ще ни спечели награди за най-добра хартия. Интересното при тези резултати е, че инструментите, които използваме, никога не са проектирани с нещо подобно и въпреки това (с малко фина настройка) можем да получим достоверни резултати. Проблемът, който в крайна сметка обрича нашия подход, са данните за обучение: нашият синтезатор трябва да вижда предварително всички данни за обучение, кодирани като твърдения и това бързо води до неразрешими размери на проблема.

Мисля, че има две вълнуващи бъдещи насоки, които могат да заобиколят този проблем. Единият е да се съсредоточим повече върху проверката, както прави Reluplex. Фактът, че можем изобщо да получим някакви резултати за този проблем със синтеза, е добър за проверка, която обикновено е по-лесна за автоматизираните инструменти (един от начините да се мисли за това е, че синтезът количествено определя всички невронни мрежи, докато проверката се грижи само за една мрежа). Нашата синтезна инфраструктура дори ни позволява да доказваме отрицателни резултати, както в нашите XOR експерименти.

Втората посока е да се използват техники за синтез, за ​​да се увеличи машинното обучение. Има някои вълнуващи ранни резултати при използването на синтез за генериране на интерпретируеми програми за описване на поведението на невронна мрежа с черна кутия. Като се има предвид обучена мрежа за черна кутия, няма нужда фазата на синтез да вижда всички данни за обучение, което помага да се избегнат проблемите с мащабирането, които видяхме по-рано. Този подход съчетава силните страни както на синтеза, така и на машинното обучение.

Пропускаме пристрастни термини от внедряването на нашата невронна мрежа, но те биха били лесни за добавяне.

Формата (let loop ([a b]) expr.) В този код определя и незабавно извиква рекурсивна функция; това е еквивалентно на (letrec ([loop (lambda (a) expr.)]]) (loop b)).