Компанијата OpenAI објави серија нови математички резултати и решенија генерирани од нивен интерен напреден модел на вештачка интелигенција. Објавата уследи по консултации со независната Советодавна група за математика и вештачка интелигенција при Институтот за напредни студии во Принстон. Податоците се јавно достапни преку складиште на платформата GitHub, заедно со протоколи за ревизија, цитирање и пресметковни ресурси потрошени за секој обид.
Главниот фокус на оваа објава е формализацијата на чекорите во расудувањето. Наместо само текстуални објаснувања во кои вештачката интелигенција често греши или халуцинира чекори, OpenAI вклучи докази кодирани во програмскиот јазик Lean.
Станува збор за софтверски систем кој овозможува компјутерска проверка на секој поединечен чекор во математичката логика. Од компанијата соопштија дека базата на кодови дополнително ќе се надополнува со нови формализирани докази како што ќе ги завршуваат проверките.
Транспарентноста на истражувањето е надополнета со детални метрики за пресметковната моќ. Документацијата на GitHub содржи десет прегледи на процесот на расудување, статистика за бројот на неуспешни обиди и проценка на ресурсите.
За секој поединечен резултат во просек биле искористени ресурси еднакви на околу три часа непрекинато пресметување на ниво на ChatGPT Pro верзијата. Овие параметри им даваат јасна слика на независните истражувачи колку хардверски капацитет е реално потребен за автоматизирано докажување теореми.
Научниот тим најави дека ќе финансира серија специјализирани конференции, научни работилници и програми посветени на анализа на трудови напишани со машинска помош. Целта е академската заедница директно да ги тестира границите на понудените решенија.
Истовремено, во тек се подготовки за контролирано објавување на самиот модел што ги генерирал овие решенија, со најава за дополнителни научни тестови во други природни науки.