Post #1883
905
Закачиваю гайд по Calculus of Constructions, много читаю по теме, вот свежачок "Programs as Singularities" университета Мельбурна.
Канадцы пытаются связать дискретный мир программ и доказательств с непрерывным миром машинного обучения через алгебраическую геометрию.
Исторически концепция алгоритма/программы развивалась из двух направлений:
- логические рассуждения (от Аристотеля)
- алгебраические вычисления (от аль-Хорезми)
Сегодня концептуальный ландшафт впервые за всю историю кибернетикэ качественно меняется: скоро большая часть сложных когнитивных процессов будет происходить "в машинах".
Авторы пытаются "встроить" дискретный мир программ в непрерывный мир машинного обучения. Но это должно быть гомоморфное отображение: внутренняя структура программ должна отражаться в геометрической структуре непрерывного пространства. Любая наша программа - это набор дискретных инструкций, но нейросети работают в непрерывном пространстве (с вероятностями, градиентами), а программы - в дискретном (чёткие инструкции). И как это состыковать?
Авторы предлагают т.н. "структурный байесианизм".
Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.
Таким образом формируется математический мост между классическим программированием и машинным обучением.
Но подход авторов нацелен конкретно на ML, и ему не хватает ни глубины, ни универсальности, ни прагматизма. Правильно это конечно делать в парадигме гомотопической теории, где геометрия проявляется через непрерывные деформации (гомотопии). HoTT уже имеет хорошо развитый аппарат для работы с непрерывными деформациями типов, понятие type identity естественно связывается с геометрической структурой, а формализовать переход между дискретным и непрерывным могут высшие индуктивные типы.
Например, алгоритм сортировки может быть представлен как зависимый тип
Определяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.
Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.
Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)
Таким образом получится формально доказывать свойства нейросетей, сам процесс их обучения становится непрерывным, а для анализа пространства решений используем топологические методы + визуализацию для человечков.
Основная проблема сейчас -- это исключительно разрыв между теоретической красотой HoTT и практическими инструментами для её применения в реальных задачах (такими, как у меня, но "я их вам не отдам, потому что у меня велосипеда нету" (с) Печкин :). Можно пытаться использовать кривейшие европейские теорем-пруверы, но у нас это зашквар, да и прошлый век уже.
Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.
Канадцы пытаются связать дискретный мир программ и доказательств с непрерывным миром машинного обучения через алгебраическую геометрию.
Исторически концепция алгоритма/программы развивалась из двух направлений:
- логические рассуждения (от Аристотеля)
- алгебраические вычисления (от аль-Хорезми)
Сегодня концептуальный ландшафт впервые за всю историю кибернетикэ качественно меняется: скоро большая часть сложных когнитивных процессов будет происходить "в машинах".
Авторы пытаются "встроить" дискретный мир программ в непрерывный мир машинного обучения. Но это должно быть гомоморфное отображение: внутренняя структура программ должна отражаться в геометрической структуре непрерывного пространства. Любая наша программа - это набор дискретных инструкций, но нейросети работают в непрерывном пространстве (с вероятностями, градиентами), а программы - в дискретном (чёткие инструкции). И как это состыковать?
Авторы предлагают т.н. "структурный байесианизм".
Программа отображается в "особую" точку (сингулярность, где potential function имеет особое поведение). Структура программы отражается в геометрии пространства вокруг этой точки, а ошибки соответствуют определённым типам деформаций около сингулярности. В результате AI сможет "понимать" программы не как черный ящик, а через их геометрическую структуру. Люди (топологи) смогут оценивать "красоту" и эффективность внутренней структуры модели буквально эстетическим чувством, а система сможет "видеть" структуру ошибки геометрически и находить ближайшее корректное решение в этом пространстве.
Таким образом формируется математический мост между классическим программированием и машинным обучением.
Но подход авторов нацелен конкретно на ML, и ему не хватает ни глубины, ни универсальности, ни прагматизма. Правильно это конечно делать в парадигме гомотопической теории, где геометрия проявляется через непрерывные деформации (гомотопии). HoTT уже имеет хорошо развитый аппарат для работы с непрерывными деформациями типов, понятие type identity естественно связывается с геометрической структурой, а формализовать переход между дискретным и непрерывным могут высшие индуктивные типы.
Например, алгоритм сортировки может быть представлен как зависимый тип
Sort : (A: Type) → (List A) → (List A) с доказательством упорядоченности, а нейросеть можно представить как тип NeuralNet : (Input: Type) → (Output: Type) → TypeОпределяем пространство всех возможных программ заданного типа.
Разные реализации одного алгоритма становятся путями в этом пространстве.
Оптимизация нейросети - непрерывное движение по этому пространству.
Можно доказывать корректность программ, можно определять "расстояние" между программами, можно плавно трансформировать одну программу в другую (на уровне AST) и т.д. и т.п.
Веса нейросети = точка в пространстве программ
Обучение = путь в этом пространстве
Ошибки = особые точки (сингулярности)
Таким образом получится формально доказывать свойства нейросетей, сам процесс их обучения становится непрерывным, а для анализа пространства решений используем топологические методы + визуализацию для человечков.
Основная проблема сейчас -- это исключительно разрыв между теоретической красотой HoTT и практическими инструментами для её применения в реальных задачах (такими, как у меня, но "я их вам не отдам, потому что у меня велосипеда нету" (с) Печкин :). Можно пытаться использовать кривейшие европейские теорем-пруверы, но у нас это зашквар, да и прошлый век уже.
Глубокоуважаемый AGIRu, забашляй $1m, и мы с пацанами такое сделаем.
- ❤ 37
- 😁 10
- 👍 6
- 🤯 6
- ✍ 3
