Очень хорошая статья, спасибо! Со студенческих лет глубоко интересовался этими темами, посчастливилось пройти спецкурс по Матлогике и теории доказательств Льва Дмитриевича Беклемишева в НМУ, базовые курсы по Матлогике и просеминары на мехмате (https://proseminar.math.ru/). Это реально интереснейшая наука, настоящая и очень изящная математика, разбирающая устройство всей остальной математики.
К сожалению автор в конце статьи ушел в сторону Пенроуза и более популистких тем, и не обратил внимание читателей на потрясающе интересные достижения последних лет, с которыми еще долго предстоит разбираться. И кстати тоже сделанные в принстонском Институте перспективных исследований, где когда-то работал Гёдель, выдающимся и очень необычным математиком нашего времени Владимиром Воеводским. Воеводский создал новое направление - Унивалентные основания математики на основе гомотопической теории типов: https://ru.wikipedia.org/wiki/%D0%93%D0%BE%D0%BC%D0%BE%D1%82%D0%BE%D0%BF%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D1%82%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D1%82%D0%B8%D0%BF%D0%BE%D0%B2Если кратко и популярно, то это новый формальный язык для конструирования доказательств и формализации теорий, который можно использовать вместо языка логики высказываний. Работает это примерно так - вы конструируете такой математический объект в формализме теории гомотопий, что само его существование является доказательством какой-то логической конструкции, связывающей объекты из которых он состоит, аналогично тому, как на языке логики можно пришлось бы строить сложные синтаксические конструкции вывода, используя аксиомы теории доказательств и введенные ранее теоремы и объекты теории в рамках которых проводится доказательство. Внеся очень значимый вклад в алгебраическую геометрию, Воеводский говорил, что подходящих формальных инструментов для "автоматизированной" проверки выводимых теорем не существовало, поскольку формализация этих теорем на языке классической логики привела бы к очень громоздким конструкциям. Итак, какое отношение все это имеет к настоящей статье? Демотивация многих математиков после открытия Гёделя похоже привела к тому, что они перестали так активно искать и создавать новые языки и инструменты более высокого уровня для формализации теорий и автоматического вывода и проверки теорем. А ведь неполнота теории правда не означает, что попытка Гильберта аккуратно формализовать всю математику не принесла бы пользы, как минимум в виде удобства построения и анализа новых теорий.Воеводский в одной из своих лекций говорит об этом именно так: "The nature of Goedel's argument shows that it is impossible to construct foundations for mathematics which will be provably consistent.
What we need are the foundations which can be used to construct reliable proofs despite being inconsistent." (https://youtu.be/O45LaFsaqMA?t=2100) Говоря про инструменты более высокого уровня - для любого изучавшего функан хорошей аналогией будет построение функционального анализа на основе теории множеств, либо на основе теории категорий - как говорят у нас в Одессе, это две большие разницы. Гомотопическая теория типов выглядит как действительно очень удобная богатая база для формализации современных разделов математики. Если кому-то стало особенно интересно - очень рекомендую эту книгу: https://hott.github.io/book/nightly/hott-ebook-1280-ga0040d8.pdfКрасота в том, что книга совместно создавалась (и создается https://github.com/HoTT/book) прямо на Git большой группой математиков и теоретиков-информатиков, которые включились в это направление запущенное инициативой Воеводского. Очень интересно послушать, что вдохновило самого Владимира Воеводского заняться основаниями математики, очень рекомендую это видео: https://www.youtube.com/watch?v=55yZE3IoAy8В целом работа Воеводского и то, куда сейчас развивается это направление достойно отдельной очень интересной и яркой статьи.
Все классно, и даже нас пропиарил) Спасибо, подписался на тебя)
По статье есть несколько вопросов. Кто на твой взгляд из покупателей этих данных получает максимальный эффект, т.е. наиболее заметно повышает прибыль в своем бизнесе за счет использования того, что купил у Liveramp? Понимаю, что точный ответ наверное тяжело найти, но интересны твои мысли на эту тему.
Второй вопрос — есть ли кто-то из покупателей Liveramp, кто потом перепродает эти данные, упаковав их в какие-то модели и сделав серьезную добавочную стоимость? Вообще как устроен «вторичный» рынок данных на твой взгляд, какие там игроки?
Третий вопрос — хайп big data потихоньку закончится, как это повлияет на этот рынок в ближайшей перспективе?
И четвертый вопрос — почему про эту тему на Хабр?) Просто любопытно.
Полезные практические статьи про dynamic UI или prodictive UI пока трудно найти, мы сделаем отдельную техническую статью на Хабр про это, так как сейчас делаем бесплатный реп с такой технологией. Из релевантного можно прочесть еще эту статью: gcn.com/articles/2016/08/15/future-ux-predictive-analytics.aspx
Спасибо большое автору за интересную статью! Давно пользуюсь этим методом.
Важное отличие Левенберга — Марквардта, из-за которого я перешел на него с квазиньютоновского Limited-memory BFGS, это возможность Л-М корректно работать в пространстве переменных разного масштаба. LBFGS очень удобен тем, что экономит итерации и ограниченно потребляет память на задачах локальной оптимизации в пространствах большой размерности. Мы удачного использовали его в задачах размерности 30 000, 100 000 и более, например в оптимизации атомных структур больших молекул — там все координаты и их изменения одинакового масштаба, например ангстремы.
Однако, в иных задачах, таких как фиттинг модели под экспериментальные данные, варьируемые параметры модели могут оказаться сильно разных масштабов. Варианты вроде искать оптимум в пространстве логарифмов параметров не всегда разумны. А при введении скалирующих коэффициентов Левенберг — Марквардт по моему опыту оказывается более толерантен к ошибкам скалирования, чем LBFGS, который начинает давать разные оптимумы в зависимости от конкретного выбора скалирования.
Насколько я понял в SciPy сейчас отсутствует реализация Левенберга — Марквардта, мне кажется автор этой статьи вполне дозрел добавить этот метод в SciPy, это был бы очень серьезный вклад.
Однажды столкнулся с необходимостью проводить глобальный фиттинг, пришлось писать собственную реализацию на С++ с использованием оптимизатора Л-М из библиотеки ALGLIB, так как в SciPy этот метод отсутствовал, в Mathematica он формально есть, но заставить его работать в моей задаче мне не удалось — в Mathematica несколько оптимизаторов, метод оптимизации L-M задается как параметр и поддерживается только одним из оптимизаторов, как раз тем, в который нельзя передать в качестве функции свой код. В Matlab тоже оптимизация хромает.
Очень хорошая статья, спасибо! Со студенческих лет глубоко интересовался этими темами, посчастливилось пройти спецкурс по Матлогике и теории доказательств Льва Дмитриевича Беклемишева в НМУ, базовые курсы по Матлогике и просеминары на мехмате (https://proseminar.math.ru/). Это реально интереснейшая наука, настоящая и очень изящная математика, разбирающая устройство всей остальной математики.
К сожалению автор в конце статьи ушел в сторону Пенроуза и более популистких тем, и не обратил внимание читателей на потрясающе интересные достижения последних лет, с которыми еще долго предстоит разбираться. И кстати тоже сделанные в принстонском Институте перспективных исследований, где когда-то работал Гёдель, выдающимся и очень необычным математиком нашего времени Владимиром Воеводским. Воеводский создал новое направление - Унивалентные основания математики на основе гомотопической теории типов: https://ru.wikipedia.org/wiki/%D0%93%D0%BE%D0%BC%D0%BE%D1%82%D0%BE%D0%BF%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D1%82%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D1%82%D0%B8%D0%BF%D0%BE%D0%B2Если кратко и популярно, то это новый формальный язык для конструирования доказательств и формализации теорий, который можно использовать вместо языка логики высказываний. Работает это примерно так - вы конструируете такой математический объект в формализме теории гомотопий, что само его существование является доказательством какой-то логической конструкции, связывающей объекты из которых он состоит, аналогично тому, как на языке логики можно пришлось бы строить сложные синтаксические конструкции вывода, используя аксиомы теории доказательств и введенные ранее теоремы и объекты теории в рамках которых проводится доказательство. Внеся очень значимый вклад в алгебраическую геометрию, Воеводский говорил, что подходящих формальных инструментов для "автоматизированной" проверки выводимых теорем не существовало, поскольку формализация этих теорем на языке классической логики привела бы к очень громоздким конструкциям. Итак, какое отношение все это имеет к настоящей статье? Демотивация многих математиков после открытия Гёделя похоже привела к тому, что они перестали так активно искать и создавать новые языки и инструменты более высокого уровня для формализации теорий и автоматического вывода и проверки теорем. А ведь неполнота теории правда не означает, что попытка Гильберта аккуратно формализовать всю математику не принесла бы пользы, как минимум в виде удобства построения и анализа новых теорий.Воеводский в одной из своих лекций говорит об этом именно так: "The nature of Goedel's argument shows that it is impossible to construct foundations for mathematics which will be provably consistent.
What we need are the foundations which can be used to construct reliable proofs despite being inconsistent." (https://youtu.be/O45LaFsaqMA?t=2100) Говоря про инструменты более высокого уровня - для любого изучавшего функан хорошей аналогией будет построение функционального анализа на основе теории множеств, либо на основе теории категорий - как говорят у нас в Одессе, это две большие разницы. Гомотопическая теория типов выглядит как действительно очень удобная богатая база для формализации современных разделов математики. Если кому-то стало особенно интересно - очень рекомендую эту книгу: https://hott.github.io/book/nightly/hott-ebook-1280-ga0040d8.pdfКрасота в том, что книга совместно создавалась (и создается https://github.com/HoTT/book) прямо на Git большой группой математиков и теоретиков-информатиков, которые включились в это направление запущенное инициативой Воеводского. Очень интересно послушать, что вдохновило самого Владимира Воеводского заняться основаниями математики, очень рекомендую это видео: https://www.youtube.com/watch?v=55yZE3IoAy8В целом работа Воеводского и то, куда сейчас развивается это направление достойно отдельной очень интересной и яркой статьи.
По статье есть несколько вопросов. Кто на твой взгляд из покупателей этих данных получает максимальный эффект, т.е. наиболее заметно повышает прибыль в своем бизнесе за счет использования того, что купил у Liveramp? Понимаю, что точный ответ наверное тяжело найти, но интересны твои мысли на эту тему.
Второй вопрос — есть ли кто-то из покупателей Liveramp, кто потом перепродает эти данные, упаковав их в какие-то модели и сделав серьезную добавочную стоимость? Вообще как устроен «вторичный» рынок данных на твой взгляд, какие там игроки?
Третий вопрос — хайп big data потихоньку закончится, как это повлияет на этот рынок в ближайшей перспективе?
И четвертый вопрос — почему про эту тему на Хабр?) Просто любопытно.
www.youtube.com/watch?v=vzvZR2GICRU
Полезные практические статьи про dynamic UI или prodictive UI пока трудно найти, мы сделаем отдельную техническую статью на Хабр про это, так как сейчас делаем бесплатный реп с такой технологией. Из релевантного можно прочесть еще эту статью:
gcn.com/articles/2016/08/15/future-ux-predictive-analytics.aspx
Важное отличие Левенберга — Марквардта, из-за которого я перешел на него с квазиньютоновского Limited-memory BFGS, это возможность Л-М корректно работать в пространстве переменных разного масштаба. LBFGS очень удобен тем, что экономит итерации и ограниченно потребляет память на задачах локальной оптимизации в пространствах большой размерности. Мы удачного использовали его в задачах размерности 30 000, 100 000 и более, например в оптимизации атомных структур больших молекул — там все координаты и их изменения одинакового масштаба, например ангстремы.
Однако, в иных задачах, таких как фиттинг модели под экспериментальные данные, варьируемые параметры модели могут оказаться сильно разных масштабов. Варианты вроде искать оптимум в пространстве логарифмов параметров не всегда разумны. А при введении скалирующих коэффициентов Левенберг — Марквардт по моему опыту оказывается более толерантен к ошибкам скалирования, чем LBFGS, который начинает давать разные оптимумы в зависимости от конкретного выбора скалирования.
Насколько я понял в SciPy сейчас отсутствует реализация Левенберга — Марквардта, мне кажется автор этой статьи вполне дозрел добавить этот метод в SciPy, это был бы очень серьезный вклад.
Однажды столкнулся с необходимостью проводить глобальный фиттинг, пришлось писать собственную реализацию на С++ с использованием оптимизатора Л-М из библиотеки ALGLIB, так как в SciPy этот метод отсутствовал, в Mathematica он формально есть, но заставить его работать в моей задаче мне не удалось — в Mathematica несколько оптимизаторов, метод оптимизации L-M задается как параметр и поддерживается только одним из оптимизаторов, как раз тем, в который нельзя передать в качестве функции свой код. В Matlab тоже оптимизация хромает.