В OpenAI обучили модель доказывать теоремы

OpenAI представила нейросеть, доказывающую теоремы. Модель достигла точности 41% на miniF2F — датасете школьных олимпиадных задач.

Для поиска доказательств используется языковая модель, обученная по принципу обучения школьников: каждый раз, когда нейросеть находит новое доказательство, оно добавляется в обучающий датасет, что улучшает нейросеть и позволяет ей итеративно находить решения все более сложных утверждений.

Лучший результат на бенчмарке miniF2F (41.2% против 29.3% у предыдущей state-of-the-art модели) был достигнут после 8 итераций обучения.

В OpenAI утверждают, что использование обучения с подкреплением не позволило бы получить столь высокий результат из-за бесконечного пространства математических действий. Использование языковой модели решает эту проблему, так как языковые модели обладают способностью вводить новые математические конструкции, позволяющие решить задачу (как это сделано в примере ниже, где модель вводит выражение n + 1, позволяющее доказать теорему):