DeepMind достига основен камък в решението на математическите проблеми - следващото голямо предизвикателство за AI

Изследователите са постигнали смесени резултати, когато отговарят на математически въпроси с гласови модели - типът система, която води чатботи като Чат. Понякога моделите дават правилния отговор, но не могат да обяснят разсъжденията си рационално, а понякога

Само миналата седмица екип от софтуерни компании Numina и Huggingface използваха гласов модел, за да спечелят междинна „цена на напредъка“, базирани на опростени версии на IMO проблеми. Компаниите направиха цялата си система с отворен код и го предоставиха за изтегляне на други изследователи. Но победителите казаха природа , че само езиковите модели вероятно няма да са достатъчни за решаване на трудни проблеми.

Alphaproof комбинира гласов модел с технологията на засилване на обучението, което „Alphazero“ двигателят за игри за атака, като GO, както и някои Специфични математически проблеми . С увеличаването на обучението невронната мрежа се учи чрез експерименти и грешки. Това работи добре, ако отговорите му могат да бъдат оценени с помощта на обективна скала. За тази цел Alphaproof беше обучен да чете и пише доказателства на официален език, наречен Lean, който се използва в софтуерния пакет „Proof Assistant“ със същото име, който е популярен сред математиците. За това Alphaproof тества дали разходите му са правилни, като ги прави в пакета Lean, което помогна за попълването на някои от стъпките в кода.

Обучението на гласов модел изисква огромни количества данни, но в Lean бяха налични само няколко математически доказателства. За да преодолее този проблем, екипът разработи допълнителна мрежа, която се опита да преведе съществуващ запис на един милион проблеми, написани на естествен език, но без да превежда решения, написани в Lean, казва Томас Хюбърт, изследовател на DeepMind Machine, който е провел развитието на Alphaproof. "Можем да се научим да доказваме нашия подход, дори и първоначално да не сме обучили за доказателства, написани от хора?" (Компанията беше подобна на GO, където неговият AI се научи да играе играта, като играе срещу себе си, вместо начина, по който го правят хората.)

магически ключ

Много от стройните преводи нямаха смисъл, но достатъчно бяха достатъчно добри, за да доведат Alphaproof до момента, в който може да започне своите нарастващи цикли на обучение. Резултатите бяха много по -добри от очакваното, каза Gowers от консултацията по пресата. "Много проблеми с IMO имат това свойство на магическия ключ. Проблемът първо изглежда трудно, докато не намерите магически ключ, който го отваря", каза Гоуърс, който работи в Collège de France в Париж.

В някои случаи Alphaproof изглежда беше в състояние да предприеме тази допълнителна стъпка на креативност, като му даде правилна стъпка от безкрайно голямо възможно решение. Но е необходим допълнителен анализ, за ​​да се определи дали отговорите са по -малко изненадващи, отколкото изглеждаха, добавиха Gowers. Подобен дискурс възникна след изненадващия 'zug 37' , DeepMinds Alphago-Bot в неговия Известна победа през 2016 г. за най-добрия играч на човешкия Go в света --А повторна точка за KI.

Остава да се види дали техниките могат да бъдат усъвършенствани, за да работят на ниво изследвания по математика, каза Майерс от пресата за пресата. "Може ли да се разшири до други видове математика, където не могат да се обучават милиони проблеми?"

"Ние стигнахме до момента, в който не само можете да докажете отворени изследователски проблеми, но и проблеми, които са много предизвикателни за най-добрите млади математици в света", заяви компютърният специалист на DeepMind Дейвид Силвър, който беше водещ изследовател в развитието на Alphago в средата на 2010 г.