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

Большие языковые модели (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.