Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2020-02-09 20:27:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: tired
Музыка:Forgotten Woods - AS THE WOLVES GATHER
Entry tags:math, smeshnoe

Cyclicly co-fibrant co-homotopy
Прекрасное
https://cemulate.github.io/the-mlab/
генератор статей из нкатлаба
совершенно неотличимых от оригинала
Уважаю дико

Если перегружать, она загружает новую статью,
такую же осмысленную! бесконечно много их.



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


[info]sometimes
2020-02-11 17:55 (ссылка)
> тонко красивые, куда там Талю.
Ну это вы перебарщиваете. Для "тонко красивых партий" нужно, чтобы соперник глубоко ошибался
(и за это Таля критиковали Бронштейн и Корчной - в противовес Бронштейну Таль максимально
запутывал позицию, так что все фигуры находились под взаимным боем; у счетного движка на
это есть "форсированный вариант", в котором считаются только шахи и взятия, так что с ним
такой номер не прокатит).

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

Что касается математики - вот интересно, допустим, компьютер научится прилично решать задачи
(на уровне сильного математика); и предположим, что он бы это умел бы уже в 19 веке, и доказал
бы (формально, в рамках аксиом Пеано или там ZFC) неразрешимость уравнений степени выше 5 в радикалах.
И вот, внимание, вопрос - удалось ли бы вытрясти из этого черного ящика и сгенерированной
им пачки страниц с логическими символами теорию Галуа?

Потому что частично компьютерные (с переборными программами) доказательства уже известны лет
30 как, толку-то с них, только proof of concept и всё.

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


[info]balalajkin
2020-02-12 02:37 (ссылка)
Ну вот например, охуительная же партия, вполне в духе Таля.

https://www.youtube.com/watch?v=YgZEaP6Qte0

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


[info]balalajkin
2020-02-12 03:37 (ссылка)
Идея написания хороших математических статей при помощи компьютера - это кажется на поверхности - нейросеть пишет варианты решения известных задач, аналитический движок ищет ошибки и отсекает заимствования.

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


[info]sometimes
2020-02-13 02:39 (ссылка)
Не, так не взлетит (нейросеть генеративного типа генерит ахинею, там за сто лет аналитический движок ничего не найдет, это все равно как броуновским движением писать стихи, а потом искать смысл).

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

Важно, что все ходы - корректные; "математическому движку" в этом смысле соответствовали бы тоже только корректные "логические ходы".

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

Математики без особого восторга относятся к записыванию утверждений в строго формальном виде (хотя в последнее время есть определенный прогресс, см. https://www.youtube.com/watch?v=Dp-mQ3HxgDE - Баззард не хуй собачий, а наоборот ученик Ричарда Тейлора, который гипотеза Шимуры-Таниямы-Вейля), а шахматных партий, чтобы стать Бронштейном, Фишером и Талем, надо наиграть реально дохуища; проблема в том, что, как это не дико звучит, математики берут задачи из объективной реальности, в некотором смысле - предпочитая формулировки, которые им почему-либо кажутся интересными, что воспитано физико-арифметической реальностью и традицией.

Насколько близок прорыв в этом направлении - не очень понятно; чуваки про Deep Learning очень хотят сделать девайс, который сможет функционировать не в системе с небольшим простым набором формальных правил (как шахматы), а прямо тут, чтобы нас всех поубивать нахуй - вот звезды DL тут, кажется, об этом тоже говорили https://vimeo.com/390347111; но через какое время у девайса получится нас нахуй поубивать, у них пока оценить не получается; разброс, типа, от 10 лет до 200.

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


[info]sometimes
2020-02-13 02:47 (ссылка)
Звезды думают вот о чем: нейросеть на самом деле играет и учится гораздо хуже человека; скорость работы GPU в миллиард раз выше, чем скорость работы мозга, поэтому она наигрывает с собой на порядки больше партий, чем шахматист. Шахматиста, уже гроссмейстера и гения, подводит во время счета медленность и несовершенство его мозга, снова; если бы он своей внутренней функцией оценки мог бы перебирать ходы так же быстро, как видеокарта, он бы вынес её вдребезги, конечно.

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

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


(Анонимно)
2020-02-13 14:30 (ссылка)
Она и так сможет. Подумай.

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


[info]stereo_sanctity
2020-02-13 11:36 (ссылка)
> частично компьютерные (с переборными программами) доказательства

Переборные доказательства это вроде бы тема 1950х, в 1960х уже изобрели

https://en.wikipedia.org/wiki/Resolution_(logic) --

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

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


[info]sometimes
2020-02-13 16:04 (ссылка)
Я не про теорию, а про Аппеля и Хакена (то есть про настоящие доказательства настоящих
теорем с помощью компьютера - толку от них, впрочем, мало, понимания они особо не
прибавляют). Такого сейчас уже довольно много - это когда компьютер используют
для обхода обширной комбинаторной структуры и проверки свойств в каждой вершине.

Почему "минимальных моделей" планарных графов получается так много (в отличие от
случая g > 0), и почему нельзя доказать, что они покрывают всё, непереборным
образом, совершенно непонятно до сих пор вроде. Это как если бы для доказательства
однозначности разложения на множители в кольце целых пришлось бы разбирать
50 разных случаев (не имеющих никакой самостоятельной ценности причем).

Что касается стратегий, они не особо помогают. Есть proof assistance типа Coq
или вот там на видео LEAN даже гораздо лучше, но они не слишком хороши -
гэпы (пропущенные за недостатком занудства) в совершенно прозрачных на глаз
математика доказательствах оно заполняет довольно хреново.

Поэтому и думают про deep learning.

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


[info]stereo_sanctity
2020-02-13 20:51 (ссылка)
> про Аппеля и Хакена

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

Просто экспертную систему по отрасли знания
куда уже математики, типа автоматический юрисконсульт,
сделать довольно сложно, чтобы заменяла нормально человека,
а в математике, емнип, до сих пор споры идут,
является ли математика познаваемой областью знания,
или это все конструируемое знание:
сори, если проебываюсь с терминологией,
но со вторым машины работать не умеют пока,
и действительно вся надежда на Deep Learning.

Мне кажется только, что реальный прорыв в этом DL
произойдет когда наконец-то сделают нормальный хардварь,
который работает с нечеткими множествами и логиками поверх них,
и алгоритмы тоже долбить надо сильно в ту сторону дальше текущих,
полумеры типа TrueNorth/Loihi это все-таки немного не туда, кажется.

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


[info]sometimes
2020-02-14 23:25 (ссылка)
Нечеткие множества - это по факту тип double, все классификаторы внутри
вычисляют какой-то род степени правдоподобия принадлежности классу. Так что такого рода хардварь - это NVIDIA 2080 Ti, TPU и какое-то сейчас ещё более продвинутое говно параллельное недавно выпустили с низким энергопотреблением. Впрочем, число ядер ещё пока совсем несравнимо с числом нейронов в коре - хотя нейрон и более примитивное вычислительное устройство, чем GPU-ядро (но не столь примитивное, как считалось ранее). Но все-таки какую-нибудь аплизию вряд ли получится "обучить" играть в шахматы - а было бы забавно; собаку или дельфина, наверное, можно.

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


[info]stereo_sanctity
2020-02-15 17:36 (ссылка)
не, я больше про neuro-fuzzy подходы
(ANFIS: https://en.wikipedia.org/wiki/Adaptive_neuro_fuzzy_inference_system , и ее потомки),

сейчас очень ного используется это подход в системах с on-chip learning ,
типа умных вебкамер без бэкенда и теде ,

требует много слабее железо чем "традиционный" DL, и работает не хуже, но зачастую железо идет как SoC с единственным применением. плюс можно проследить полностью за тем как система делает inference в большинстве случаев, нет проблемы черного ящика, как с модными ныне NN без нечеткой логики.

но вот фундаментальные исследования сильно тормозят и там фигачат по сути полтора сингапурца/тайваньца : https://ieeexplore.ieee.org/author/37301984400 и соавторы + с середины нулевых особо новых алгоритмов нетути.

Nvidia 2080 Ti это уже хорошо ближе чем нейроморфные интерфейсы, конечно. мне еще Jetson Nano нравится из подобного хардваря,
но чтобы там чтото реальное было,
нужно массово раздавать такие камни,
просить людей подключать к сети,
типа как BOINC вот был,
чтобы машина обучалась постоянно в сети,
чтото подобное

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


[info]jduns
2020-02-17 21:28 (ссылка)
А что сегодня с унивалентными основаниями математики и проверкой доказате(тао с использованием Coq (Воеводский) - есть новости ?
За вопрос извиняюсь, но ничего нового найти не могу.

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


[info]tiphareth
2020-02-17 22:42 (ссылка)
ничего
это всегда была тупая фигня

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


[info]kaledin
2020-02-17 22:52 (ссылка)
Ну, там лично у Воеводского было несколько неплохих идей, но их самих по себе ни для чего не хватает.

Это что касается оснований; вся компьютерная часть фигня целиком.

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


[info]jduns
2020-02-18 06:21 (ссылка)
Понятно. Спасибо !

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


[info]jduns
2020-02-18 06:20 (ссылка)
Спасибо !
Жаль, что все так у Воеводского - как-то никак, после мотивных работ

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


[info]kaledin
2020-02-18 06:22 (ссылка)
Да нет, это по уму-то важнее и более фундаментально, чем мотивные работы (которые по большому счету попса лишь бы отстали). Но он недоделал. Причем даже не потому, что помер.

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


[info]jduns
2020-02-18 22:03 (ссылка)
Простите, но не могу удержаться - а почему ? Меня вся эта история реально волнует (из чистого интереса).
Заранее спасибо за ответ !

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


[info]kaledin
2020-02-18 22:12 (ссылка)
Потому что речь на самом деле про хорошее понимание абстрактной теории гомотопий, которое по ощущениям разных людей должно также задевать лямбда-калкулус и вычислимость. А такого и близко нет пока что.

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


(Анонимно)
2020-02-21 23:10 (ссылка)
Спасибо !

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


[info]stereo_sanctity
2020-02-13 13:44 (ссылка)
Еще вспомнил классный гитхаб по теме -- https://github.com/theoremprover-museum

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


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