Анализ моделей машинного обучения при помощи Imandra
Расскажем о задачах классификации и регрессии. Данные, модели, условия и Imandra с её возможностями помогать прогнозировать рак и вред от лесных пожаров.
Введение
Проверка параметров изучаемых моделей — сложная задача, но ее важность растет, поскольку нужно убедиться в безопасности, надежности и понятности систем ИИ, использующих эти модели.
Машинное обучение в целом и глубокое обучение в частности— это мощная техника, которая за последнее время показала беспрецедентный успех в широком многообразии задач, часто демонстрируя нечеловеческую эффективность. Тем не менее понимание итоговых моделей и формирование гарантий эффективности с учетом определенных условий ввода или вывода часто становится сложной задачей. Imandra — механизм автоматического мышления общего назначения, предлагающий набор инструментов, которые можно использовать для получения подходящих типов инсайтов и гарантий для широкого ряда алгоритмов.
Обучение с учителем — подраздел машинного обучения, который включает в себя обучение модели с помощью данных, полученных из пар ввода-вывода таким образом, что у нас в распоряжении оказываются новые незнакомые модели ввода.
Обучение с учителем — это подраздел МО, в который входит обучение модели при помощи данных, полученных из пар ввода-вывода, таким образом, что если “скармливать” модели новые неиспользованные данные, она будет способна выдавать подходящий прогноз для вывода. Другими словами, задача — изучить модель, которая аппроксимирует функцию мэппинга ввода на вывод. Для взаимодействия с Imandra мы используем понятный ей язык моделирования IML (Imandra Modelling Language), который основан на дополненном подразделе функционального языка программирования OCaml и позволяет рассуждать о таких функциях в естественной форме.
Чтобы проиллюстрировать такой подход, мы будем рассматривать примеры двух самых популярных задач по обучению с учителем (и в целом по МО): классификация и регрессия. В частности, мы покажем как два самых распространенных типа моделей, которые нужны для обработки задач со случайными лесами и нейронными сетями, можно проанализировать с помощью Imandra. Для каждой задачи мы возьмем реальный эталонный датасет из репозитория по машинному обучению UCI и напишем наши модели на Python с применением некоторых стандартных библиотек МО. Полную версию кода для обеих моделей (обучения и анализа) можно найти на GitHub. Вы также можете просмотреть аналогичный облачный Imandra Jupyter Notebook.
Классификация
В этой задаче мы изучим прогноз отметки данных, основанный на предыдущих маркированных данных. Для классического датасета о раке груди в Висконсине цель состоит в том, чтобы определить, является ли рак доброкачественным или злокачественным на основании характеристик образца клеточных ядер. В датасете у нас будут следующие переменные:
1. ID number — идентификационный номер;
2. Diagnosis (malignant or benign) — диагноз (злокачественная или доброкачественная опухоль);
3–32. Действительные значения среднего арифметического и стандартной ошибки, а также самое "худшее" значение для ядра каждой клетки;
a) Radius — радиус;
b) Texture — строение;
c) Perimeter — периметр;
d) Area - область;
e) Smoothness — сглаженность;
f) Compactness — компактность;
g) Concavity — вогнутость;
h) Concave points — точки вогнутости;
i) Symmetry — симметрия;
j) Fractal dimension — фрактальное измерение.
Предварительная обработка данных перед обучением — это обычная практика. Сначала мы стандартизируем каждую переменную для того, чтобы у нас было нулевое среднее арифметическое и единичная дисперсия. Затем мы убираем всё, кроме групп переменных с высокой корреляцией, а также тех, у которых низкий уровень общей информации с целевой переменной.
Данные делим так: 80% для обучения и 20% для тестирования. Мы используем Scikit-Learn для обучения случайного леса с 3-мя деревьями решений (максимальная глубина равна 3), поскольку это относительно простая проблема, что даже такая незамысловатая модель выдаёт достаточно высокую точность. Коротким скриптом на Python каждое дерево конвертируется в IML и может участвовать в мышлении с применением Imandra.
/IML-ВЕРСИЯ КЛАССИФИКАТОРА СЛУЧАЙНОГО ЛЕСА
let tree_0 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
if f_2 <=. (-0.10815) then
if f_0 <=. (0.26348) then
if f_6 <=. (-0.06176) then
(236.0, 1.0)
else
(17.0, 5.0)
else
if f_3 <=. (-0.54236) then
(8.0, 2.0)
else
(3.0, 7.0)
else
if f_6 <=. (0.09812) then
if f_6 <=. (-0.17063) then
(24.0, 0.0)
else
(4.0, 2.0)
else
if f_2 <=. (2.65413) then
(6.0, 128.0)
else
(7.0, 5.0)
let tree_1 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
if f_5 <=. (-0.05799) then
if f_0 <=. (0.68524) then
if f_1 <=. (-0.83180) then
(110.0, 3.0)
else
(137.0, 0.0)
else
if f_3 <=. (0.45504) then
(1.0, 8.0)
else
(0.0, 7.0)
else
if f_0 <=. (-0.18668) then
if f_6 <=. (0.45214) then
(39.0, 0.0)
else
(2.0, 11.0)
else
if f_6 <=. (-0.00009) then
(8.0, 4.0)
else
(5.0, 120.0)
let tree_2 f_0 f_1 f_2 f_3 f_4 f_5 f_6 = let open Real in
if f_2 <=. (0.10459) then
if f_5 <=. (-0.38015) then
if f_5 <=. (-0.60659) then
(139.0, 1.0)
else
(44.0, 3.0)
else
if f_6 <=. (-0.07927) then
(38.0, 2.0)
else
(25.0, 17.0)
else
if f_6 <=. (0.46888) then
if f_3 <=. (0.41642) then
(28.0, 3.0)
else
(1.0, 4.0)
else
if f_2 <=. (1.74327) then
(3.0, 122.0)
else
(4.0, 21.0)
let rf (f_0, f_1, f_2, f_3, f_4, f_5, f_6) = let open Real in
let (a_0, b_0) = tree_0 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_1, b_1) = tree_1 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_2, b_2) = tree_2 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let a = a_0 + a_1 + a_2 in
let b = b_0 + b_1 + b_2 in
(a, b)
Мы также можем создать свой тип ввода в Imandra для нашей модели, чтобы отслеживать различные параметры данных.
При этом помните, что мы обработали данные перед обучением. Чтобы упростить процесс, мы добавим функцию, применяющую эти преобразования к каждой переменной ввода с помощью дополнительных мультипликативных значений масштабирования, полученных во время предварительной обработки данных. После этого определим полностью сквозную модель, в которой соединяются шаги предварительной обработки и случайный лес.
/Тип ввода и функции предварительной обработки используются для определения целостной модели.
type rf_input = {
radius_mean : real;
compactness_mean : real;
concavity_mean : real;
radius_se : real;
compactness_worst : real;
concavity_worst : real;
concave_points_worst : real
}
let process_rf_input input = let open Real in
let f_0 = (input.radius_mean - 14.12729) / 3.52405 in
let f_1 = (input.compactness_mean - 0.10434) / 0.05281 in
let f_2 = (input.concavity_mean - 0.08880) / 0.07972 in
let f_3 = (input.radius_se - 0.40517) / 0.27731 in
let f_4 = (input.compactness_worst - 0.25427) / 0.15734 in
let f_5 = (input.concavity_worst - 0.27219) / 0.20862 in
let f_6 = (input.concave_points_worst - 0.11461) / 0.06573 in
(f_0, f_1, f_2, f_3, f_4, f_5, f_6)
let process_rf_output (a, b) =
if a >. b then "benign" else "malignant"
let rf_model input = input |> process_rf_input |> rf |> process_rf_output
Так как наша IML-модель полностью выполняемая, мы можем отправлять ей запросы, находить контрпримеры, доказывать свойства, применять дополнительные логические условия, декомпозировать ее поведение по областям и так далее. В качестве быстрой проверки работоспособности мы можем запустить данную величину (которая в этом случае получила маркировку “злокачественной” — malignant) из нашего датасета через модель следующим образом:
# rf_model {radius_mean = 17.99;
compactness_mean = 0.2776;
concavity_mean = 0.3001;
radius_se = 1.095;
compactness_worst = 0.6656;
concavity_worst = 0.7119;
concave_points_worst = 0.7119};;- :
string = "malignant"
Выглядит хорошо. Мы также можем использовать Imandra, чтобы генерировать инстансы и контрпримеры для себя, по возможности добавляя дополнительные логические условия. Их можно определять как функции, которые выводят логические (булевые) значения. По этом Imandra будет возвращать инстансы, которые будучи корректными, могут очень сильно отличаться от любых разумных значений, которые мы могли бы ожидать в реальности. Обычно в первую очередь мы беспокоимся о производительности наших моделей при включении некоторых разумных границ для вводных значений (к примеру, средний радиус не может быть отрицательным, и если значения для этой переменной не выходят из нашего диапазона данных от 6.98 до 28.11, то не стоит ожидать никаких значений, больших, чем, например 35).
Используя описание каждой переменной в информации о датасете выше, мы можем сформировать условие, описывающее корректные и логичные вводные данные для нашей модели. В целом в МО обычно больше внимания уделяется эффективности и качеству модели, чем конкретному распределению данных, насчет которых обычно есть предварительные ожидания.
Наше условие для определения допустимых вводных данных в случайный лес:
let is_valid_rf input =
5.0 <=. input.radius_mean && input.radius_mean <=. 35.0 &&
0.0 <=. input.compactness_mean && input.compactness_mean <=. 0.4 &&
0.0 <=. input.concavity_mean && input.concavity_mean <=. 0.5 &&
0.0 <=. input.radius_se && input.radius_se <=. 3.5 &&
0.0 <=. input.compactness_worst && input.compactness_worst <=. 1.2 &&
0.0 <=. input.concavity_worst && input.concavity_worst <=. 1.5 &&
0.0 <=. input.concave_points_worst && input.concave_points_worst <=. 0.35
Кастомный принтер для создания инстансов десятичной записи:
let pp_approx fmt r = CCFormat.fprintf fmt "%s" (Real.to_string_approx r) [@@program]Такой подход позволит нам сгенерировать следующую синтетическую точку данных, которую наша модель будет классифицировать как доброкачественную. Затем мы можем получить доступ к нашему инстансу x, выполнить с его помощью вычисления, используя модуль CX (контрпример), и вывести результаты в десятичной нотации при помощи кастомного принтера, который мы определяли выше:
# instance (fun x -> rf_model x = "benign" && is_valid_rf x);;
- : rf_input -> bool = <fun>
Instance (after 0 steps, 0.021s):
let (x : rf_input) =
{radius_mean = (Real.mk_of_string
"28061993138323/5000000000000");
compactness_mean = (Real.mk_of_string
"8487976201/5000000000000");
concavity_mean = (Real.mk_of_string
"162320931909/2500000000000");
radius_se = (Real.mk_of_string
"40971/20000");
compactness_worst = (Real.mk_of_string
"321/5000");
concavity_worst = (Real.mk_of_string
"415811319441/25000000000000");
concave_points_worst = (Real.mk_of_string
"3877904791/781250000000")}
[✔] Instance found.
module CX : sig val x : rf_input end
# #install_printer pp_approx;;
# CX.x;;- : rf_input = {radius_mean = 5.61239862766;
compactness_mean = 0.0016975952402;
concavity_mean = 0.0649283727636;
radius_se = 2.04855;
compactness_worst = 0.0642;
concavity_worst = 0.0166324527776;
concave_points_worst = 0.00496371813248}
Также можно “размышлять” о нашей модели в более интересных ракурсах, например, проверить валидность определенных ограничений, которым должна соответствовать эта модель. Допустим, если у поверхности ядра клетки много крупных вогнутых секций, то это особенно явный негативный знак того, что рак скорее всего будет злокачественным. Мы можем использовать Imandra, чтобы убедиться, что наша модель всегда классифицирует валидный сэмпл сильно вогнутых клеток как злокачественный:
# verify (fun x ->
is_valid_rf x &&
x.concavity_mean >=. 0.4 &&
x.concavity_worst >=. 1.0 &&
x.concave_points_worst >=. 0.25 ==>
rf_model x = "malignant");;
- : rf_input -> bool = <fun>
[✓] Theorem proved.
Imandra доказала, что это свойство соблюдается всегда и для всех возможных введенных значений. Хотя наша модель корректно ведёт себя в таких случаях, при настройке некоторых чисел в проверяемом утверждении, не сложно придумать якобы разумные параметры, которым наша модель не сможет отвечать (увидим это на примере в следующем разделе). Imandra скажет нам не только, когда команда верификации не сработает, а еще укажет на конкретный инстанс, где вводные данные не соответствуют содержимому. В таком случае этот инстанс автоматически попадает в пространство состояний, в котором его уже можно исследовать. Таков один из путей применения Imandra для диагностики проблем с моделями и получении информации об их поведении.
Последняя функция, которую мы рассматриваем в этом разделе, — декомпозиция областей. Эту технику Imandra использует для прерывания потенциально бесконечного вводного пространства в дискретных областях, поверх которых поведение декомпозированной функции остается неизменным.
Вложенные утверждения if ... then ... else о том, как определены деревья (из случайного леса), обозначают, что они первые кандидаты для этой функциональности. Imandra может строить логические описания областей и интерактивные диаграммы Voronoi, чтобы визуализировать поведение алгоритма. Чтобы увидеть, как это работает, загляните в рабочий notebook, а чтобы прочитать её описание, кликните по области:
Мы также можем взять дополнительные условия для декомпозиции области нашей модели с помощью флага ~assuming:. У этого метода есть один прикладной вариант — симуляция частичной наблюдаемости. Предположим, мы знаем большинство измерений отдельного набора клеток и хотим увидеть, что классификация вводных данных зависит от остальных функций. Представим, что есть только измерения вогнутости для образца клеток конкретного пациента, и мы хотим увидеть, как выводные данные нашей модели зависят от значений других функций.
/Условие описывает наши частичные наблюдения
let partial_observation x =
is_valid_rf x &&
x.concavity_mean = 0.04295 &&
x.concavity_worst = 0.26000 &&
x.concave_points_worst = 0.11460
Благодаря уточнению известных значений в дополнительном условии мы получаем интерактивный визуальный инструмент (встроенный в наш Imandra Jupyter Notebook или доступный по автоматически сгенерированной HTML-ссылке), который даст конечный набор возможных выводов и логическое описание для каждого из них.
#install_printer Imandra_voronoi.Voronoi.print;;
Decompose.top
~ctx_asm_simp:true
~assuming:"partial_observation"
"rf_model" [@@program];;
9 regions computed.
- : Imandra_interactive.Decompose.t list =
Open:
file:////var/folders/l9/d5spnx9177v53nkbpjl4f0yr0000gs/T/voronoi_ee639a.html
Регрессия
Решая задачу регрессии, мы хотим научиться прогнозировать значение(я) некоторой(ых) переменной(ых) с учётом данных, полученных ранее. Для популярного датасета лесных пожаров цель состоит в том, чтобы спрогнозировать размер сожженной после лесных пожаров территории в северо-восточной области Португалии. В нём используются метеорологические и прочие данные. Это довольно сложная задача, и пока что нейросети, показанные ниже, не достигают высокого уровня эффективности. При этом мы всё же видим, как можно анализировать относительно простые модели такого типа в Imandra. В датасете у нас есть следующие переменные:
1. X-axis spatial coordinate (within the Montesinho park map)- координаты пространства по оси Х.
2. Y-axis spatial coordinate (within the Montesinho park map)- координаты пространства по оси Y.
3. Month - месяц.
4. Day - день.
5. FFMC index (from the FWI (Forest Fire Weather Index) system)- Fine Fuel Moisture Code (показатель вероятности возгорания).
6. DMC index (from the FWI system)- The Duff Moisture Code (уровень влажности).
7. DC index (from the FWI system)- The Drought Code (уровень засухи).
8. ISI index (from the FWI system) - Initial Spread Index (показатель распределения).
9. Temperature - температура.
10. Relative percentage humidity - относительная влажность.
11. Wind speed - скорость ветра.
12. Rainfall - ливни.
13. Area of forest burnt - область сожженного леса.
Мы снова проводим обработку данных перед обучением. В первую очередь мы преобразовываем переменные месяца и дня в цифровые значения и применяем синус-преобразование (чтобы аналогичные временные периоды были близки по значению). Также удаляем остатки и применяем приближенное логарифмическое преобразование к области переменной (так рекомендуют в описании датасета). Каждая переменная масштабируется таким образом, чтобы она попала в интервал между 0 и 1. Удаляем те, у которых высокая корреляция и\или низкий уровень общей информации с целевой переменной.
Затем мы разделяем данные на два сета: 80% для тренировки и 20% для тестирования. Будем использовать Keras, чтобы обучить простую нейросеть с прямой связью и одним скрытым слоем (из шести нейронов). А функции активации ReLU и стохастический градиентный спад понадобятся нам для оптимизации среднеквадратической ошибки. Сохраним модель в формате файла .h5 и возьмём короткий скрипт Python, чтобы вытащить нейронную сеть в файл типа IML для его обработки в Imandra.
/IML-версия нейронной сети
let relu x = Real.(if x > 0.0 then x else 0.0)
let linear x = Real.(x)
let layer_0 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
let y_0 = relu @@ (0.20124)*x_0 + (-0.15722)*x_1 + (-0.19063)*x_2 + (-0.54562)*x_3 + (0.03425)*x_4 + (0.50104)*x_5 + -0.02768 in
let y_1 = relu @@ (0.29103)*x_0 + (0.03180)*x_1 + (-0.16336)*x_2 + (0.17919)*x_3 + (0.32971)*x_4 + (-0.43206)*x_5 + -0.02620 in
let y_2 = relu @@ (0.66419)*x_0 + (0.25399)*x_1 + (0.00449)*x_2 + (0.03841)*x_3 + (-0.51482)*x_4 + (0.58299)*x_5 + 0.11858 in
let y_3 = relu @@ (0.47598)*x_0 + (-0.36142)*x_1 + (0.38981)*x_2 + (0.27632)*x_3 + (-0.61231)*x_4 + (-0.03662)*x_5 + -0.02890 in
let y_4 = relu @@ (0.10277)*x_0 + (-0.28841)*x_1 + (0.04637)*x_2 + (0.28808)*x_3 + (0.05957)*x_4 + (-0.22041)*x_5 + 0.18270 in
let y_5 = relu @@ (0.55604)*x_0 + (-0.04015)*x_1 + (0.10557)*x_2 + (0.60757)*x_3 + (-0.32314)*x_4 + (0.47933)*x_5 + -0.24876 in
(y_0, y_1, y_2, y_3, y_4, y_5)
let layer_1 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
let y_0 = linear @@ (0.28248)*x_0 + (-0.25208)*x_1 + (-0.50075)*x_2 + (-0.07092)*x_3 + (-0.43189)*x_4 + (0.60065)*x_5 + 0.47136 in
(y_0)
let nn (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
(x_0, x_1, x_2, x_3, x_4, x_5) |> layer_0 |> layer_1
В первом примере можем определить:
- некоторые кастомные типы данных;
- функции повторения предварительной и пост-обработки данных;
- условие, которое описывает валидные входные данные в модель (из описания датасета, а также некоторые разумные допущения о климате в Португалии).
/Кастомные типы вводных данных и функции для предварительной и пост-обработки
type month = Jan | Feb | Mar | Apr | May | Jun| Jul | Aug | Sep | Oct | Nov | Dec
type day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
type nn_input = {
month : month;
day : day;
dmc : real;
temp : real;
rh : real;
rain : real
}
let month_2_num month = let open Real in function
| Jan -> 0.134
| Feb -> 0.500
| Mar -> 1.000
| Apr -> 1.500
| May -> 1.866
| Jun -> 2.000
| Jul -> 1.866
| Aug -> 1.500
| Sep -> 1.000
| Oct -> 0.500
| Nov -> 0.133
| Dec -> 0.000
let day_2_num day = let open Real in function
| Mon -> 0.377
| Tue -> 1.223
| Wed -> 1.901
| Thu -> 1.901
| Fri -> 1.223
| Sat -> 0.377
| Sun -> 0.000
let process_nn_input input = let open Real in
let real_month = month_2_num input.month in
let real_day = day_2_num input.day in
let x_0 = (real_month - 0.0) / (2.0 - 0.0) in
let x_1 = (real_day - 0.0) / (1.901 - 0.0) in
let x_2 = (input.dmc - 1.1) / (291.3 - 1.1) in
let x_3 = (input.temp - 2.2) / (33.3 - 2.2) in
let x_4 = (input.rh - 15.0) / (100.0 - 15.0) in
let x_5 = (input.rain - 0.0) / (6.40 - 0.0) in
(x_0, x_1, x_2, x_3, x_4, x_5)
let process_nn_output y_0 = let open Real in
let y = 4.44323 * y_0 in
if y <= 1.0 then (y - 0.00000) * 1.71828 else
if y <= 2.0 then (y - 0.63212) * 4.67077 else
if y <= 3.0 then (y - 1.49679) * 12.69648 else
if y <= 4.0 then (y - 2.44700) * 34.51261 else
(y - 3.42868) * 93.81501
let nn_model input = input |> process_nn_input |> nn |> process_nn_output
Условие определения валидных вводных данных для нашей нейросети:
let is_valid_nn input =
0.0 <=. input.dmc && input.dmc <=. 500.0 &&
0.0 <=. input.temp && input.temp <=. 40.0 &&
0.0 <=. input.rh && input.rh <=. 100.0 &&
0.0 <=. input.rain && input.rain <=. 15.0
В процессе генерации инстансов со сторонними условиями (такими, как в примере ниже, где мы требуем, чтобы вывод был больше, чем 20 гектаров, температура 20 градусов Цельсия и месяц должен быть май) можно снова вызвать и вычислить модель, проводя автоматическое размышление над результатами в модуле CX. Обратите внимание, что здесь есть наш “принтер” (установленный ранее), который снова конвертирует значения в десятичную нотацию:
# instance (fun x ->
nn_model x >. 20.0 &&
x.temp = 20.0 &&
x.month = May &&
is_valid_nn x);;
- : nn_input -> bool = <fun>
Instance (after 0 steps, 0.103s):
let (x : nn_input) =
{month = May;
day = Mon;
dmc = 500.;
temp = 20.;
rh = 100.;
rain = (Real.mk_of_string
"24634017759143723418947963885307992/
1878541866480547748364634187934375")}
[✔] Instance found.
module CX : sig val x : nn_input end
# CX.x;;
- : nn_input = {month = May;
day = Mon;
dmc = 500.;
temp = 20.;
rh = 100.;
rain = 13.1133717053}
# nn_model CX.x;;
- : real = 20.0272890315
Доступные тут виды анализа не отличаются от тех, что мы видели выше в задаче классификации. Не будем повторяться и завершим этот раздел иллюстрацией возможностей Imandra в доказательстве пары полезных свойств нашей сети. Начнем с проверки условия, которое, как мы надеемся, будет соблюдать любая разумная модель прогнозирования для этого задания. Попробуем доказать, что область вывода модели никогда не будет отрицательной:
# verify (fun x -> is_valid_nn x ==> nn_model x >=. 0.0);
;- : nn_input -> bool = <fun>
[✓] Theorem proved.
Отлично! Мы доказали, что если наша нейронная сеть получает валидные данные, то она никогда не будет давать сбои в виде отрицательного числа на выходе. Пусть это и простой пример, но он даёт те гарантии, которые нужны для безопасной разработки подобных моделей в реальном мире. Например, для таких случаев, где выход нейросети может формировать часть управляющей последовательности для контроля беспилотного автомобиля.
Теперь попробуем что-то более амбициозное и проверим свою гипотезу. При прочих равных условиях мы ожидаем, что, чем выше температура, тем большая площадь леса сгорит. Из-за недостатков нашей модели (ограниченность данных, стохастичность при обучении, сложные паттерны в природном физическом феномене и т. д.) это утверждение легко искажается в Imandra. Убедитесь в этом сами:
# verify (fun a b ->
is_valid_nn a &&
is_valid_nn b &&
a.month = b.month &&
a.day = b.day &&
a.dmc = b.dmc &&
a.rh = b.rh &&
a.rain = b.rain &&
a.temp >=. b.temp ==>
nn_model a >=. nn_model b);;
- : nn_input -> nn_input -> bool = <fun>
Counterexample (after 0 steps, 0.116s):
let (a : nn_input) =
{month = Feb;
day = Wed;
dmc = (Real.mk_of_string
"2001302860578649047203412202395247295896300726349164954426900657936422485111743/26290894775182656579389311741592195964262695657047583625044304683319346328960");
temp = (Real.mk_of_string "91160069288673997541144963139828470662342220288373496574482010785769071655/16907327829699457607324316232535174253545141901638317443758395294739129472");
rh = (Real.mk_of_string "310987560530841206048248341173125577069685813208286530077844293829277108589275/5258178955036531315877862348318439192852539131409516725008860936663869265792");
rain = (Real.mk_of_string "75815863864250199885180688130868702048660206232272093463832717880470859243/24896680658316909639573211876507761329794219372204151160079833980416047660")}
let (b : nn_input) =
{month = Feb;
day = Wed;
dmc = (Real.mk_of_string "2001302860578649047203412202395247295896300726349164954426900657936422485111743/26290894775182656579389311741592195964262695657047583625044304683319346328960");
temp = 0.;
rh = (Real.mk_of_string "310987560530841206048248341173125577069685813208286530077844293829277108589275/5258178955036531315877862348318439192852539131409516725008860936663869265792");
rain = (Real.mk_of_string "75815863864250199885180688130868702048660206232272093463832717880470859243/24896680658316909639573211876507761329794219372204151160079833980416047660")}
[✗] Conjecture refuted.
module CX : sig val a : nn_input val b : nn_input end
Получилось достаточно много информации. Однако если углубиться в неё, то можно изучить ключевые части контрпримеров, которые сгенерировала Imandra. Например, мы уже знаем, что вводные данные будут одинаковыми во всех функциях, кроме температуры. Поэтому давайте сразу посмотрим на эти значения, а потом запустим каждый контрпример в модель. Так мы увидим, как она действительно опровергнет нашу гипотезу:
# CX.a.temp;;
- : real = 5.39174908104
# CX.b.temp;;
- : real = 0.
# nn_model CX.a;;
- : real = 1.47805400176
# nn_model CX.b;;
- : real = 1.79452234896
Не всё ещё потеряно. Хотя сеть и не соответствует нашему изначальному утверждению проверки, мы можем ограничить нашу установку, чтобы доказать что-то более простое:
- Поскольку данных о зимних месяцах совсем немного, вряд ли модель сделает достоверное обобщение в этой части. Поэтому мы будем рассматривать все месяцы кроме зимних.
- Увеличим допуск по температуре до 10 градусов Цельсия.
- И аналогично — допуск по сожжённой территории до 25 гектаров.
/Условие определения зимних месяцев
let winter month = month = Oct || month = Nov || month = Dec || month = Jan || month = Feb
С учетом этих допущений Imandra вернёт финальное доказательство:
# verify (fun a b ->
is_valid_nn a &&
is_valid_nn b &&
a.month = b.month &&
not (winter a.month) &&
a.day = b.day &&
a.dmc = b.dmc &&
a.rh = b.rh &&
a.rain = b.rain &&
(a.temp -. 10.0) >=. b.temp ==>
(nn_model a +. 25.0) >=. nn_model b);;
- : nn_input -> nn_input -> bool = <fun>
[✓] Theorem proved.
Заключение
Итак, в контексте моделей, изучаемых по данным, мы прошли только один из множества путей использования формальных методов в области МО. А пока эта задача остаётся сложной, поскольку большинству самых современных подходов необходимо узкоспециализированное ПО, техники и методы, которые Imandra пока ещё не поддерживает.
Мы стремимся улучшить способности Imandra, в особенности масштабируемость. При этом есть и другие интересные пути в сфере наших исследований. Например, использование декомпозиции области для повышения эффективности выборки в процессе глубокого обучения с подкреплением.
Если вам интересно разобраться с такими вопросами, то заглядывайте в другие рабочие ноутбуки, читайте и получайте обновления с нашего сайта на почту. Подтягивайте английский и участвуйте в обсуждении на канале Discord.
Перевод статьи Lewis Hammond: Analysing Machine Learning Models with Imandra
Комментарии