Источник: Nuances of Programming
Расскажем о задачах классификации и регрессии. Данные, модели, условия и Imandra с её возможностями помогать прогнозировать рак и вред от лесных пожаров.
Введение
Проверка параметров изучаемых моделей — сложная задача, но ее важность растет, поскольку нужно убедиться в безопасности, надежности и понятности систем ИИ, использующих эти модели.
Машинное обучение в целом и глубокое обучение в частности— это мощная техника, которая за последнее время показала беспрецедентный успех в широком многообразии задач, часто демонстрируя нечеловеческую эффективность. Тем не менее понимание итоговых моделей и формирование гарантий эффективности с учетом определенных условий ввода или вывода часто становится сложной задачей. Imandra — механизм автоматического мышления общего назначения, предлагающий набор инструментов, которые можно использовать для получения подходящих типов инсайтов и гарантий для широкого ряда алгоритмов.
Обучение с учителем — подраздел машинного обучения, который включает в себя обучение модели с помощью данных, полученных из пар ввода-вывода таким образом, что у нас в распоряжении оказываются новые незнакомые модели ввода.
Обучение с учителем — это подраздел МО, в который входит обучение модели при помощи данных, полученных из пар ввода-вывода, таким образом, что если “скармливать” модели новые неиспользованные данные, она будет способна выдавать подходящий прогноз для вывода. Другими словами, задача — изучить модель, которая аппроксимирует функцию мэппинга ввода на вывод. Для взаимодействия с Imandra мы используем понятный ей язык моделирования IML (Imandra Modelling Language), который основан на дополненном подразделе функционального языка программирования OCaml и позволяет рассуждать о таких функциях в естественной форме.
Чтобы проиллюстрировать такой подход, мы будем рассматривать примеры двух самых популярных задач по обучению с учителем (и в целом по МО): классификация и регрессия. В частности, мы покажем как два самых распространенных типа моделей, которые нужны для обработки задач со случайными лесами и нейронными сетями, можно проанализировать с помощью Imandra. Для каждой задачи мы возьмем реальный эталонный датасет из репозитория по машинному обучению UCI и напишем наши модели на Python с применением некоторых стандартных библиотек МО. Полную версию кода для обеих моделей (обучения и анализа) можно найти на GitHub. Вы также можете просмотреть аналогичный облачный Imandra Jupyter Notebook.
Классификация
В этой задаче мы изучим прогноз отметки данных, основанный на предыдущих маркированных данных. Для классического датасета о раке груди в Висконсине цель состоит в том, чтобы определить, является ли рак доброкачественным или злокачественным на основании характеристик образца клеточных ядер. В датасете у нас будут следующие переменные:
Предварительная обработка данных перед обучением — это обычная практика. Сначала мы стандартизируем каждую переменную для того, чтобы у нас было нулевое среднее арифметическое и единичная дисперсия. Затем мы убираем всё, кроме групп переменных с высокой корреляцией, а также тех, у которых низкий уровень общей информации с целевой переменной.
Данные делим так: 80% для обучения и 20% для тестирования. Мы используем Scikit-Learn для обучения случайного леса с 3-мя деревьями решений (максимальная глубина равна 3), поскольку это относительно простая проблема, что даже такая незамысловатая модель выдаёт достаточно высокую точность. Коротким скриптом на Python каждое дерево конвертируется в IML и может участвовать в мышлении с применением Imandra.
Мы также можем создать свой тип ввода в Imandra для нашей модели, чтобы отслеживать различные параметры данных.
При этом помните, что мы обработали данные перед обучением. Чтобы упростить процесс, мы добавим функцию, применяющую эти преобразования к каждой переменной ввода с помощью дополнительных мультипликативных значений масштабирования, полученных во время предварительной обработки данных. После этого определим полностью сквозную модель, в которой соединяются шаги предварительной обработки и случайный лес.
Так как наша IML-модель полностью выполняемая, мы можем отправлять ей запросы, находить контрпримеры, доказывать свойства, применять дополнительные логические условия, декомпозировать ее поведение по областям и так далее. В качестве быстрой проверки работоспособности мы можем запустить данную величину (которая в этом случае получила маркировку “злокачественной” — malignant) из нашего датасета через модель следующим образом:
Выглядит хорошо. Мы также можем использовать Imandra, чтобы генерировать инстансы и контрпримеры для себя, по возможности добавляя дополнительные логические условия. Их можно определять как функции, которые выводят логические (булевые) значения. По этом Imandra будет возвращать инстансы, которые будучи корректными, могут очень сильно отличаться от любых разумных значений, которые мы могли бы ожидать в реальности. Обычно в первую очередь мы беспокоимся о производительности наших моделей при включении некоторых разумных границ для вводных значений (к примеру, средний радиус не может быть отрицательным, и если значения для этой переменной не выходят из нашего диапазона данных от 6.98 до 28.11, то не стоит ожидать никаких значений, больших, чем, например 35).
Используя описание каждой переменной в информации о датасете выше, мы можем сформировать условие, описывающее корректные и логичные вводные данные для нашей модели. В целом в МО обычно больше внимания уделяется эффективности и качеству модели, чем конкретному распределению данных, насчет которых обычно есть предварительные ожидания.
Наше условие для определения допустимых вводных данных в случайный лес:
Кастомный принтер для создания инстансов десятичной записи:
let pp_approx fmt r = CCFormat.fprintf fmt "%s" (Real.to_string_approx r) [@@program]
Такой подход позволит нам сгенерировать следующую синтетическую точку данных, которую наша модель будет классифицировать как доброкачественную. Затем мы можем получить доступ к нашему инстансу x, выполнить с его помощью вычисления, используя модуль CX (контрпример), и вывести результаты в десятичной нотации при помощи кастомного принтера, который мы определяли выше:
Также можно “размышлять” о нашей модели в более интересных ракурсах, например, проверить валидность определенных ограничений, которым должна соответствовать эта модель. Допустим, если у поверхности ядра клетки много крупных вогнутых секций, то это особенно явный негативный знак того, что рак скорее всего будет злокачественным. Мы можем использовать Imandra, чтобы убедиться, что наша модель всегда классифицирует валидный сэмпл сильно вогнутых клеток как злокачественный:
Imandra доказала, что это свойство соблюдается всегда и для всех возможных введенных значений. Хотя наша модель корректно ведёт себя в таких случаях, при настройке некоторых чисел в проверяемом утверждении, не сложно придумать якобы разумные параметры, которым наша модель не сможет отвечать (увидим это на примере в следующем разделе). Imandra скажет нам не только, когда команда верификации не сработает, а еще укажет на конкретный инстанс, где вводные данные не соответствуют содержимому. В таком случае этот инстанс автоматически попадает в пространство состояний, в котором его уже можно исследовать. Таков один из путей применения Imandra для диагностики проблем с моделями и получении информации об их поведении.
Последняя функция, которую мы рассматриваем в этом разделе, — декомпозиция областей. Эту технику Imandra использует для прерывания потенциально бесконечного вводного пространства в дискретных областях, поверх которых поведение декомпозированной функции остается неизменным.
Вложенные утверждения if ... then ... else о том, как определены деревья (из случайного леса), обозначают, что они первые кандидаты для этой функциональности. Imandra может строить логические описания областей и интерактивные диаграммы Voronoi, чтобы визуализировать поведение алгоритма. Чтобы увидеть, как это работает, загляните в рабочий notebook, а чтобы прочитать её описание, кликните по области:
Мы также можем взять дополнительные условия для декомпозиции области нашей модели с помощью флага ~assuming:. У этого метода есть один прикладной вариант — симуляция частичной наблюдаемости. Предположим, мы знаем большинство измерений отдельного набора клеток и хотим увидеть, что классификация вводных данных зависит от остальных функций. Представим, что есть только измерения вогнутости для образца клеток конкретного пациента, и мы хотим увидеть, как выводные данные нашей модели зависят от значений других функций.
Благодаря уточнению известных значений в дополнительном условии мы получаем интерактивный визуальный инструмент (встроенный в наш Imandra Jupyter Notebook или доступный по автоматически сгенерированной HTML-ссылке), который даст конечный набор возможных выводов и логическое описание для каждого из них.
Регрессия
Решая задачу регрессии, мы хотим научиться прогнозировать значение(я) некоторой(ых) переменной(ых) с учётом данных, полученных ранее. Для популярного датасета лесных пожаров цель состоит в том, чтобы спрогнозировать размер сожженной после лесных пожаров территории в северо-восточной области Португалии. В нём используются метеорологические и прочие данные. Это довольно сложная задача, и пока что нейросети, показанные ниже, не достигают высокого уровня эффективности. При этом мы всё же видим, как можно анализировать относительно простые модели такого типа в Imandra. В датасете у нас есть следующие переменные:
Мы снова проводим обработку данных перед обучением. В первую очередь мы преобразовываем переменные месяца и дня в цифровые значения и применяем синус-преобразование (чтобы аналогичные временные периоды были близки по значению). Также удаляем остатки и применяем приближенное логарифмическое преобразование к области переменной (так рекомендуют в описании датасета). Каждая переменная масштабируется таким образом, чтобы она попала в интервал между 0 и 1. Удаляем те, у которых высокая корреляция и\или низкий уровень общей информации с целевой переменной.
Затем мы разделяем данные на два сета: 80% для тренировки и 20% для тестирования. Будем использовать Keras, чтобы обучить простую нейросеть с прямой связью и одним скрытым слоем (из шести нейронов). А функции активации ReLU и стохастический градиентный спад понадобятся нам для оптимизации среднеквадратической ошибки. Сохраним модель в формате файла .h5 и возьмём короткий скрипт Python, чтобы вытащить нейронную сеть в файл типа IML для его обработки в Imandra.
В первом примере можем определить:
- некоторые кастомные типы данных;
- функции повторения предварительной и пост-обработки данных;
- условие, которое описывает валидные входные данные в модель (из описания датасета, а также некоторые разумные допущения о климате в Португалии).
Условие определения валидных вводных данных для нашей нейросети:
В процессе генерации инстансов со сторонними условиями (такими, как в примере ниже, где мы требуем, чтобы вывод был больше, чем 20 гектаров, температура 20 градусов Цельсия и месяц должен быть май) можно снова вызвать и вычислить модель, проводя автоматическое размышление над результатами в модуле CX. Обратите внимание, что здесь есть наш “принтер” (установленный ранее), который снова конвертирует значения в десятичную нотацию:
Доступные тут виды анализа не отличаются от тех, что мы видели выше в задаче классификации. Не будем повторяться и завершим этот раздел иллюстрацией возможностей Imandra в доказательстве пары полезных свойств нашей сети. Начнем с проверки условия, которое, как мы надеемся, будет соблюдать любая разумная модель прогнозирования для этого задания. Попробуем доказать, что область вывода модели никогда не будет отрицательной:
# verify (fun x -> is_valid_nn x ==> nn_model x >=. 0.0);
;- : nn_input -> bool = <fun>
[✓] Theorem proved.
Отлично! Мы доказали, что если наша нейронная сеть получает валидные данные, то она никогда не будет давать сбои в виде отрицательного числа на выходе. Пусть это и простой пример, но он даёт те гарантии, которые нужны для безопасной разработки подобных моделей в реальном мире. Например, для таких случаев, где выход нейросети может формировать часть управляющей последовательности для контроля беспилотного автомобиля.
Теперь попробуем что-то более амбициозное и проверим свою гипотезу. При прочих равных условиях мы ожидаем, что, чем выше температура, тем большая площадь леса сгорит. Из-за недостатков нашей модели (ограниченность данных, стохастичность при обучении, сложные паттерны в природном физическом феномене и т. д.) это утверждение легко искажается в Imandra. Убедитесь в этом сами:
Получилось достаточно много информации. Однако если углубиться в неё, то можно изучить ключевые части контрпримеров, которые сгенерировала Imandra. Например, мы уже знаем, что вводные данные будут одинаковыми во всех функциях, кроме температуры. Поэтому давайте сразу посмотрим на эти значения, а потом запустим каждый контрпример в модель. Так мы увидим, как она действительно опровергнет нашу гипотезу:
Не всё ещё потеряно. Хотя сеть и не соответствует нашему изначальному утверждению проверки, мы можем ограничить нашу установку, чтобы доказать что-то более простое:
- Поскольку данных о зимних месяцах совсем немного, вряд ли модель сделает достоверное обобщение в этой части. Поэтому мы будем рассматривать все месяцы кроме зимних.
- Увеличим допуск по температуре до 10 градусов Цельсия.
- И аналогично — допуск по сожжённой территории до 25 гектаров.
С учетом этих допущений Imandra вернёт финальное доказательство:
Заключение
Итак, в контексте моделей, изучаемых по данным, мы прошли только один из множества путей использования формальных методов в области МО. А пока эта задача остаётся сложной, поскольку большинству самых современных подходов необходимо узкоспециализированное ПО, техники и методы, которые Imandra пока ещё не поддерживает.
Мы стремимся улучшить способности Imandra, в особенности масштабируемость. При этом есть и другие интересные пути в сфере наших исследований. Например, использование декомпозиции области для повышения эффективности выборки в процессе глубокого обучения с подкреплением.
Если вам интересно разобраться с такими вопросами, то заглядывайте в другие рабочие ноутбуки, читайте и получайте обновления с нашего сайта на почту. Подтягивайте английский и участвуйте в обсуждении на канале Discord.
Читайте также:
Читайте нас в телеграмме и vk
Перевод статьи Lewis Hammond: Analysing Machine Learning Models with Imandra
