- Поиск доказательства гипердерева для доказательства нейронной теоремы (arXiv)
Автор: Гийом Лампель, Мари-Анн Лашо, Тибо Лавриль, Ксавье Мартине, Амори Хаят, Габриэль Эбнер, Орельен Родригес, Тимоти Лакруа.
Аннотация: Мы предлагаем процедуру онлайн-обучения для автоматизированного доказателя теорем на основе трансформатора. В нашем подходе используется новый алгоритм поиска HyperTree Proof Search (HTPS), вдохновленный недавним успехом AlphaZero. Наша модель учится на предыдущих поисковых доказательствах посредством онлайн-обучения, что позволяет обобщать ее на домены, далекие от распределения обучения. Мы сообщаем о подробном анализе основных компонентов нашего конвейера, изучая производительность в трех средах с возрастающей сложностью. В частности, мы показываем, что только с HTPS модели, обученной на аннотированных доказательствах, удается доказать 65,4 % выдвинутого набора теорем Metamath, что значительно превосходит предыдущий уровень техники в 56,5 % с помощью GPT-f. Онлайн-обучение этим недоказанным теоремам повышает точность до 82,6%. С аналогичным вычислительным бюджетом мы улучшаем современное состояние набора данных miniF2F-curriculum на основе Lean с 31% до 42%, доказывая точность.
2. Быстрая параллельная декомпозиция гипердерева в логарифмической глубине рекурсии (arXiv)
Автор:
Абстрактный :
