Комментарии 22
А разве основная работа математиков — это доказательства? Я думал, что их основная задача — придумывать интересные математические объекты с прелюбопытнейшими математическими свойствами.
Я не понимаю, например, как из аксиом геометрии и арифметики с помощью доказательств можно прийти к понятию планарного графа, групп Ли, или, условным, гёделевским номерам. Или к понятию многообразия.
— Описать планарный граф на языке арифметики (+формальной логики), — можно, Гёдель вам может помешать на прямом пути, при попытке выводить из аксиом вашей формальной системы, но не помешает использовать формальную систему как метаязык для описания аксиом следующего порядка и правил манипуляции ими (очень надеюсь, что сейчас не наврал).
— Догадаться, что планарные графы вообще представляют интерес. Ну, можно дать роботу доступ к реальному миру, где он познает дзен. Я ставлю на то, что можно доступ и не давать, но будет сложнее.
Прийти к понятию — придумать. Если вы сделаете пермутацию всех символов в математическом алфавите для построения всех тавтологий, это никаким образом не позводит вам сделать так:
У нас есть функция декартова произведения N множеств. Я буду это записывать как R^n. А что, если попытатся придумать смысл для утверждения R^r, где r€R? Хм… Выглядит интересно. А какой смысл я могу вложить в идею R^S, где S — произвольное множество, включая R?
Вот это — идеи. И их нельзя получить с помощью тавтологий по аксиомам.
Вы не можете придумать i, перебирая арифметические правила. Вам надо придумать новые объекты и исследовать их. Вот этим и занимаются математики.
Очень советую книгу "Математика в огне" которая как раз и показывает процесс появления новых идей.
Отличие идеи от механической пермутации символов (по правилам) ровно такое же, как в отличии книги от механической пермутации букв. Теоретически второе может сделать первое, практически же, нет того, кто бы это сумел прочитать и понять.
никаким образом не позводит вам сделать так:...Для этого и нужен ML, выбирать интересные направления в пространстве перебора.
Предположение о том, что ML, натасканная на старых теоремах, вдруг, выдаст crown jewel в виде новой теории — это как предположение, что gpt может писать интересные тексты. Тексты она писать умеет, но вот интереса (не говоря уже про нетривиальность) в них...
Видимо, сетку придётся натаскивать, то надо натаскивать на IRL проблемах, откуда интересные идеи и приходят. А вот как натаскать нейронную сеть IRL — никто не знает.
(Примеры лучше на агде, её я хоть чуть-чуть ковырял, coq совсем не осилил.)
Если бы я сейчас занялся, я бы в датасет кроме формул арифметики и простой алгебры напихал бы задачек на базе: — сокобана, маджонга, сднф<->скнф, шахмат, шашек, го и т.д. задачек, вычисление чисел Рамсея,…
Про IRL — Alfa Go Zero не согласен.
Мир комбинации гёделевых чисел неисчерпаем, но перечисляем. Проблема не в том, чтобы найти "богатую теорию", а в том, чтобы из найденного отрезать всё лишнее, но так, чтобы производить впечатление.
Все математические теории строились на размахивании руками предположениях и интуитивном ощущении "это оно". Потом притягивалась строгая аксиоматика и теория, а сначала это было ощущение.
Вот каким образом ML должно будет суметь сделать такое — не понимаю.
Ага, я понял суть проблемы. Все ML'ные псевдотворческие задачи ставят своей метрикой "чтобы обыватель не отличил от человекого творения". А если мы говорим про создание математической теории, то любой школьник вам придумает не хуже, чем нейронная сеть, и будет такая же ахинея, не интересная никому. Нужно, чтобы оно производило впечатление. Творческая составляющая не в рамках определения авторского права (художественная ценность не важна), а в рамках впечатления на человека.
Потому что в финале в математике строгие доказательства, а в начале — безумные бурления креативного сознания.
В первую очередь нужно ощущение красоты (наверное, значительно сводящееся к замечаемой симметрии, может быть, даже между разными формулами и правилами), а во-вторых подспудное чувство достижения (свершения). В целом, весь разговор сейчас может быстро перейти к игре в биссер, потому что там есть много про "формалистскую игру символами без скрытого смысла".
ITP — Интерактивное доказательство теорем
Давно жду прорыва от применения тут машинного обучения, причем польза для машинного обучения превысит пользу для математики. По мне, так удивительно медленно события развиваются.
Говорят, что в 1970-е годы ныне почивший математик Пол Джозеф Коэн, единственный лауреат Филдсовской премии за работы по математической логике, сделал огульное предсказание, которое до сих пор продолжает как восторгать, так и раздражать математиков: «когда-нибудь в будущем математиков заменят компьютеры». Коэн, известный дерзостью методов в работе с теорией множеств, предсказал, что можно автоматизировать всю математику, включая и написание доказательств.Молодец, хорошо высказался. А 1963 году Коэн доказал невозможность доказательства континуум-гипотезы, и своим доказательством подвесил проблему машинного обучения до лучших времен)
Сможет ли система сгенерировать интересную гипотезу и доказать её так, чтобы это было понятно людям?
«Нейросети способны выработать искусственное подобие интуиции», — сказал Сзегеди.Для этого нужно понимать эту интуицию, и новое в понимании ИНС, а это далеко не очевидно, см. эту публикацию. Чтобы такого непонимания возникало меньше, логика ИИ должна быть «дружественной» логике человека, а для этого нужно устранять несоответствия, что-то в этом направлении. Ну, а происхождение интуиции человека, в том числе математической, теряется во мраке эволюции жизни и разума на Земле)
Насколько близко компьютеры подошли к автоматическому построению математических рассуждений?