Вперше система зі штучним інтелектом, призначена для перевірки математичних доказів, виявила фундаментальну помилку в науковій статті з фізики, що рецензується. Це відкриття, зроблене Джозефом Тубі-Смітом з Університету Бата, підкреслює стурбованість, що зростає: скільки подібних помилок може існувати в існуючій науковій літературі? Ця подія демонструє потенціал автоматизованих інструментів перевірки для перетворення академічної публікації та підвищення надійності наукових висновків.
Розквіт формальної верифікації
Формальна верифікація – процес суворої перевірки математичної та логічної несуперечності – стає все більш поширеною в математиці. Спеціалізоване програмне забезпечення, таке як мова Lean, використана в цьому випадку, може виявляти протиріччя та прогалини у доказах, які можуть пропустити людські рецензенти. Цей підхід спрямований не лише на виявлення помилок, а й розглядається як спосіб вирішення особливо складних проблем, таких як невирішена гіпотеза ABC, де навіть експерти розходяться у думках щодо обґрунтованості запропонованих рішень.
Фізика під мікроскопом
Тубі-Сміт застосував формальну верифікацію до статті 2006 року про стабільність потенціалу моделі двох дублетів Хіггса (2HDM), що широко цитується у фізиці частинок. Метою було інтегрувати статтю до PhysLib, проект, спрямований на створення формалізованої бази даних фізичних досліджень за аналогією з успішним MathsLib для математики. Штучний інтелект показав, що ключова умова, представлена в оригінальній статті, не гарантувала стабільного рішення, як стверджували автори.
Відкриття був навмисною спробою дискредитувати роботу. Як пояснює Тубі-Сміт, команда прагнула “формальної вправи”, щоб створити надійну бібліотеку формалізованої фізики. Однак виявлена помилка порушує важливе питання: якщо стаття, що добре цитується, може містити таку помилку, то скільки інших можуть бути настільки ж помилковими?
Чому це важливо
Фізика спирається на математичну строгість, але фізики часто віддають пріоритет результатам, а чи не вичерпної деталізації. На відміну від математиків, які зазвичай надають явні кроки докази, фізики можуть опускати, начебто, незначні деталі, які, як свідчить цей випадок, можуть підірвати обгрунтованість теореми. Ця різниця в практиці означає, що фізичні статті потенційно більш вразливі до недосліджених помилок.
Майбутнє наукової перевірки
Наслідки цього відкриття є значними. Хоча помилка навряд чи дискредитує подальші роботи, які посилаються на статтю (нині готується виправлення), вона зміцнює аргумент на користь інтеграції формальної верифікації до стандартного процесу публікації.
Кевін Баззард з Імперського коледжу Лондона зазначає, що формалізація вже перетворила математику, і немає причин, через які теоретична фізика не може отримати користь із того ж підходу. Проте проблема полягає у створенні досить великого корпусу формалізованих фізичних даних для ефективного навчання моделей штучного інтелекту. “В ідеалі нам потрібен мільйон рядків фізичного коду… якщо машини спочатку недостатньо добре знаються на фізиці, то спочатку буде потрібно ручна робота”, – каже Баззард.
Автоматизована верифікація готова стати важливим інструментом забезпечення наукової точності. Хоча початкові зусилля можуть бути трудомісткими, довгострокові переваги більш надійного наукового обліку є незаперечними.
