GPT-f [2020] - LLM пытается доказывать теоремы.
Обязательно посмотрите предыдущий пост, если не видели, там объясняется задача.
Претрейн: помимо кучи текстов из интернета, модель учат на смеси GitHub, arXiv Math, и Math StackExchange.
Файнтюн: На основе базы доказательств Metamath строится датасет для файнтюна, состоящий из последовательностей вида , где нужно предсказать шаг доказательства по цели. Иначе говоря, учимся генерировать тактику доказательства заданного на вход утверждения.
Как работает процесс: мы храним в очереди с приоритетом все вершины дерева доказательства, которые мы ещё не пытались доказывать. Вначале в дереве только корень.
Выбираем вершину из очереди, пытаемся доказать, генерируя 32 тактики доказательства. Скорим их по сумме log-prob-ов всех токенов, и прибавляем скор родителя - это и будут приоритеты, с которыми мы их кладём в очередь.
На попытку доказательства выделяем до 128 таких шагов, и 4 попытки всего процесса, начиная с чистого листа.
После инференса модели на тренировочном датасете задач:
1) Учим value-функцию вида цель -> [0; 1] - предсказывает то, докажет ли модель данное утверждение.
2) Дообучаем генератор тактик на успешных тактиках
Весь процесс применения на трейнсете повторяем заново, теперь уже скоря вершины value-функцией. И потом повторяем 2 пункта выше. Так можно делать сколько угодно раз. То есть претрейн -> файнтюн -> инференс -> файнтюн на инференсе -> инференс №2 -> ...
Результат - 56% успешных док-в на тесте вместо 21% у предыдущего SOTA, и в ходе работы было сгенерировано 23 более коротких доказательств для базы Metamath, которые туда внедрили.
Это открыло ярмарку статей на эту тему, о которых мы ещё поговорим.
@knowledge_accumulator
Обязательно посмотрите предыдущий пост, если не видели, там объясняется задача.
Претрейн: помимо кучи текстов из интернета, модель учат на смеси GitHub, arXiv Math, и Math StackExchange.
Файнтюн: На основе базы доказательств Metamath строится датасет для файнтюна, состоящий из последовательностей вида , где нужно предсказать шаг доказательства по цели. Иначе говоря, учимся генерировать тактику доказательства заданного на вход утверждения.
Как работает процесс: мы храним в очереди с приоритетом все вершины дерева доказательства, которые мы ещё не пытались доказывать. Вначале в дереве только корень.
Выбираем вершину из очереди, пытаемся доказать, генерируя 32 тактики доказательства. Скорим их по сумме log-prob-ов всех токенов, и прибавляем скор родителя - это и будут приоритеты, с которыми мы их кладём в очередь.
На попытку доказательства выделяем до 128 таких шагов, и 4 попытки всего процесса, начиная с чистого листа.
После инференса модели на тренировочном датасете задач:
1) Учим value-функцию вида цель -> [0; 1] - предсказывает то, докажет ли модель данное утверждение.
2) Дообучаем генератор тактик на успешных тактиках
Весь процесс применения на трейнсете повторяем заново, теперь уже скоря вершины value-функцией. И потом повторяем 2 пункта выше. Так можно делать сколько угодно раз. То есть претрейн -> файнтюн -> инференс -> файнтюн на инференсе -> инференс №2 -> ...
Результат - 56% успешных док-в на тесте вместо 21% у предыдущего SOTA, и в ходе работы было сгенерировано 23 более коротких доказательств для базы Metamath, которые туда внедрили.
Это открыло ярмарку статей на эту тему, о которых мы ещё поговорим.
@knowledge_accumulator