Бенчмарк · 25 липня 2024 р.
Срібло Міжнародної математичної олімпіади
AlphaProof і AlphaGeometry 2 розв'язали чотири задачі з шести й набрали 28 балів із 42 — на бал менше за поріг золотої медалі.
Чому це важливо
Машина вперше пройшла олімпіадну математику на рівні сильного людського учасника, а не лише окремий її розділ.
AlphaProof формулює задачу мовою Lean, де кожен крок перевіряється машинно, і навчається грою проти себе: породжує варіанти доведення, перевіряє їх, підсилюється на тих, що пройшли. AlphaGeometry 2 взяла геометричну задачу. Три задачі система розв'язала повністю, включно з найважчою, яку на живій олімпіаді здолали лише п'ятеро учасників. Застереження було в часі: людям дають дев'ять годин, системі на одну задачу знадобилися дні.
Відомості про подію
- Дата події
- 25 липня 2024 р.
- Дата на часовій лінії
- Дата події
- Перевірка
- Джерела зібрано автоматично · 18 вересня 2026 р.
- Лінії
- ID
- evt-0306
Оголошення від 25 липня 2024 року, за результатами олімпіади того року.
Записи, що посилаються на цей
- Розвиває Золото Міжнародної математичної олімпіади
Та сама олімпіада через рік: із срібла на золото, і вже без формальної мови.
Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad - Уможливлює Числення конструкцій
AlphaProof записує задачі в Lean, а ядро Lean, за статтею його авторів 2015 року, дає версію числення індуктивних конструкцій із посиланням на цю роботу.
The Lean Theorem Prover (system description) (Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer), CADE-25, LNCS 9195, 378-388AI achieves silver-medal standard solving International Mathematical Olympiad problems