Обсуждение

Глупо логику и математику отрабатывать в нейронной сети, она должна отрабатываться на классических компьютерных архитектурах.

У меня есть чувство, что при помощи нейронных сеток можно искать доказательства теорем в символьном виде. т.е. использовать нейронные сетки вместо эвристик, которые сейчас запрограммированны вручную, но все символьные выражения держать в символьном виде.

У меня тоже есть такое чувство -- важно только найти правильный баланс. Ибо нейронными сетками и просто можно делать символьный вывод (мозги-то его делают), только это очень неэффективно. "Можно" -- это не значит "нужно".

Помните я говорил, что алг. верификация это сначала верификация, потом синтез сразу-верифицированных моделей? Вот как раз на втором этапе welcome deep learning, потому что надо искать решения уравнений. Я думаю это вполне возможно. И будет электронный инженер :)

Оптимизация кода, построение планов запросов, решение систем уравнений в символьном виде и даже формальные доказательства - это всё цепочки преобразований, по каждому из которых в отдельности нельзя предсказать, приближает ли оно к одному из правильных (или одному из более выгодных) решений. "Потенциально выигрышные" стратегии перебираются вручную и хардкодятся. Вот пусть "кластер-самоучка" их и перебирает, экономя время специалистов.

А вот интересно, что будет, если взять, например, все теории, написанные на Coq, и скормить сети с удачной архитектурой? А потом поставить задачу, и продолжай, мол.

Это обратная задача, для которой нельзя создать машинную метрику качества. Т.е. вот генерируется по выбранной аксиоматике бесконечное множество теорий - какие из них полезны и являются свидетельством хорошей стратегии генерации?

машинную метрику качества нельзя, зато: 1) можно подключить пруф чекер и направить фидбек от него на вход сети, таким образом она будет учиться выдавать только корректные теории 2) сеть учится на осмыслегнных, прагматичных теориях, а не на случайном потоке корректных формул, так что есть надежда, что она внутри себя там что-то "поймет" про прагматики и поэтому ее выдача будет не совсем уж бессмысленным перебором всех корректных теорий подряд

на самом деле даже из первого пункта уже много можно извлечь: 1) нанимаем гениального архитектора сетей, который придумывает мудрую архитектуру 2) реализуем сеть 3) скармливаем сети все coq-файлы, которые удается найти в интернете 4) закорачиваем фидбек пруфчекера на вход сети, чтобы она училась выдавать только корректные теории 5) формулируем открытую проблему в виде теоремы и подаем сети для продолжения (понятия не имею, как это сделать) 6) любая корректная теория, выданная сетью, будет корректным формальным доказательством сформулированной проблемы, не важно насколько распухшим, нечитаемым и использующим непостижимые нечеловеческие тактики доказательств оно будет

и обратите внимание на тот интересный факт, что для сети в том состоянии, когда мы уже запихали в нее все Coq тексты мира, но еще не крутили циклы с обратной связью от пруфчекера, нет разделения на корректость и полезность теорий, есть только некий образ хороших теорий, которые нравятся людям

1. Теории уже корректны, так как выведены по аксиоматике. 2. Для понимания чего-то внутри требуется мотивация извне. Чётко заданные критерии "полезности" или хотя бы "интересности".

>> Теории уже корректны, так как выведены по аксиоматике. сеть-то не "выводит по аксиоматике", а синтезирует "по образу и подобию", согласно своей "теории теорий", так что первые ее выходы скорее всего не пройдут пруфчекинг

>> Для понимания чего-то внутри требуется мотивация извне. Чётко заданные критерии "полезности" или хотя бы "интересности". конечно но я имею в виду, что сети показывали только полезные теории, поэтому ее "теория теорий" будет уже только о полезных теориях это, конечно, совсем не так круто, как если бы у нас был инструмен механической оценки полезности, но уже хоть что-то

В режиме заметки на полях: Попытки написать программу, которая не только по-настоящему понимает математику, но и может двигать ее вперед (начиная с переизобретения фундаментальных уже известных теорем и так далее), предпринимаются уже давно http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.53.3340&rep=rep1&type=pdf https://at-web1.comp.glam.ac.uk/pages/research/ai-cognitive-science/mu.html попытке не совсем безуспешны, но на некоем уровне сложности внезапно наступает затык, папер называется что-то вроде "Why Mathematics Understander is Out Of Steam" не смог нагуглить пока быть может, для нейросетей не будет такого досадного "потолка"

Если вы формализовали критерии "по образу и подобию", то можете попробовать и такую сеть. Но смысла в ней нет. Вычислительные затраты на генерацию по аксиоматике практически ничтожны по сравнению с затратами на доказательство, а для каждой рассматриваемой теории заведомо потребуется либо одно, либо другое. Сеть здесь пригодна только для выбора стратегий, какие комбинации преобразований пробовать в первую очередь, etc. Если дана мотивация, разумеется.

неэффективно -- это если низкоуровнево: берем символьный алгоритм и реализуем его поверх сети а если высокоуровнево? берем генератор теорий, обучаем, соединяем с программами проверки доказательств и заставляем решать открытые проблемы -- то не факт, что не получится и аналогия с wetware, кстати, тут тоже прекрасно работает

Вот, нашёл http://archive.is/WPCN https://en.wikipedia.org/wiki/Automated_Mathematician

А ещё есть системы моделирования с экспортом в theorem proof assistant's форматы, типа AutoFocus3 (экспортирует в Isabelle/HOL) если бы много накопить таких материалов, можно было бы обучать сети ещё и связи теорий и моделей, про которые они "рассуждают"

Папер по теме -- AutoFocus Tool Chain https://www4.in.tum.de/publ/papers/@techreport%7BTUM-I1021%7D.pdf

Давайте я на всякий случай переформулирую свое предложение, дабы устранить всякие недоразумения. У нас есть совокупность людей, которая генерирует теории на языке Coq (выбираем его, потому что у меня создалось впечатление, что больше всего теорий написанно именно на этом языке). Таким образом, мы имеем некий мегаинтеллект, продуцирующий теории на Coq, которые ему по каким-то причинам интересны. Мы берем сеть, которая делает то же, что и этот мегаинтеллект -- генерирует интересные теории на Coq. Далее. Некоторые из них пройдут проверку, если их засунуть в Coq, а а на некоторых он будет выдавать сообщение об ошибке. Мы запускаем ферму, на ней запускаем выдающую теории сеть, ее выход подаем на проверятель, и в зависимости от исхода проверки поощряем или наказываем сеть. В результате сеть изменяет себя таким образом, что процент ее теорий, который проходит проверку, становится все больше и больше. Тут выход сети становится интересен -- в плане свежих идей, до которых не дает добраться сложившаяся культура. Но можно пойти еще дальше -- заставить сеть генерить теории, начинающиеся с данного префикса -- в который мы засовываем формулировку открытой проблемы. Все ее выходы с данным префиксом, прошедшие проверку проверятелем, будут решениями открытой проблемы.

Можно ещё внести простой критерий качества выходной теории -- ее размер ("компактификация описаний")