Denis Ignatovich, współzałożyciel i współprezes Imandry – seria wywiadów

Denis Ignatovich, współzałożyciel i współprezes Imandry, ma ponad dekadę doświadczenia w handlu, zarządzaniu ryzykiem, modelowaniu ilościowym i projektowaniu złożonych systemów handlowych. Przed założeniem Imandry kierował centralnym biurem zarządzania ryzykiem w Deutsche Bank (DB ) London, gdzie uznał kluczową rolę, jaką może odegrać sztuczna inteligencja w sektorze finansowym. Jego spostrzeżenia w tym czasie pomogły ukształtować gamę produktów finansowych Imandry. Wkład Denisa w dziedzinie logiki obliczeniowej dla platform handlowych obejmuje kilka patentów. Ukończył studia magisterskie z finansów na London School of Economics oraz studia licencjackie z informatyki i finansów na Uniwersytecie Teksasu w Austin.

Imandra to silnik rozumnego wnioskowania oparty na sztucznej inteligencji, który wykorzystuje neurosymboliczną sztuczną inteligencję do automatyzacji weryfikacji i optymalizacji złożonych algorytmów, szczególnie w handlu finansowym i systemach oprogramowania. Łącząc wnioskowanie symboliczne z uczeniem maszynowym, zwiększa bezpieczeństwo, zgodność i wydajność, pomagając instytucjom zmniejszyć ryzyko i poprawić przejrzystość w podejmowaniu decyzji z użyciem sztucznej inteligencji.

Czym było inspiracją dla ciebie i dra Granta Passmore, by założyć Imandrę, i jak twoje doświadczenie wpłynęło na wizję firmy?

Po ukończeniu studiów zacząłem pracę w handlu ilościowym i skończyłem w Londynie. Grant ukończył studia doktoranckie w Edynburgu, a następnie przeniósł się do Cambridge, aby pracować nad zastosowaniami automatycznego wnioskowania logicznego do analizy bezpieczeństwa systemów autopilotów (złożonych algorytmów, które obejmują nieliniową obliczeniowość). W mojej pracy również zajmowałem się złożonymi algorytmami z wieloma nieliniowymi obliczeniami i zrozumieliśmy, że istnieje głębokie połączenie między tymi dwoma dziedzinami. Sposób, w jaki finanse tworzyły takie algorytmy, był naprawdę problematyczny (jak podkreślały wiele artykułów prasowych dotyczących „błędów algorytmicznych”), więc postanowiliśmy to zmienić, wyposażając inżynierów w finansach w automatyczne narzędzia logiczne, aby wprowadzić rygorystyczne techniki naukowe do projektowania i rozwoju oprogramowania. Jednak to, co ostatecznie stworzyliśmy, jest niezależne od branży.

Czy możesz wyjaśnić, co to jest neurosymboliczna sztuczna inteligencja i jak różni się od tradycyjnych podejść do sztucznej inteligencji?

Dziedzina sztucznej inteligencji składa się (bardzo ogólnie!) z dwóch obszarów: statystycznego (który obejmuje LLM) i symbolicznego (znany również jako automatyczne wnioskowanie). Statystyczna sztuczna inteligencja jest niesamowita w identyfikowaniu wzorców i tłumaczeniu przy użyciu informacji, które nauczyła się z danych, na których została wyszkolona. Ale jest słaba w wnioskowaniu logicznym. Symboliczna sztuczna inteligencja jest prawie dokładnym przeciwieństwem – zmusza do bycia bardzo precyzyjnym (matematycznie) w tym, co się robi, ale może używać logiki do wnioskowania w sposób, który jest (1) logicznie spójny i (2) nie wymaga danych do szkolenia. Techniki łączące te dwie dziedziny sztucznej inteligencji nazywają się „neurosymbolicznymi”. Jednym z najbardziej znanych zastosowań tego podejścia jest projekt AlphaFold z DeepMind, który niedawno otrzymał Nagrodę Nobla.

Co, Twoim zdaniem, wyróżnia Imandrę na czele rewolucji neurosymbolicznej sztucznej inteligencji?

Istnieje wiele niesamowitych symbolicznych wnioskowań dostępnych (większość w akademii) skierowanych do określonych nisz (np. składania białek), ale Imandra wyposaża deweloperów w możliwość analizy algorytmów z niezwykłą automatyzacją, co ma znacznie szersze zastosowanie i większą grupę docelową niż te narzędzia.

Jak Imandra eliminuje powszechne wyzwania sztucznej inteligencji, takie jak halucynacje, i poprawia zaufanie do systemów sztucznej inteligencji?

W naszym podejściu LLM są używane do tłumaczenia żądań ludzi na logikę formalną, która jest następnie analizowana przez silnik wnioskowania z pełnym śladem logicznym. Chociaż mogą wystąpić błędy tłumaczenia podczas korzystania z LLM, użytkownik otrzymuje logiczne wyjaśnienie, w jaki sposób żądania zostały przetłumaczone, a audyty logiczne mogą być weryfikowane przez oprogramowanie open source. Naszym ostatecznym celem jest wprowadzenie przejrzystości działania, w którym systemy sztucznej inteligencji mogą wyjaśniać swoje wnioskowanie w sposób, który jest niezależnie logicznie weryfikowalny.

Imandra jest używana przez Goldman Sachs (GS ) i DARPA, między innymi. Czy możesz podzielić się prawdziwym przykładem, jak twoja technologia rozwiązała złożony problem?

Wspaniałym przykładem realnego wpływu Imandry jest nasze zwycięstwo w konkursie UBS Future of Finance (szczegóły z kodem Imandry znajdują się na naszej stronie). Podczas tworzenia studium przypadku dla UBS, które zakodowało dokument regulacyjny, który został złożony do SEC, Imandra wykryła fundamentalną i subtelną wadę w opisie algorytmu. Wada wynikała z subtelnych warunków logicznych, które muszą być spełnione w celu rangowania zamówień w książce zamówień – coś, co byłoby niemożliwe do wykrycia przez ludzi „ręcznie”. Bank nagrodził nas pierwszym miejscem (spośród ponad 620 firm na całym świecie).

Jak twoje doświadczenie w Deutsche Bank wpłynęło na zastosowania Imandry w systemach finansowych, a jaki jest najbardziej wpływowy przypadek użycia, jaki widziałeś do tej pory?

W Deutsche Bank zajmowaliśmy się wieloma złożonymi kodami, które podejmowały automatyczne decyzje handlowe na podstawie różnych danych wejściowych ML, wskaźników ryzyka itp. Jak każdy bank, musieliśmy również przestrzegać licznych regulacji. To, co Grant i ja zrozumieliśmy, to fakt, że jest to matematycznie bardzo podobne do badań, które prowadził nad bezpieczeństwem autopilotów.

Poza finansami, które branże, Twoim zdaniem, mają największy potencjał, aby skorzystać na neurosymbolicznej sztucznej inteligencji?

Widzieliśmy, jak AlphaFold otrzymał Nagrodę Nobla, więc zdecydowanie możemy to policzyć… Ostatecznie większość zastosowań sztucznej inteligencji będzie korzystać z użycia symbolicznych metod, ale konkretnie pracujemy nad następującymi agentami, które zostaną wydane wkrótce: analiza kodu (tłumaczenie kodu źródłowego na modele matematyczne), tworzenie rygorystycznych modeli z angielskich specyfikacji, wnioskowanie o modelach SysML (język używany do opisu systemów w branżach krytycznych dla bezpieczeństwa) i automatyzacja procesów biznesowych.

Imandra’s region decomposition to nowa funkcja. Czy możesz wyjaśnić, jak działa i jakie jest jej znaczenie w rozwiązywaniu złożonych problemów?

Pytanie, o które każdy inżynier myśli, pisząc oprogramowanie, to „jakie są przypadki brzegowe?”. Kiedy ich praca polega na QA i muszą pisać przypadki testowe lub piszą kod i myślą o tym, czy poprawnie zaimplementowali wymagania. Imandra wprowadza naukową rygorystyczność, aby odpowiedzieć na to pytanie – traktuje kod jako model matematyczny i symbolicznie analizuje wszystkie przypadki brzegowe (tworząc dowód o kompletności pokrycia). Ta funkcja opiera się na technice matematycznej zwanej „cylindryczną dekompozycją algebraiczną”, którą „podniesiono” do algorytmów w ogóle. Zapisano niezliczone godziny naszym klientom w finansach i ujawniono krytyczne błędy. Teraz wprowadzamy tę funkcję do inżynierów na całym świecie.

Jak Imandra integruje się z dużymi modelami językowymi, a jakie nowe możliwości to otwiera dla generatywnej sztucznej inteligencji?

LLM i Imandra współpracują, aby sformalizować dane wejściowe ludzi (czy to kod źródłowy, angielski, itp.), aby wnioskować o nich, a następnie zwrócić dane wyjściowe w sposób łatwy do zrozumienia. Używamy ramowych frameworków (np. Langgraph), aby zorganizować tę pracę i dostarczyć doświadczenie jako agent, którego nasi klienci mogą używać bezpośrednio lub integrować z ich aplikacjami lub agentami. Ten symbiotyczny przepływ pracy rozwiązuje wiele wyzwań związanych z używaniem tylko narzędzi LLM i rozszerza ich zastosowanie poza wcześniej widziane dane szkoleniowe.

Jakie jest twoje długoterminowe wizja dla Imandry, i jak widzisz, jak zmieni ona zastosowania sztucznej inteligencji w różnych branżach?

Uważamy, że techniki neurosymboliczne będą fundamentem, który otworzy drogę do realizacji obietnic sztucznej inteligencji. Techniki symboliczne są brakującym składnikiem dla większości przemysłowych zastosowań sztucznej inteligencji, i jesteśmy podekscytowani, że jesteśmy na czele tego następnego rozdziału sztucznej inteligencji.

Dziękujemy za wspaniały wywiad, czytelnicy, którzy chcą dowiedzieć się więcej, powinni odwiedzić Imandrę.