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

    OpenAI представила нейросеть, доказывающую теоремы. Модель достигла точности 41% на miniF2F — датасете школьных олимпиадных задач.
    Для поиска доказательств используется языковая модель, обученная по принципу обучения школьников: каждый раз, когда нейросеть находит новое доказательство, оно добавляется в обучающий датасет, что улучшает нейросеть и позволяет ей итеративно находить решения все более сложных утверждений.
    Лучший результат на бенчмарке miniF2F (41.2% против 29.3% у предыдущей state-of-the-art модели) был достигнут после 8 итераций обучения.
    В OpenAI утверждают, что использование обучения с подкреплением не позволило бы получить столь высокий результат из-за бесконечного пространства математических действий. Использование языковой модели решает эту проблему, так как языковые модели обладают способностью вводить новые математические конструкции, позволяющие решить задачу (как это сделано в примере ниже, где модель вводит выражение n + 1, позволяющее доказать теорему):
    Подписаться
    Уведомить о
    guest
    0 Comments
    Межтекстовые Отзывы
    Посмотреть все комментарии