Учора OpenAI опублікувала одразу 722 рукописи з ШІ-математики, а щойно відкликала 3 з них.
Причина проста: було неправильно написано знак плюс-мінус.
Щойно OpenAI опублікувала свій перший журнал оновлень у репозиторії openai/math. Журнал показує, що OpenAI відкликала 3 рукописи, виправила 14 і оновила посилання ще для 13. Загальна кількість рукописів у репозиторії впала з 722 до 719.
Один знак плюс-мінус знищує три статті
Три відкликані статті всі пов'язані з гіпотезою Ходжа, однією з проблем тисячоліття:
Алгебраїчність класів Вейля на розщеплених абелевих восьмивимірних многовидах
Алгебраїчність відповідностей Куґи–Сатаке для поверхонь K3
Раціональна гіпотеза Ходжа для добутків поверхонь K3
Проблема полягає в першій статті. У записці про відкликання OpenAI написала, що в ключовому аргументі стаття зафіксувала знак певної геометричної операції як +1, тоді як згідно з власною конвенцією статті він має бути -1.
https://github.com/openai/math/blob/main/history.md
Плюс проти мінуса створює величезну різницю. Підрахунок, який мав скоротитися і врешті-решт дорівнювати нулю, став ненульовим числом. Класична теорема, на яку спирається стаття, має як передумову саме те, що цей підрахунок має дорівнювати нулю. Коли передумова не виконується, вся подальша конструкція втрачає підґрунтя.
Дві інші статті обидві запозичили цю конструкцію, тому їх також відкликали.
Однак у всіх трьох записах про відкликання OpenAI підкреслила одне й те саме речення: відкликається доведення, що не означає, що самі ці математичні твердження є хибними. Оригінальні рукописи також не були видалені, і їх все ще можна переглянути за архівними посиланнями.
Ці три статті всі належать до сімейства результатів репозиторію № 032, тобто до раніше найбільш пильно відстежуваних результатів, пов'язаних з гіпотезою Ходжа.
Після відкликання назва цього сімейства також змінилася: з "Результати Ходжа та Куґи–Сатаке для всіх проєктивних поверхонь K3" на "раціональна гіпотеза Ходжа для CM абелевих многовидів".
Іншими словами, частину висновків, що стосуються поверхонь K3, було вилучено зі списку. Основне твердження цього сімейства, а саме доведення раціональної гіпотези Ходжа для всіх комплексних CM абелевих многовидів, все ще збережено, і нова версія цієї статті лише оновила посилання.
Варто зазначити, що стаття з помилкою датована 18 вересня, що робить її однією з найраніших партій рукописів у репозиторії. Від її дати до публічного випуску минуло майже три тижні, і її було відкликано протягом одного-двох днів після публікації. Щодо того, хто виявив помилку, OpenAI не повідомила.
Ще 14 статей було переглянуто
Окрім відкликань, OpenAI також переглянула 14 рукописів, зокрема виправлення доведень, коригування формулювань висновків та уточнення передумов і залежностей.
Ці 14 стосуються висот Ліпшиця та моделі Ашкіна–Теллера у статистичній фізиці (4 статті), програми мінімальних моделей Келера та достатку в комплексній геометрії (6 статей), симплектичної геометрії (2 статті), загального обчислення для рідин Нав'є–Стокса (1 стаття) та однієї статті про формулу BSD, з якої було видалено застарілі цитати.
Один перегляд є досить показовим. Родина результатів № 342 стверджувала, що доводить гіпотезу «сумісності тамерного просування вперед», запропоновану Саймоном Дональдсоном. Основний висновок не змінився, і є формалізація Lean. Але було виявлено, що сильніший побічний висновок у статті було перебільшено: переглянута версія звужує його до конкретного випадку, а також додає приклад, який показує, що він не виконується в загальному випадку.
Рівень формалізації: 42%
Оновлення також додало 6 формалізацій Lean і 5 додаткових допоміжних результатів. Згідно з підрахунками OpenAI, основні результати 300 рукописів наразі формалізовано, що становить близько 42% від усіх 719.
Серед новододаних формалізацій кілька мають значну вагу, наприклад, 103-тя родина досягнень у теоретичній інформатиці, яка стверджує, що доводить повну дерандомізацію обчислень у логарифмічному просторі (L = RL = BPL).
Слід зазначити, що «близько шістдесяти відсотків», про які ми повідомляли раніше, підраховувалися за родинами досягнень, тобто якщо хоча б одна стаття в родині має формалізацію, вона зараховується; 42%, оголошені OpenAI, підраховуються за окремими основними результатами, що краще відображає фактичну частку, яку було перевірено комп'ютером рядок за рядком.
Там, де виникають помилки, немає нагляду Lean
Порівняння з каталогом репозиторію виявляє закономірність: вміст, який цього разу було відкликано та суттєво переглянуто, майже весь припадає на частини без формалізації Lean.
Це також підтверджує попереднє нагадування математичної спільноти: результати, які не пройшли формалізацію та рецензування, наразі можна розглядати лише як «твердження».
На щастя, цю erratum було опрацьовано досить належно: помилки було чітко викладено, ланцюжок залежностей пояснено, а стару версію збережено для довідки, що відповідає принципу «виправлення зі слідом», рекомендованому Консультативною групою з математики та штучного інтелекту Інституту перспективних досліджень.
Однак лише через два дні після оприлюднення понад 700 рукописів надійшла перша erratum. Це, найімовірніше, не остання.
Ця стаття походить із публічного акаунта WeChat «Machine Heart» (ID: almosthuman2014), редактор: Panda
