MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (OpenAI)
Датасет формальных задач по математике олимпиадного уровня, предназначенный для создания единого межсистемного бенчмарка для нейронного доказательства теорем
Статья
GitHub
#datasets #math #ScientificML #gpt
Датасет формальных задач по математике олимпиадного уровня, предназначенный для создания единого межсистемного бенчмарка для нейронного доказательства теорем
Статья
GitHub
#datasets #math #ScientificML #gpt
GitHub
GitHub - openai/miniF2F: Formal to Formal Mathematics Benchmark
Formal to Formal Mathematics Benchmark. Contribute to openai/miniF2F development by creating an account on GitHub.
Может ли машинное обучение в математику?
Судя по недавней статье в Nature - может. DeepMind и Оксфордские математики András Juhász & Marc Lackenby использовали машинное обучение для выявления новых связей в теории узлов.
🎥 Видео
🔭 Блог-пост
#ScientificML #math
Судя по недавней статье в Nature - может. DeepMind и Оксфордские математики András Juhász & Marc Lackenby использовали машинное обучение для выявления новых связей в теории узлов.
🎥 Видео
🔭 Блог-пост
#ScientificML #math
Nature
Advancing mathematics by guiding human intuition with AI
Nature - A framework through which machine learning can guide mathematicians in discovering new conjectures and theorems is presented and shown to yield mathematical insight on important open...
OpenAI научили нейросеть решать (некоторые) олимпиадные задачи по математике
Они создали нейронный доказыватель, который научился решать множество сложных олимпиадных задач для старших классов, включая задачи из конкурсов AMC12 и AIME, а также две задачи, адаптированные из IMO (математики, дайте знать в коментах круто ли это).
Доказыватель использует языковую модель для поиска доказательств формальных утверждений.
Каждый раз, когда OpenAI находят новое доказательство, они используют его в качестве новых обучающих данных (таким образом улучшая нейронную сеть и позволяя ей итеративно находить решения все более трудных утверждений)
📸 Блог-пост
📎 Статья
#ScientificML #math
Они создали нейронный доказыватель, который научился решать множество сложных олимпиадных задач для старших классов, включая задачи из конкурсов AMC12 и AIME, а также две задачи, адаптированные из IMO (математики, дайте знать в коментах круто ли это).
Доказыватель использует языковую модель для поиска доказательств формальных утверждений.
Каждый раз, когда OpenAI находят новое доказательство, они используют его в качестве новых обучающих данных (таким образом улучшая нейронную сеть и позволяя ей итеративно находить решения все более трудных утверждений)
📸 Блог-пост
📎 Статья
#ScientificML #math