tiphareth: Cat eating a big sandwich by Rembrant

(Читать комментарии) - (Добавить комментарий)

	(Анонимно) 2022-08-08 21:11 (ссылка)
	миша, вместо того, чтобы смотреть и слушать очередные помои, написали бы по хардкору нейросеть, чтоб сама формулировала теоремы и сама же их доказывала (Ответить) (Ветвь дискуссии)

	nancygold 2022-08-09 18:46 (ссылка)
	>написали >нейросеть Hello, Russian retard. (Ответить) (Уровень выше) (Ветвь дискуссии)

	(Анонимно) 2022-08-09 23:12 (ссылка)
	>Russian Woman. Тренируемую модель всё равно _пишут_, в основном на питоне. (Ответить) (Уровень выше)

montag
2022-08-11 01:29 (ссылка)

Задача несколько иная, чем генерить картинки.
По Карри-Ховарду, теорема - это некая функциональная программа, а процесс доказательства технически идентичен процессу компиляции программы (не вдаваясь в теорию). Компиляторы обычно работают с древовидными структурами данных, а вот машинное обучение делают на графических процессорах или ещё более специализированных устройствах вроде TPU, которые очень быстро обрабатывают тензоры* (коими являются картинки и видео), но которые крайне неэффективно работают с деревьями.
То есть процесс обучения нейросети доказательству теорем требует вычислений, которые слабо ложатся на железо, используемое для машоба. Хотя некий madlad вроде как сумел в компиляцию на GPU: https://scholarworks.iu.edu/dspace/handle/2022/24749

А теоремы и доказательства генерят на компе, почему нет. Просто не нейросетями.

* В computer soyence смысле этого слова

(Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-08-12 07:23 (ссылка)

> Просто не нейросетями.

Нейросетями можно было бы похитить "стиль человеческого доказательства", для того, чтобы для начала сделать приличный proof assistant хотя бы. Человеческое доказательство ближе к тексту, GPT-3 хорошая модель, но (судя по DALLE) она не очень понимает, кто на ком стоял (при просьбе нарисовать mandalorian reading tail to baby Yoda он рисует взрослого Yoda читающего сказку маленькому старичку) и хреново считает, ну вот как-то надо суметь совместить строгость уровня до аксиом и правил вывода и внятность для человека.

Недавно был интересный эксперимент с liquid math у Шольце
https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/

увенчавшийся, в принципе, успехом, который бы удовлетворил Воеводского, например
https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/

Но там использовался Lean, у него, насколько я помню, ещё обычный SMT solver, и есть вопросы с доказательством корректности самого Lean, чтобы замкнуть. Что интересно, однако, взаимодействие с Lean было вполне плодотворным и позволило Шольце в результате разобраться, что происходит в его мутном с его т.з. доказательстве. One small step for a ~~man~~person, так сказать.

(Ответить) (Уровень выше) (Ветвь дискуссии)

	montag 2022-08-12 16:43 (ссылка)
	Под "Просто не нейросетями." я и понимаю SMT-солверы, hammer-ы и прочие тактики. Мне игрища с нейронками для доказательств особого профита не принесли, а вот hammer-ы реально работают. (Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-08-12 20:10 (ссылка)

Мне казалось правдоподобным, что какие-то вариации трансформеров могут помочь "оцифровать" существующие доказательства в конце концов (arxiv, например), чтобы набрать паттернов доказательства; но я совершенно не настоящий сварщик.

(Ответить) (Уровень выше) (Ветвь дискуссии)

montag
2022-08-12 22:59 (ссылка)

Проблема, мне кажется, в том, что смищые картинки DALL-E могут быть неточными, а доказательства - нет. Генерить доказательства можно как угодно (принцип де Брёйна), а вот проверять их нужно неким простым алгоритмом. Вот этот простой алгоритм-то на GPU и не ложится, следовательно имеется bottleneck.

(Ответить) (Уровень выше) (Ветвь дискуссии)

sometimes
2022-08-13 21:49 (ссылка)

Аутологично получилось (из-за размытости обычного языка я непонятно выразился). Попробую на примере (моего общения с языком F*, в частности).

В программировании часто используется сортировка. Что такое "отсортировать массив" человеку "понятно": это "те же самые элементы, идущие в неубывающем порядке". Окей, мы написали это строго: массив есть функция на [1 .. n], через кванторы всеобщности записали неубывание, определили сортировку как биективное отображение [1 .. n] в себя, такое, что композиция с ним неубывающая. И тут начинают сыпаться нюансы: что композиция биективных отображений биективна (допустим даже, это лежит у компилятора в багажнике, но если это не упомянуть в доказательстве, ему придется по всему багажнику искать - не это ли пропущено), что композиция отображений ассоциативна, что инъективное отображение [1 .. n] в себя сюръективно и наоборот - то, что при описании конкретных алгоритмов сортировки, конечно, никогда не упоминается.

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

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

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

(Ответить) (Уровень выше)

	(Анонимно) 2022-11-19 06:36 (ссылка)
	да всё неохота какт (Ответить) (Уровень выше)

(Читать комментарии) -