Штучний інтелект (ШІ) щотижня знаходить рішення нових математичних задач. Минулого місяця OpenAI опублікувала 719 рукописів із запропонованими розв’язками складних проблем. Проте навіть перевірки, призначені для підтвердження результатів, можуть давати збій. Після років необережних результатів роботи ШІ виникає слушне запитання, чи не стане математика наступною жертвою.
Компанія Axiom Math робить ставку на те, що математика зможе уникнути цієї долі, не сповільнюючись, а спираючись на міцніший фундамент. Стартап вартістю 1,6 мільярда доларів прагне створити перевірену основу, на яку ШІ-агенти зможуть покладатися для написання програмного забезпечення, а згодом і для наукових досліджень.
У середу компанія оголосила про офіційне верифікацію Stacks Project — одного з найбільших зібрань математичних робіт, коли-небудь написаних людьми. Математики високо цінують Stacks: математик Колумбійського університету Пітер Войт стверджував, що «немає нічого справді порівнянного», порівнюючи проєкт із «знаменитими книгами Бурбакі» — серією, яка перебудувала математику з її основ у 20-му столітті.
Йохан де Йонг, колега Войта з Колумбійського університету, розпочав Stacks Project у 2005 році як відкритий довідник. З того часу математики роблять внесок у його розвиток, будуючи результати від рівня університетської алгебри до найпередовіших ідей у галузях алгебри, геометрії та теорії чисел.
Парк ШІ-агентів компанії перекладає приблизно 7654 сторінки бібліотеки приблизно на 16 мільйонів рядків коду, перевіреного комп’ютером.
Формалізація математики — це спосіб переконатися, що її структурний каркас є надійним. Математики переписують доведення у вигляді коду на мові програмування Lean, а програма-помічник для доведень перевіряє код рядок за рядком. Якщо доведення проходить перевірку, математики можуть бути впевнені в його логічній обґрунтованості.
Інженери використовують ту саму ідею, відому як формальна верифікація, для підтвердження працездатності дизайнів своїх мікросхем, тоді як дослідники у Франції використовували її для виявлення помилок у програмному забезпеченні, яке розраховує сімейні виплати.
Для такої бібліотеки, як Stacks Project, перевірка кожного теореми — це лише частина роботи. Теореми та визначення в Stacks взаємопов’язані, і кожне з них спирається на попередні. Подібно до генеалогічного дерева, багато результатів у Stacks відстежуються до тих, що передували їм.
Ця взаємопов’язаність спочатку викликала сумніви у Axiom щодо успішності проєкту. Команді довелося зберегти кожне з’єднання цілим у приблизно 16 мільйонах рядків коду Lean.
«Речі, які є великими, і речі, які є делікатними в житті, просто не поєднуються», — сказала CEO Axiom Каріна Хонг TechCrunch. «[Stacks] — це зібрання математичних результатів, яке є фундаментом математики. Ви хочете, щоб [теореми] були послідовними, а не парадоксальними. Ви хочете, щоб визначення не суперечили одне одному».
25-річна CEO покинула аспірантуру з математики Стенфордського університету та заснувала компанію у березні 2025 року. У березні Axiom залучила 200 мільйонів доларів у рамках раунду серії A під керівництвом Menlo Ventures.
«Ми не були впевнені, чи зможе “вайбове кодування” зберегти красу Stacks», — сказала Хонг.
Щоб реалізувати проєкт, команда надала своїм агентам гнучку структуру та дозволила їм працювати паралельно. «З Stacks ми запровадили ієрархію… [але] це не була повна ієрархія, яка диктувала, що робить кожен окремий агент», — сказав Ашвін Свамінатан, співробітник технічного відділу Axiom. «Агенти самі знаходили завдання та визначали, над чим вони могли працювати паралельно».
Axiom також тренувала власні моделі, щоб вони добре працювали з математикою, — підхід, якого, за словами Хонг, не дотримуються більшість інших стартапів у сфері верифікації. Спочатку команда покладалася на одного зі своїх внутрішніх експертів з Lean, щоб навчити агентів людському «смаку». З часом, за словами Хонг, агенти почали самостійно розвивати цей «смак».
Результат заповнює одну з найбільших прогалин у формалізованій математиці. «Коли ви дивитеся на те, що було формалізовано в математиці, існує ця величезна чорна діра. І ця чорна діра охоплює алгебричну геометрію», — сказав Свамінатан.
До цього моменту дослідники, які хотіли перевіряти нові роботи з алгебричної геометрії за допомогою Lean, мали мало з чого почати, зазначив Свамінатан. «Але тепер вони мають».
Axiom стверджує, що кожен верифікований результат стає будівельним блоком, тому майбутні доведення можуть спиратися на перевірену математику, а не починати з нуля. Теренс Тао, математик UCLA та лауреат Філдовської премії, простіше висловив загальну ідею: «Чим більше формалізованих доведень ви маєте, тим більше формалізованих доведень ви можете створити».
Математики — не єдина цільова аудиторія Axiom. Розробники вже давно стикаються з труднощами у гарантуванні того, що їхній код не містить помилок і вразливостей безпеки. Ця проблема зростає, оскільки ШІ-агенти пишуть дедалі більше коду у світі.
Axiom робить ставку на те, що програмне забезпечення майбутнього потребуватиме спиратися на перевірені основи, подібно до того, як це робить Stacks.
«Ми вважаємо, що математика — це сфера, з якої починається побудова цих речей, і що це навичка, яка може бути передана», — сказав Свамінатан. «Агенти можуть читати наш код, розуміти його та створювати нову інфраструктуру на його основі. Наша формалізація Lean тепер є субстратом, на якому агенти можуть будувати».
Спосіб, у який агенти Axiom побудували Stacks, працюючи паралельно та самостійно обираючи завдання, — це те, як Хонг очікує, що відбуватиметься багато майбутньої роботи ШІ. ШІ-агентам, на її думку, знадобиться добре побудований, багаторазовий обсяг знань, щоб уникнути створення низькоякісних результатів.
«Ви хочете, щоб [агенти] мали бібліотеку для багаторазового використання, на якій вони могли б будувати та просувати кордони», — сказала Хонг. «Якщо ви робите погані інженерні рішення на початку, тоді їм буде дуже важко розширювати ці межі».
Хонг настільки впевнена у цьому підході, що кидає виклик: «Я відкрито закликаю всі компанії, що займаються кодуванням, працювати над формалізацією такого масштабу».
Дізнатися більше на: techcrunch.com