tiphareth: Cyclicly co-fibrant co-homotopy

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

sometimes
2020-02-13 16:04 (ссылка)

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

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

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

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

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

stereo_sanctity
2020-02-13 20:51 (ссылка)

> про Аппеля и Хакена

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

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

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

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

sometimes
2020-02-14 23:25 (ссылка)

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

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

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 вот был,
чтобы машина обучалась постоянно в сети,
чтото подобное

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

jduns
2020-02-17 21:28 (ссылка)

А что сегодня с унивалентными основаниями математики и проверкой доказате(тао с использованием Coq (Воеводский) - есть новости ?
За вопрос извиняюсь, но ничего нового найти не могу.

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

	tiphareth 2020-02-17 22:42 (ссылка)
	ничего это всегда была тупая фигня (Ответить) (Уровень выше) (Ветвь дискуссии)

	kaledin 2020-02-17 22:52 (ссылка)
	Ну, там лично у Воеводского было несколько неплохих идей, но их самих по себе ни для чего не хватает. Это что касается оснований; вся компьютерная часть фигня целиком. (Ответить) (Уровень выше) (Ветвь дискуссии)

	jduns 2020-02-18 06:21 (ссылка)
	Понятно. Спасибо ! (Ответить) (Уровень выше)

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

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

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

kaledin
2020-02-18 22:12 (ссылка)

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

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

	(Анонимно) 2020-02-21 23:10 (ссылка)
	Спасибо ! (Ответить) (Уровень выше)

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