Math and ML stuff

Knowledge Editing LLM. Знания в LLM устаревают, может потребоваться дополнение знаний новыми фактами или знания могут быть просто фактически не верными (кстати, исследователи из DeepMind фактчекают существующие LLM).
Как редактировать представления знаний внутри LLM, т.е. делать специальные "хирургии знаний" в соответствии с тем, чтобы модель на заранее выбранные вопросы выдавала новые ожидаемые ответы?

LLM связывает входные данные X (prompt) с соответствующим прогнозом Y. Сначала формируем корпус дискрипторов редактирования D = (X_e, Y_e)_i=0..N, описывающих предполагаемые изменения в ответах LLM.
Например, (X_e, Y_e) = (президент США, Байден), если ранее Y был Трамп. Конечная цель — создать отредактированную модель LLM_edit которая по запросу X_e выдаст Y_e.

Успешно отредактированная модель LLM_edit должна удовлетворять следующим требованиям:

1. Efficacy. Очевидное свойство. LLM_edit с большей вероятностью даст ответы, предусмотренные операцией редактирования.
2. Generality. Устойчивость к перефразированию. Например, на промпт «Кто в настоящее время занимает должность президента США?» также .
3. Locality. Границы редактирования. Не меняются ответы на запросы, которые выходят за рамки темы редактирования: «Кто президент Франции?» по-прежнему - «Макрон». При этом редактирование не должно негативно влиять на решение не-связанных с темой задач (общий ризонинг, конкретные downstream задачи).
4. Portability или Transferability. Знание не изолировано. Одного только изменения ответа Y_e недостаточно. Модель должна давать ответы, учитывая эффекты исправления и распространять редактирование на связанные вопросы (Multi-hop Knowledge Stability), то есть при редактировании имени президента США, должны меняться ассоциированные с ним факты, типа место рождения президента.

Баланс между 3 и 4 условием гарантирует успешное редактирование знаний. Высокоуровневое введение в проблематику можно найти в обзорных статьях здесь_1 и здесь_2. Далее, продолжение с описанием методов редактирования и открытых проблем.

AlphaGeometry от DeepMind . Разбираемся подробно.

AlphaGeometry способна к математическому ризонингу в эвклидовой геометрии на плоскости, на уровне призеров международной олимпиады по геометрии IMO. С этой же задачей GPT-4 справляется с успехом 0%. AlphaGeometry работает как гибрид 2-х парадигм: символьной дедукции и нейросетей. Общий пайплайн вывода выглядит так:

1. Подаем на вход текст задачи: предпосылка и цель, в доменно специфичном языке (DSL)
2. LLM на основе предпосылок генерирует вспомогательную (magic) конструкцию и передаёт в символьный движок.
3. Символьный движок на основе пошагово/аксиоматических методов выполняет механическую дедукцию и предлагает решение.
4. Если решение не правильное, снова отправляем LLM для создания дополнительной новой magic construction.
5. И так в цикле, пока решение не будет найдено.

Компоненты и методология

1.Символьный движок, соединяющий дедукцию и алгебраический вывод (deduction algebraic reasoning - DDAR): берет за основу механические, захардкоженные правила вывода, например: "E середина отрезка AB, F середина AC, то EF параллельно BC". Они давно известны и аккуратно систематизированы в 2000 г. Далее, расширяем эти правила с помощью операций над углами, отношениями, расстояниями между точками и арифметикой с константами - это алгебраическая составляющая движка. Сам по себе этот движок без нейронных компонент показывает эффективность чуть ниже бронзовых медалистов IMO и решает 15 из 30 задач.

2. Генерация синтетических теорем и доказательств. Синтетический датасет доказательств для обучения LLM модели собирается следующим образом: стартуем с предпосылок Р, генерируем направленный ациклический граф (DAG) логического вывода с помощью символьного движка, а затем фиксируем один из узлов N и идем по дереву назад (обратная трассировка) для идентификации подграфа зависимостей G(N), необходимого для геометрического вывода от минимального кол-ва выбранных посылок P (листьев) к выбранному узлу-выводу N, получаем датасет пар: <теорема: листья P и узел N> <подграф-доказательство G(N)>

После отсева изморофных док-в остается 100 млн пар <теорема-доказательство>, длины док-в распределяются от 1 до 247 шагов, средняя длина 60 при средней длины док-ва человеком в IMO - 50 шагов. Среди полученных док-в есть также заново переизобретенные хорошо известные. Стоит отметить, что метод док-в у символьных движков отличается от метода у систем компьютерной алгебры (а их точность 10/30 задач на IMO).

3. Обучение LLM. Структура <P, N, G (N)> сериализуется в текстовую строку <предпосылка> <вывод> <доказательство>. Обучаясь на таких последовательностях символов, языковая модель эффективно учится генерировать доказательство, обусловливая предпосылки и выводы теоремы. Архитектура модели проста - Трансформер с 12 слоями, 8 головами, со скромным 151 млн параметров и длиной контекста 1024 токена обучается всего лишь на 4-х GPU V100. На полученном в п.2 датасете обучают LLM, точность 21/30 задач.
Но это еще не всё.

4. Magic construction. У существующих дедуктивных решений генерации доказательств есть одно ограничение: они плохо справляются, когда требуется предложить нестандартное решение с введением новых понятий. Ключевой момент у AlphaGeometry для генерации доказательств - это предложение magic construction, т.е. введения новых вспомогательных конструкций (exogenous term). Для этого дополняем датасет следующим трюком: берем предпосылки, от которых результат N зависит, но они не входят в минимальный набор Р, и переносим их в доказательство. Тюнинг LLM на этом небольшом дополнении датасета (9 млн) заставляет генеративную модель "строить" новые предпосылки в самом док-ве и повышает точность до 23/30 задач.

В итоге, AlphaGeometry как нейро-символьная система, работающая в цикле, решает 25/30 задач в IMO, золотой медалист 26/30. Говоря про фронтиры применимости за пределами школьной геометрии, то для успешного обобщения AlphaGeometry на другие домены, требуется база дедуктивных выводов и формализация домена, что для многих областей не очень развито, поэтому перспектива сомнительная.

ControlLLM: Augment Language Models with Tools by Searching on Graphs

Продолжение предыдущего поста:
Концептуальный фреймворк для решения мультимодальных задач - т.е. где одновременно нужно делать манипуляции с текстом, изображением, видео, музыкой итд. Пример: "Совмести видео, поданное на вход, с музыкой, и сделай отдельную HTML-страницу для его воспроизведения". Задачи сложные, поэтому их предлагается с помощью ChatGPT разбить на подзадачи. Для каждой большой задачи формируется граф инструментов-ресурсов, в котором ноды инструментов - это применения разных API больших моделей для разных манипуляций с данными, а ресурсы - тип данных (модальность).

Найти решение задачи - это значит найти наилучший путь в графе инструментов-ресурсов от входных данных до целевых (Thoughts on graph вместо Chain of Thought), оценка решений тоже делегируется LLM, а наилучший путь строится с помощью алгоритма поиска в глубину. Получается что-то типа "мышления на графе". Также в 2023 вышла HuggingGPT: схожая концепция решения мультимодальных задач через пингование в правильном порядке разных больших моделей из Huggingface

Год подходит к концу, и пришло время вспомнить наиболее важные и запоминающиеся исследования (согласно научным интересам админа), опубликованные в 2023.

Тема "LLM and foundation models":

Foundation model - конвенционального определения не существует, так что можно условно считать, что это овер-параметризированная модель, "хитрым" (как правило, не требуется меток) образом обученная на больших кастомных датасетах (сбор данных для них - отдельная наука) и способная выучивать информативные, богатые представления знаний, может быть применима для задач, под которые не была обучена. Примеры: BERT, CLIP, DALLe ,итд.

DINOv2: Learning Robust Visual Features without Supervision

Foundation model для CV. Развитие идеи DINOv1 - архитектуры на основе взаимодействия учитель-ученик, где ученик (архитектура ViT, но есть вариации с ResNet) пытается предсказать выходы модели-учителя (имитировать его работу), метки класса в такой постановке не требуются - объяснение от Yannic Kilcher. В новой версии модель обучалась на наборе данных LVD-142M и были добавлены новые фишки в процесс self-DIstillation, а также предложен более эффективный по памяти механизм самовнимания.

Интересный факт: матрицы внимания ViT, обученном методом DINOv1, демонстрируют семантическую сегментацию изображений (это наталкивает на мысль больше исследовать представления трансформеров на предмет - "что они еще выучивают"), однако в DINOv2 такого не наблюдается. Но фичи из DINOv2 все равно можно применять для сторонних задач: оценки глубины, сегментации, матчинг объектов на 2-х изображениях итд. Модели типа DINO уже зарекомендовали себя как сильный фичер-экстрактор (если вам нужны информативные эмбединги, смело берите ViT из DINO или CLIPа в качестве бэкбона)

Llemma: An Open Language Model For Mathematics

Большая языковая модель для решения математических задач. Наиболее интересная особенность в том, что модель обучена в том числе и на данных программ на языках для автоматических док-в теорем, также Llemma бьёт по бенчмаркам другие модели в математическом ризонинге, более подробно в этом посте.

ULTRA: Towards Foundation Models for Knowledge Graph Reasoning

ULTRA - Первая Foundation model для GraphML. Предлагается модель, позволяющая выучивать представления (юзают GNN) графов знаний (KG), которая может быть эффективно перенесена на новые KG датасеты. В задачах прогнозирования отношений и сущностей в zero-shot режиме уже работает лучше, чем существующая SOTA и может быть дотюнена на любые реляционные графы. Известно (см статью How Powerful are Graph Neural Networks?), что мы можем выучивать представления графов и обобщать их на тестовые данные из-за эквивариантности к перестановкам узлов (т.е. выучиваются структурные особенности графа), но можно пойти дальше и заставить модель быть эквивариантной к перестановкам типов отношений - двойная эквивариантность.

Модель ULTRA пытается это делать и выучивает "граф отношений" (ГО) - авторами утверждается, что это такой мощный инвариант структурных закономерностей данных. Ребра в графе отношений бывают 4 типов, в зависимости от того, какого типа сущности они соединяют (tail или head). ГО кодирует топологию в ориентированном графе и ГО можно легко построить по любому реляционному графу. В работе также продемонстрированы тенденции улучшать точность zero-shot при увеличении разнообразия графов в обучающем датасете.

4-й фильм Р.М. - "Поедем с тобой в Макао" про отношения отца и сына, в киноленте достаточно реалистично показана подпольная покерная жизнь, лудоманские трипы и структура покерной игромании.

Сопутствующие и частично показанные в самом фильме материалы - это The Topology of Poker, статья Р.М про топологическое богатство Техас Холдема (разновидность покера). Допустим, у нас есть симплициальный комплекс K_x, построеннный на X вершинах, где X соответствует множеству пар карт (всем раздачам), всего их 1326, и отношениям между ними. Отношение на множестве пар возникает из заранее известной вероятности выиграть одной пары у другой (априорно мы предполагаем, что Карабас 3♣️5♣️ проигрывает паре A♣️2♣️ с вероятностью 0.591), но интересный момент в том, что оно образует сферу, т.к. оно не всегда иерархично (как в игре "камень-ножницы-бумага"). Важно заметить, что вся эта структура не образует ЧУМ.
Основной результат - это Теорема, утверждающая, что K_x содержит S^4 в качестве подкомплексов. Такой комплекс K_x чем-то похож на диаграмму Хасса, но в которой на одном уровне возможны связи и нет транзитивной редукции.

Работа выглядит интересной, по модулю того, что в тексте есть небольшие ошибки, группы гомотопий обозначены как группы гомологий. И конструкция, похожая на их симплициальный комплекс, по всей видимости, была изобретена ранее под названием directed flag complexes (и в ней уже пытались вычислять устойчивые гомологии).

Подробно остановимся на проблеме доказательства теорем и на существующих системах формальных верификаций.

С развитием математики, усложнением и появлением новых ответвлений, мы наблюдаем очень беспокойные тенденции: из-за слишком «глубокой и специфичной» теории и подходов к доказательству, научное сообщество просто не может проверить многие результаты. Ручная проверка работы сравнялась по сложности с написанием работы. В итоге современная математика наполнена непроверенными теоремами, и это пирамида продолжает расти. Например, в результатах Воеводского, за которые он получил Филдсовскую премию, уже впоследствии были найдены серьезные ошибки, ситуация закончилась благополучно, потому что спустя много лет Воеводский таки смог исправить ошибки - но сам случай симптоматичный. Никто не мог проверить почти 10 лет доказательство abc-гипотезы японским математиком Матидзуки, его док-во на 600 страниц остаётся в подвешенном состоянии до сих пор, не смотря на принятие работы в журнал. Аналогичная проблема была с проверкой доказательство теоремы Ферма на 100 страниц от Эндрю Уайлса.

Как избежать этих проблем? Правильно - автоматизировать и делегировать компьютеру проверку доказательств. Но для этого нужно записывать док-ва в понятном машине формате, для этого и были созданы такие языки формальных верификаций как Lean v4, Agda, Isabelle, Idris, а так же Coq (Воеводский осмыслял его теоретические основания). Если доказательство записано корректно, то система быстро его проверит. Эти системы включают библиотеки, содержащие модули, в них определяются мат концепции, которые переопределяются через другие модули с более базовыми понятиями, получается некоторое вложение абстракций. Актуальная проблема в том, что пакетов и модулей внутри языков для записи доказательств для современной математики на данный момент недостаточно. При этом уже существует множество формализаций известных классических теорем, Фриком Вейдиком отслеживался прогресс в формализации 100 величайших теорем - на данный момент 99% сделано, осталась лишь Великая теорема Ферма.

Ниже пример записи на языке Isabell базовой леммы из геометрии о Сумме углов треугольника. Здесь представлено доказательство этой теоремы из модуля Triangle.

lemma angle_sum_triangle:
  assumes "a ≠ b ∨ b ≠ c ∨ a ≠ c"
  shows   "angle c a b + angle a b c + angle b c a = pi"

ML в настоящий момент даёт новый виток развитию автоматических доказательств. Помимо модели Llemmа, за последние годы появилось много исследований в области пруверов: Например, модель ASTactic обученная на датасете CoqGym, успешно предлагает тактики доказательств в виде абстрактных синтаксических деревьев (AST). Система TRAIL c помощью RL ищет оптимальную стратегию доказательства теорем. GPT-f генерирует доказательства на языке Metamath, а недавняя работа HyperTree Proof Search предлагает модель превосходящую по точности GPT-f и обученную на Lean v4.

Как нейросети могут быть применимы в математике?

Большие языковые модели (LLM) уже давно показали способность к математическим выводам: доказательство несложных теорем, решение задач с подробным объяснением. Стоит отметить давнюю работу MathBERT для анализа мат.формул, а также Minerva для мат. ризонинга.

Недавно была представлена модель Llemma на 34 млрда параметров: в основе её архитектуры лежит Code Llama, инициализирована весами модели Llama 2 и оригинальным способом дотренирована на расширенном датасете Proof-Pile-2 (55 млрд токенов), который содержит программный код на 17 ЯП из GitHub, статьи из arxiv и OpenWebMath.
В итоге Llemma умеет следующее:

1. Solving Math Problems. Prompt: постановка математической задачи на естественном языке. Ответ: Пошаговое описание решения, записанное на LateX, а затем его имплементация на Python.

2. Informal-to-formal. Prompt: доказательство на естественном языке. Ответ: запись на формальном языке доказательства теорем (proof assistant) Isabelle .

3. Formal-to-formal. Prompt: доказательство на формальном языке Lean. Ответ: разбиение доказательства из prompt в последовательность шагов с подробным описанием на том же языке Lean.

Интригующие результаты в применении инструментов компьютерной алгебры и средств формального доказательства теорем удалось добиться с помощью добавления большого объема данных, связанных с программированием математики, символьными вычислениям итд; авторы назвали эту часть собранного датасета - AlgebraicStack. Утверждается, что Llemmа по точности бьёт все прошлые подходы: Minerva (540 млрд параметров и не open-sourse), Code Llama; при этом исходный код, веса модели и датасет в открытом доступе.

Видео-лекция с подробным описанием работы от Sean Welleck на New Technologies in Mathematics Seminar, в рамках этого семинара затрагивают и много других интересных тем: формальное математическое объяснение успеха механизма Attention или статистическая механика в нейросетках.

пока писал этот текст, вышла статья LEGO-Prover про док-во теорем с помощью LLM.

Автор канала теперь живет в Японии. Фото, истории про местную специфику и стримы с улиц Токио можно найти в лайв-канале https://t.me/junkyard_goi_jin

Топологические графовые нейронные сети TGNN - это обобщение классических GNN на случай, когда данные имеют богатую топологическую информацию. Такие сети обучаются аналогично GNN через message passing, но с учетом того, что данные могут содержать не только ребра и вершины, но и более высокоразмерные подструктуры, а отношения между подструктурами сложнее. Кратко упомянем основные типы архитектур TGNN:

1. Simplicial Complexes (SC) TGNN: в отличии от GNN допускается не только вершины и ребра, но и симплексы более высоких размерностей. Примеры архитектур: SNN, Hodge Laplacian, SCCONV.

2. Cellular Complexes (CC) TGNN: обобщение SC на случай, когда клетки не ограничиваются симплексами и могут содержать более 3-х узлов. За счет этих дополнений архитектура CC более выразительная. Примеры: CXNs, Cell attention networks

3. Hypergraphs: обобщение графов, которое позволяет соединять ребрами произвольные подмножства вершин. Более подробно про это написал Paul Snopov в посте о нашем с ним участии в ICML челендже, где мы реализовали архитектуры HyperSage и HyperGat.

4. Combinatorial complexes (CCCs): обобщают клеточные и гиперграфы, позволяют также реализовывать тип отношений часть-целое. Higher-Order Attention Networks (HOAN)

5*. Отдельно стоят Neural Sheaf Diffusion - GNN на основе клеточных пучков.

TGNN уже давно применяются для анализа молекул, социальных сетей, графов цитирования и для многих других задач, где просто GNN могут справляться не очень успешно из-за слабой выразительной силы. Более подробно это объясняется в "A Survey on The Expressive Power of Graph Neural Networks".

Готовые имплементации архитектур TGNN удобно представлены в фреймворке TopoModelX. А также недавно вышел тех-репорт по ICML 2023 Topological Deep Learning Challenge, в котором предлагалось сделать контрибьюшн в TopoModelX.

Asynchronous Algorithmic Alignment with Cocycles, среди авторов Petar Velickovic

Предлагается теоретическое обоснование дизайна архитектуры графовой нейронной сети (GNN ) c полностью асинхронным вычислением (update и aggregation) состояний узлов. Для того, что бы имплементировать такую архитектуру, операция обновления и агрегации должна удовлетворять некоторым условиям: быть коммутативным моноидом и быть идемпотентной. Авторы называют такие функции - 1-коциклы. Кода и экспериментов нет.

https://arxiv.org/pdf/2306.15632.pdf

Применение GPT-2 для генерации элементов из пересечения нормальных замыканий: prompt и masking подходы

Applying language models to algebraic topology: generating simplicial cycles using multi-labeling in Wu's formula

Computing homotopy groups of spheres has long been a fundamental objective in algebraic topology. Various theoretical and algorithmic approaches have been developed to tackle this problem. In this paper we take a step towards the goal of comprehending the group-theoretic structure of the generators of these homotopy groups by leveraging the power of machine learning. Specifically, in the simplicial group setting of Wu's formula, we reformulate the problem of generating simplicial cycles as a problem of sampling from the intersection of algorithmic datasets related to Dyck languages. We present and evaluate language modelling approaches that employ multi-label information for input sequences, along with the necessary group-theoretic toolkit and non-neural baselines.

Neural Networks are Decision Trees

In this manuscript, we show that any neural network with any activation function can be represented as a decision tree. The representation is equivalence and not an approximation, thus keeping the accuracy of the neural network exactly as is. We believe that this work provides better understanding of neural networks and paves the way to tackle their black-box nature. We share equivalent trees of some neural networks and show that besides providing interpretability, tree representation can also achieve some computational advantages for small networks. The analysis holds both for fully connected and convolutional networks, which may or may not also include skip connections and/or normalizations.

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

Riemannian Geometry of Symmetric Positive Definite Matrices via Cholesky Decomposition

We present a new Riemannian metric, termed Log-Cholesky metric, on the manifold of symmetric positive definite (SPD) matrices via Cholesky decomposition. We first construct a Lie group structure and a bi-invariant metric on Cholesky space, the collection of lower triangular matrices whose diagonal elements are all positive. Such group structure and metric are then pushed forward to the space of SPD matrices via the inverse of Cholesky decomposition that is a bijective map between Cholesky space and SPD matrix space. This new Riemannian metric and Lie group structure fully circumvent swelling effect, in the sense that the determinant of the Fréchet average of a set of SPD matrices under the presented metric, called Log-Cholesky average, is between the minimum and the maximum of the determinants of the original SPD matrices. Comparing to existing metrics such as the affine-invariant metric and Log-Euclidean metric, the presented metric is simpler, more computationally efficient and numerically stabler. In particular, parallel transport along geodesics under Log-Cholesky metric is given in a closed and easy-to-compute form.

Data Analysis with the Riemannian Geometry of Symmetric Positive-Definite Matrices
http://www.ipam.ucla.edu/abstract/?tid=15457&pcode=GLWS3

Data Topology-Dependent Upper Bounds of Neural Network Widths

Our primary contribution is to introduce data topology-dependent upper bounds on the network width. Specifically, we first show that a three-layer neural network, applying a ReLU activation function and max pooling, can be designed to approximate an indicator function over a compact set, one that is encompassed by a tight convex polytope. This is then extended to a simplicial complex, deriving width upper bounds based on its topological structure. Further, we calculate upper bounds in relation to the Betti numbers of select topological spaces. Finally, we prove the universal approximation property of three-layer ReLU networks using our topological approach. We also verify that gradient descent converges to the network structure proposed in our study.

https://arxiv.org/pdf/2305.16375.pdf