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

С развитием математики, усложнением и появлением новых ответвлений, мы наблюдаем очень беспокойные тенденции: из-за слишком «глубокой и специфичной» теории и подходов к доказательству, научное сообщество просто не может проверить многие результаты. Ручная проверка работы сравнялась по сложности с написанием работы. В итоге современная математика наполнена непроверенными теоремами, и это пирамида продолжает расти. Например, в результатах Воеводского, за которые он получил Филдсовскую премию, уже впоследствии были найдены серьезные ошибки, ситуация закончилась благополучно, потому что спустя много лет Воеводский таки смог исправить ошибки - но сам случай симптоматичный. Никто не мог проверить почти 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.

Год подходит к концу, и пришло время вспомнить наиболее важные и запоминающиеся исследования (согласно научным интересам админа), опубликованные в 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 при увеличении разнообразия графов в обучающем датасете.

ControlLLM: Augment Language Models with Tools by Searching on Graphs

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

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

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 на другие домены, требуется база дедуктивных выводов и формализация домена, что для многих областей не очень развито, поэтому перспектива сомнительная.

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. Далее, продолжение с описанием методов редактирования и открытых проблем.

Недавно прошла ICLR 2024. Собрал запоминающиеся и важные статьи по интересным мне темам.

Knowledge Graph Reasoning and Question Answering - рассуждение и генерация ответов на графах знаний.

1. Reasoning on Graphs: Faithful and Interpretable Large Language Model Reasoning - ответим на вопрос "Кто ребенок Алисы?". Сначала на стадии планирования генерируем LLMкой путь отношений z = {marry to → father of}, затем накладываем его на граф знаний wz = (Alice) marry to → (Bob) father of → (Charlie), из структуры графа получаем ответ Charlie. Т.е. в каком-то смысле паттерн-матчинг. LLM знает про структуру графа и через Planning optimization учится создавать все более релевантные пути отношений.

LLM и все, что в них обитает:

1. Unveiling the Pitfalls of Knowledge Editing for Large Language Models - авторы исследуют проблемы, возникающие в процессе редактирования знаний внутри LLM, более подробно в прошлом посте. Из-за запутанной структуры знаний внутри LLM после редактирования появляются необратимые изменения (метастазы), отражающиеся на множество других сопряженных знаний. Даже если измененный факт отредактировать обратно, то на последствия исходного изменения это не повлияет. Еще рассматриваются логические противоречивые хирургий знаний и их следствия. Тема очень важная в контексте Safety AI.

2. The Geometry of Truth: Emergent Linear Structure in Large Language Model Representations of True/False Datasets - геометрия правды и лжи. По моему мнению, самая интересная статья на конфе. Авторы показывают, что истинные и ложные утверждения образуют разделимые линейные структуры во внутренних представлениях LLM

World Modeling - задача изучения богатого представления, которое учитывает динамику среды, что позволяет агенту прогнозировать будущие состояния и последствия своих действий. Классическое поле тестирования агентов - Minecraft.

1. Mastering Memory Tasks with World Models - продолжение и развитие идеи DreamerV3, В Статье улучшает структуру памяти агента из DreamerV3 и позволяет учитывать более долгосрочные зависимости в Модели Мира, может предсказывать на большее кол-во шагов вперед.

На свободную тематику:

1. Talk like a graph: Encoding graphs for large language models - идея крайне простая, но любопытная: как можно энкодить графы внутрь LLM? Спойлер: если в промпте граф описываешь не просто перечислением вершин и ребер: "G граф с нодами 0...8, и ребрами: (0,1),(0,2)…(7,8).", а через структуру отношений в терминах Игры Престолов: "G граф взаимоотношений разных персонажей Ned, Cat, Daenerys...Jaime. В этом графе: Ned and Cat дружат...Cersei and Jaime дружат.", то LLM лучше воспринимает граф, и может больше про него сказать всякой чисто графовой инфы, типа сколько компонент связности, какая степень вершины итд. Всего Тестировалось 9 способов промптить граф.

2. Interpreting CLIP's Image Representation via Text-Based Decomposition - интерпретация внутренней структуры ViT из CLIP. Авторы определяют, какая голова ViT за какой смысловой аспект отвечает. То, что на головах происходит диверсефикация фичей, т.е. разные головы смотрят на разные объекты и уровни абстракции - это известно еще со статьи, где саму архитектуру ViT предлагали, но в данной работе конкретизируется, какая голова отвечает за форму, какая за цвета, итд. Статья - существенный вклад в explainable AI.

3. ULTRA Towards Foundation Models for Knowledge Graph Reasoning - предлагается архитектура фундаментальной модели GNN. Более подробно в этом посте.

4. Neural Network Expressive Power Analysis Via Manifold Topology - оценивается верхняя граница длины FC сети в терминах топологической сложности (сумма чисел Бетти) обучающих данных. В статье все строго доказывается, и это была бы очень хорошая работа, если бы не ограничение на размерность многообразия = 3, но мб это хороший старт для обобщения на произвольную размерность. Ну и все оценки, завязанные на сумму чисел Бетти для облаков точек тоже достаточно спекулятивные. Статья реджектнута.

Я на ICML 2024. Если вы тоже на конференции и хотите пообщаться, маякуйте. Скоро будут посты о конфе, интересных тут работах и впечатлениях.