(←) предыдущая запись ; следующая запись (→)
Есть ещё один путь, которым модели логического вывода и модели машинного обучения могли бы друг другу помочь и дополнить друг друга. Можем вспомнить AlphaGo/AlphaZero. Шахматы — игра с жёсткими формальными правилами. Нельзя просто сочинять правдоподобные ходы, потому что они должны не нарушать законы мира: нельзя пойти несуществующей фигурой или съесть несуществующую фигуру, нельзя подставиться под шах итд.
Как же тогда нейросеть может играть? Очень просто: она может перебирать реально допустимые ходы и своим статистическим мозгом оценивать в баллах, насколько благоприятная ситуация сложится в результате каждого из вариантов. А затем выбирать вариант, наилучший по очкам.
К сожалению, вариантов «хода» в логическом выводе гораздо больше, чем в шахматах, поэтому так делать не получится. Дерево (или даже граф) шагов доказательства слишком велик, из каждой вершины торчат миллионы веток. Однако всё ещё можно сделать модель, которая будет «направлять» ход доказательства в нужную сторону. Этакий guided path finding.
Немало задач можно решать в терминах поиска пути по графу. От поиска ближайшего соседа (спасибо А.Л., который рассказал про эту магию) до, не знаю… алгоритмов сборки генома.
Я давно уже думаю, что должны существовать сетки, которые рассматривают эмбеддинг как некоторое описание того, как надо идти по графу: «Три квартала по прямой, потом налево, пройти 50 метров и снова налево во двор» или «сначала докажи, что Сократ человек, а потом — что он то ещё животное».
Но пока на подобные штуки я не натыкался, а всерьёз я тему не исследовал. Если кому-нибудь есть что сказать по теме, буду рад комментариям.
(4/n)