AlphaGeometry
Система з мовної моделі та символьного вивідника розв'язала 25 із 30 геометричних задач Міжнародної математичної олімпіади в межах відведеного часу.
Чому це важливо
Рівень майже середнього золотого медаліста — і досягнутий без жодного людського розв'язку в навчальних даних.
Символьний вивідник виводить наслідки з умови, доки не застрягне; тоді мовна модель пропонує допоміжну побудову — додаткову точку чи пряму, — і вивід продовжується. Модель навчали на ста мільйонах синтетичних задач, згенерованих самою системою, без жодного людського доведення. Це поєднання двох традицій, які сорок років конкурували: логічний вивід дає гарантію правильності, навчена модель дає здогад, звідки почати.