Forwarded from Машинное обучение RU
SplineCam: Neural Decision Boundary
🖥 Github: http://github.com/AhmedImtiazPrio/SplineCAM
⭐️ Paper: http://arxiv.org/pdf/2302.12828.pdf
💻 Project : http://imtiazhumayun.github.io/splinecam
@machinelearning_ru
@machinelearning_ru
Please open Telegram to view this post
VIEW IN TELEGRAM
🔥2🤯1😱1
Солженицына цитируют даже западные специалисты по графовым нейросетям
https://towardsdatascience.com/a-new-computational-fabric-for-graph-neural-networks-280ea7e3ed1a
“Topology! The stratosphere of human thought! In the twenty-fourth century, it might possibly be of use to someone.” — Aleksandr Solzhenitsyn, In the First Circle (1968)
https://towardsdatascience.com/a-new-computational-fabric-for-graph-neural-networks-280ea7e3ed1a
“Topology! The stratosphere of human thought! In the twenty-fourth century, it might possibly be of use to someone.” — Aleksandr Solzhenitsyn, In the First Circle (1968)
Medium
A new computational fabric for Graph Neural Networks
Are graphs the right computational fabric for GNNs? A recent line of papers challenges this assumption.
👍3👎1🔥1🥴1
HOW DO VISION TRANSFORMERS WORK?
Global and local aspects consistently show that MSAs flatten loss landscapes. Left: Loss landscape visualizations show that ViT has a flatter loss than ResNet. Right: The magnitude of the Hessian eigenvalues of ViT is smaller than that of ResNet during training phases. Since the Hessian represents local curvature, this also suggests that the loss landscapes of ViT is flatter than that of ResNet.
https://arxiv.org/pdf/2202.06709.pdf
Global and local aspects consistently show that MSAs flatten loss landscapes. Left: Loss landscape visualizations show that ViT has a flatter loss than ResNet. Right: The magnitude of the Hessian eigenvalues of ViT is smaller than that of ResNet during training phases. Since the Hessian represents local curvature, this also suggests that the loss landscapes of ViT is flatter than that of ResNet.
https://arxiv.org/pdf/2202.06709.pdf
🦄2🔥1🙏1🤨1🎃1
TopoAct: Visually Exploring the Shape of Activations in Deep Learning
Deep neural networks such as GoogLeNet, ResNet, and BERT have achieved impressive performance in tasks such as image and text classification. To understand how such performance is achieved, we probe a trained deep neural network by studying neuron activations, i.e., combinations of neuron firings, at various layers of the network in response to a particular input. With a large number of inputs, we aim to obtain a global view of what neurons detect by studying their activations. In particular, we develop visualizations that show the shape of the activation space, the organizational principle behind neuron activations, and the relationships of these activations within a layer. Applying tools from topological data analysis, we present TopoAct, a visual exploration system to study topological summaries of activation vectors. We present exploration scenarios using TopoAct that provide valuable insights into learned representations of neural networks. We expect TopoAct to give a topological perspective that enriches the current toolbox of neural network analysis, and to provide a basis for network architecture diagnosis and data anomaly detection
https://arxiv.org/pdf/1912.06332.pdf
здесь можно потыкать само приложение: https://tdavislab.github.io/TopoAct/single-layer-view.html
Deep neural networks such as GoogLeNet, ResNet, and BERT have achieved impressive performance in tasks such as image and text classification. To understand how such performance is achieved, we probe a trained deep neural network by studying neuron activations, i.e., combinations of neuron firings, at various layers of the network in response to a particular input. With a large number of inputs, we aim to obtain a global view of what neurons detect by studying their activations. In particular, we develop visualizations that show the shape of the activation space, the organizational principle behind neuron activations, and the relationships of these activations within a layer. Applying tools from topological data analysis, we present TopoAct, a visual exploration system to study topological summaries of activation vectors. We present exploration scenarios using TopoAct that provide valuable insights into learned representations of neural networks. We expect TopoAct to give a topological perspective that enriches the current toolbox of neural network analysis, and to provide a basis for network architecture diagnosis and data anomaly detection
https://arxiv.org/pdf/1912.06332.pdf
здесь можно потыкать само приложение: https://tdavislab.github.io/TopoAct/single-layer-view.html
❤5🤨1🦄1
An algorithmic framework for the optimization of deep neural networks architectures and hyperparameters
Авторы показывают, что задачу NAS(Neural Architecture Search) можно разбить на 2 подзадачи - определение структуры (поиск самого DAG - пространство 𝒜) и поиск гиперпараметров (поиск операций в узлах DAG - пространство гиперпараметров Λ(a)). В итоге пространство поиска раскладывается в произведение пространств - Ω=(𝒜×{Λ(a),a∈𝒜}), где a - это архитектура. Далее используется процедура NAS на основе эволюционного элгоритма. Применяется для поиска DNN для задачи предсказания временных рядов.
https://arxiv.org/pdf/2303.12797.pdf
Авторы показывают, что задачу NAS(Neural Architecture Search) можно разбить на 2 подзадачи - определение структуры (поиск самого DAG - пространство 𝒜) и поиск гиперпараметров (поиск операций в узлах DAG - пространство гиперпараметров Λ(a)). В итоге пространство поиска раскладывается в произведение пространств - Ω=(𝒜×{Λ(a),a∈𝒜}), где a - это архитектура. Далее используется процедура NAS на основе эволюционного элгоритма. Применяется для поиска DNN для задачи предсказания временных рядов.
https://arxiv.org/pdf/2303.12797.pdf
🫡3👾2🤨1
Forwarded from MAA — САП
https://arxiv.org/abs/2305.02023 В классическом покере есть 4-мерная сфера.
We examine the complexity of the ``Texas Hold'em'' variant of poker from a topological perspective. We show that there exists a natural simplicial complex governing the multi-way winning probabilities between various hands, and that this simplicial complex contains 4-dimensional spheres as induced subcomplexes. We deduce that evaluating the strength of a pair of cards in Texas Hold'em is an intricate problem, and that even the notion of who is bluffing against whom is ill-defined in some situations.
We examine the complexity of the ``Texas Hold'em'' variant of poker from a topological perspective. We show that there exists a natural simplicial complex governing the multi-way winning probabilities between various hands, and that this simplicial complex contains 4-dimensional spheres as induced subcomplexes. We deduce that evaluating the strength of a pair of cards in Texas Hold'em is an intricate problem, and that even the notion of who is bluffing against whom is ill-defined in some situations.
❤5👍1🔥1
Towards Universal Fake Image Detectors that Generalize Across Generative Models
Авторы решают задачу распознавания фейковых примеров. Используют ViT из CLIP для извлечения признаков из (фейковых/реальных изображениях), затем тренируют обычный log-reg на бинарную классификацию на фичах. Их решение обобщается на разные домены: обучили на данных с генеративной модели ProGAN, и полученный классификатор работает на данных с других доменов (т.е. генеративных моделях - другие GAN: StyleGAN, BigGAN итд и диффузионных моделях). Применение преобученного ViT из CLIP работает лучше, чем файнтюнинг обычного ViT на классификацию.
https://arxiv.org/pdf/2302.10174.pdf
Авторы решают задачу распознавания фейковых примеров. Используют ViT из CLIP для извлечения признаков из (фейковых/реальных изображениях), затем тренируют обычный log-reg на бинарную классификацию на фичах. Их решение обобщается на разные домены: обучили на данных с генеративной модели ProGAN, и полученный классификатор работает на данных с других доменов (т.е. генеративных моделях - другие GAN: StyleGAN, BigGAN итд и диффузионных моделях). Применение преобученного ViT из CLIP работает лучше, чем файнтюнинг обычного ViT на классификацию.
https://arxiv.org/pdf/2302.10174.pdf
🫡1🗿1🦄1
AttentionViz: A Global View of Transformer Attention
Transformer models are revolutionizing machine learning, but their inner workings remain mysterious. In this work, we present a new visualization technique designed to help researchers understand the self-attention mechanism in transformers that allows these models to learn rich, contextual relationships between elements of a sequence. The main idea behind our method is to visualize a joint embedding of the query and key vectors used by transformer models to compute attention. Unlike previous attention visualization techniques, our approach enables the analysis of global patterns across multiple input sequences. We create an interactive visualization tool, AttentionViz (demo: http://attentionviz.com), based on these joint query-key embeddings, and use it to study attention mechanisms in both language and vision transformers. We demonstrate the utility of our approach in improving model understanding and offering new insights about query-key interactions through several application scenarios and expert feedback
Transformer models are revolutionizing machine learning, but their inner workings remain mysterious. In this work, we present a new visualization technique designed to help researchers understand the self-attention mechanism in transformers that allows these models to learn rich, contextual relationships between elements of a sequence. The main idea behind our method is to visualize a joint embedding of the query and key vectors used by transformer models to compute attention. Unlike previous attention visualization techniques, our approach enables the analysis of global patterns across multiple input sequences. We create an interactive visualization tool, AttentionViz (demo: http://attentionviz.com), based on these joint query-key embeddings, and use it to study attention mechanisms in both language and vision transformers. We demonstrate the utility of our approach in improving model understanding and offering new insights about query-key interactions through several application scenarios and expert feedback
🫡3👍2🔥2🦄1
Architectures of Topological Deep Learning: A Survey on Topological Neural Networks
The natural world is full of complex systems characterized by intricate relations between their components: from social interactions between individuals in a social network to electrostatic interactions between atoms in a protein. Topological Deep Learning (TDL) provides a comprehensive framework to process and extract knowledge from data associated with these systems, such as predicting the social community to which an individual belongs or predicting whether a protein can be a reasonable target for drug development. TDL has demonstrated theoretical and practical advantages that hold the promise of breaking ground in the applied sciences and beyond. However, the rapid growth of the TDL literature has also led to a lack of unification in notation and language across Topological Neural Network (TNN) architectures. This presents a real obstacle for building upon existing works and for deploying TNNs to new real-world problems. To address this issue, we provide an accessible introduction to TDL, and compare the recently published TNNs using a unified mathematical and graphical notation. Through an intuitive and critical review of the emerging field of TDL, we extract valuable insights into current challenges and exciting opportunities for future development.
https://arxiv.org/pdf/2304.10031.pdf
The natural world is full of complex systems characterized by intricate relations between their components: from social interactions between individuals in a social network to electrostatic interactions between atoms in a protein. Topological Deep Learning (TDL) provides a comprehensive framework to process and extract knowledge from data associated with these systems, such as predicting the social community to which an individual belongs or predicting whether a protein can be a reasonable target for drug development. TDL has demonstrated theoretical and practical advantages that hold the promise of breaking ground in the applied sciences and beyond. However, the rapid growth of the TDL literature has also led to a lack of unification in notation and language across Topological Neural Network (TNN) architectures. This presents a real obstacle for building upon existing works and for deploying TNNs to new real-world problems. To address this issue, we provide an accessible introduction to TDL, and compare the recently published TNNs using a unified mathematical and graphical notation. Through an intuitive and critical review of the emerging field of TDL, we extract valuable insights into current challenges and exciting opportunities for future development.
https://arxiv.org/pdf/2304.10031.pdf
⚡2👍2🔥2🫡2
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
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
👍3🔥2👨💻1
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
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
IPAM
Abstract - IPAM
Data Analysis with the Riemannian Geometry of Symmetric Positive-Definite Matrices by Ronen Talmon Technion - Israel Institute of Technology
🔥3🫡1💊1
Neural Networks are Decision Trees
In this manunoscript, 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
In this manunoscript, 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
YouTube
Neural Networks are Decision Trees (w/ Alexander Mattick)
#neuralnetworks #machinelearning #ai
Alexander Mattick joins me to discuss the paper "Neural Networks are Decision Trees", which has generated a lot of hype on social media. We ask the question: Has this paper solved one of the large mysteries of deep learning…
Alexander Mattick joins me to discuss the paper "Neural Networks are Decision Trees", which has generated a lot of hype on social media. We ask the question: Has this paper solved one of the large mysteries of deep learning…
💊4👍2👾2🦄1
Применение 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.
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.
🔥6👍2🫡2
Asynchronous Algorithmic Alignment with Cocycles, среди авторов Petar Velickovic
Предлагается теоретическое обоснование дизайна архитектуры графовой нейронной сети (GNN ) c полностью асинхронным вычислением (update и aggregation) состояний узлов. Для того, что бы имплементировать такую архитектуру, операция обновления и агрегации должна удовлетворять некоторым условиям: быть коммутативным моноидом и быть идемпотентной. Авторы называют такие функции - 1-коциклы. Кода и экспериментов нет.
https://arxiv.org/pdf/2306.15632.pdf
Предлагается теоретическое обоснование дизайна архитектуры графовой нейронной сети (GNN ) c полностью асинхронным вычислением (update и aggregation) состояний узлов. Для того, что бы имплементировать такую архитектуру, операция обновления и агрегации должна удовлетворять некоторым условиям: быть коммутативным моноидом и быть идемпотентной. Авторы называют такие функции - 1-коциклы. Кода и экспериментов нет.
https://arxiv.org/pdf/2306.15632.pdf
👍5🔥4🫡1
Топологические графовые нейронные сети 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.
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.
👍10🤯4🔥2🫡2👎1
Автор канала теперь живет в Японии. Фото, истории про местную специфику и стримы с улиц Токио можно найти в лайв-канале https://news.1rj.ru/str/junkyard_goi_jin
🔥14👍2🫡1
Как нейросети могут быть применимы в математике?
Большие языковые модели (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.
Большие языковые модели (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.
❤12👍4🤓4👨💻2