Влад Тенев, генеральний директор торгової платформи Robinhood, оголоcив про створення Harmony, комерційної дослідницької лабораторії штучного інтелекту. Ініціатива буде спрямована на створення так званого “математичного надінтелекту” (Mathematical Superintelligence або MSI), ШІ з можливостями математичного міркування, що перевершують можливості людей.
Як зазначається у нитці публікацій Тенева, сучасні великі мовні моделі здатні створювати тексти, які звучать по-людськи, але можуть видавати помилкові твердження. Математика ж дозволяє чітко визначати та узгоджувати спільну істину, тому і є основою для всіх наукових відкриттів.
За словами керівника Robinhood, Harmonic планує безпосередньо розв’язувати проблему помилок в моделях штучного інтелекту шляхом включення математики “як примітиву”. Це дозволить створити надзвичайно корисний інструмент для всього людства, результати роботи якого будуть достовірно правильними і перевіреними, без помилкових тверджень.
Тенєв обійматиме посаду виконавчого голови Harmonic, а керівником компанії буде Тудор Ахім. Керівник Robinhood підкреслив, що ця ініціатива ніяк не пов’язана з фінтехом, співзасновником якої є Тенєв, а його діяльність в Harmonic ні в якому разі не буде операційною.
На сайті проєкту зазначається, що моделі, здатні до формальних математичних міркувань, гарантуватимуть правильність результатів з інтерпретованим ланцюжком міркувань. Такий підхід буде застосовний у таких критичних галузях, як аерокосмічна, розробка мікросхем, промислові системи та охорона здоров’я.
Першим дослідницьким результатом Harmonic став Aristotle — автоматизований засіб доведення теорем, що розвиває сучасні технології на MiniF2F. Цей тест вимірює здатність розв’язувати проблеми різної складності, включаючи завдання Міжнародної математичної олімпіади.
Aristotle досягає 83% успіху, коли йому дозволяється використовувати додаткові зовнішні системи комп’ютерної алгебри для вирішення простих підзадач, і 63% успіху при обмеженні внутрішньою мовою Lean. Порівнюючи результати проходження MiniF2F, Aristotle перевершив два попередні сучасні підходи.
