Порушення бар'єру даних у навчанні символічних обчислень: тематичне дослідження щодо пропозиції впорядкування змінних для циліндричної алгебраїчної декомпозиції

Символічні обчислення, що працюють на сучасних системах комп'ютерної алгебри, мають важливе застосування в математичних міркуваннях за допомогою точних глибоких обчислень. Ефективність символічних обчислень значною мірою обмежена такими глибокими обчисленнями у високих розмірах. Це створює фундаментальний бар'єр для збору мічених даних, якщо використовувати контрольоване глибоке навчання для прискорення символічних обчислень. Циліндрична алгебраїчна декомпозиція (CAD) - це метод стовпчастого символічного обчислення для міркування з логічними формулами першого порядку над реалами з багатьма застосуваннями у формальній верифікації та автоматичному доведенні теореми. Змінні замовлення мають величезний вплив на його ефективність. Утруднені труднощами отримання великої кількості мічених даних, існуючі підходи, засновані на навчанні, конкурують лише з найкращою евристикою, заснованою на експертах. У цій роботі ми вирішуємо цю проблему, розробляючи серію тісно пов'язаних завдань, для яких можна легко отримати велику кількість анотованих даних. Ми попередньо навчаємо модель Transformer з цими даними, а потім точно налаштовуємо її на набори даних для замовлення САПР. Експерименти з загальнодоступними наборами даних упорядкування САПР показують, що в середньому порядок, передбачений новою моделлю, значно кращий, ніж запропонований найкращими евристичними методами.