Запис атласу: https://www.aitimeline.dev/uk/events/evt-0306/
Бенчмарк · 25 липня 2024 р.
Срібло Міжнародної математичної олімпіади
AlphaProof і AlphaGeometry 2 розв'язали чотири задачі з шести й набрали 28 балів із 42 — на бал менше за поріг золотої медалі.
Чому це важливо
Машина вперше пройшла олімпіадну математику на рівні сильного людського учасника, а не лише окремий її розділ.
AlphaProof формулює задачу мовою Lean, де кожен крок перевіряється машинно, і навчається грою проти себе: породжує варіанти доведення, перевіряє їх, підсилюється на тих, що пройшли. AlphaGeometry 2 взяла геометричну задачу. Три задачі система розв'язала повністю, включно з найважчою, яку на живій олімпіаді здолали лише п'ятеро учасників. Застереження було в часі: людям дають дев'ять годин, системі на одну задачу знадобилися дні.
Відомості про подію
- Дата події
- 25 липня 2024 р.
- Дата на часовій осі
- Дата події
- Перевірка
- Джерела зібрано автоматично · 18 вересня 2026 р.
- Лінії
- ID
- evt-0306
Оголошення від 25 липня 2024 року, за результатами олімпіади того року.
Пов’язані події
Раніше
- Розвиває AlphaGeometry 2024
Друга версія тієї самої геометричної системи працювала в цій парі.
- Спирається на AlphaZero 2017
AlphaProof навчається грою проти себе в просторі формальних доведень.
- Уможливлює Числення конструкцій 1986посилається на цей запис
AlphaProof записує задачі в Lean, а ядро Lean, за статтею його авторів 2015 року, дає версію числення індуктивних конструкцій із посиланням на цю роботу.
Пізніше