OpenAI залучає зовнішніх експертів до перевірки доказів ШІ з математики, інформатики та фізики

OpenAI повідомляє, що внутрішні моделі ШІ створили докази з математики, інформатики та фізики, зокрема заяву, що центральне припущення в інформатиці є хибним, і заяву, що частину Проблеми тисячоліття було доведено. Компанія звернулася до зовнішніх експертів, зокрема до лауреата Нобелівської премії, щоб ті перевірили результати й вирішили, чи витримують докази критику.

Інформатика: виклик гіпотезі ETH

OpenAI каже, що один результат стосується експоненційної часової гіпотези, або ETH, яка пов'язана з задачею виконуваності булевих формул, відомою як SAT. SAT запитує, чи можна задати значення змінних у логічній формулі так, щоб формула була істинною. ETH стверджує, що реального прискорення немає і що в найгіршому випадку час обчислень зростає експоненційно з додаванням змінних. OpenAI каже, що її система довела хибність ETH. Компанія каже, що це торкнулося б сотень статей, побудованих на ETH, хоча практичні вигоди все ще вимагали б багато досліджень.

Ryan Williams з MIT незалежно перевіряє й пояснює результат разом із Russell Impagliazzo та Ramamohan Paturi з UC San Diego. Група каже, що не має угод про нерозголошення, працює без оплати та планує ділитися проміжними висновками. У відкритому листі троє кажуть, що їхня участь не є схваленням. OpenAI публікує письмовий доказ і доказ у Lean, а також зобов'язалася фінансувати конференцію за цим результатом.

Математика: локальне згладжування в усіх вимірах

Математичний результат стосується гіпотези локального згладжування, яку запропонував Christopher Sogge в 1991 році. Гіпотеза каже, що екстремальна концентрація хвиль триває лише коротко, тому хвилі поводяться більш гладко, коли їх усереднюють за часом. Її довели у двох вимірах Guth, Wang і Zhang у 2019 році. OpenAI каже, що її моделі тепер створили доказ для кожного виміру. За словами OpenAI, результат також доводить гіпотезу Kakeya і гіпотезу обмеження Stein в усіх вимірах. OpenAI каже, що жодна спеціальна група не супроводжує цей доказ. Після звернення до зовнішнього експерта компанія опублікувала текст доказу та доказ у Lean безпосередньо, щоб дослідники самі вирішили, як перевіряти результат.

Фізика: існування квантової теорії поля

Фізичний результат стосується квантової теорії поля, яку OpenAI називає найважливішим каркасом сучасної теоретичної фізики. OpenAI каже, що її ШІ довів існування певних квантових теорій поля у чотирьох вимірах. Доказ охоплює теорію Yang-Mills, квантову хромодинаміку та найпростішу теорію великого об'єднання. Щодо Yang-Mills OpenAI каже, що розв'язано лише частину про існування, а не масову щілину, тому Проблему тисячоліття не буде повністю розв'язано.

Групу, яка супроводжуватиме роботу, очолює David Gross. Gross розділив Нобелівську премію з фізики 2004 року. До групи також входять Michael Douglas, Arthur Jaffe, Igor Klebanov і Nikita Nekrasov. OpenAI каже, що переклала доказ Yang-Mills мовою Lean, але ця група наразі не оприлюднює матеріали ШІ і планує самостійно оформити результат.

Процес перевірки та визнання

OpenAI каже, що не претендує на наукове визнання і що визнання має дістатися групам, які пояснюють результати. Компанія також визнає компроміси, зокрема те, що той, хто обирає перших супроводжувачів, допомагає вирішити, хто долучиться першим. OpenAI каже, що ще не зрозуміло, який підхід до перевірки працює найкраще.

Джерела: The Decoder