Об авторе: Анатолий Шалыто, профессор, д.т.н., Университет ИТМО
Мне некоторое время назад стало известно о существовании стартапа Logical Intelligence («Логический интеллект»). Его лозунгом является выражение: «100% correct AI formal reasoning, 100% of the time» (100% правильные формальные рассуждения ИИ в 100% случаев). Область применения: программное обеспечение ответственных систем.
Его организовали чемпион мира по программированию ICPC и его жена – PhD по квантовой физике. Они привлекли к работе двукратных чемпионов мира по программированию ICPC, которых в мире всего девять человек, причем все из России, четверо – из университета ИТМО), призёров международных студенческих соревнований по программированию, признанных лидеров в области криптографии и проблем безопасности, PhD в области математики, информатики и квантовой физики. В команду также входит обладатель самой высокой награды по математике – премии Филдса. В конце титульной страницы указанного выше сайта сказано: Ready to trust and verify? (Готовы доверять и проверять?)
Команда стартапа видит свою задачу в том, чтобы использовать математику для обеспечения безошибочности ИИ.
- Ева Бодня. Founder и Chief Executive Officer (CEO). Образование: University of California (UC), Berkeley. PhD’2025 in Quantum Information and Algebraic Topology Applications (UC Santa Barbara). Научное взаимодействие: Princeton University, Harvard University.
- Михаил Рубинчик. Chief Technology Officer (CTO). ACM ICPC Bronze Medalist (2011). Сoach of three ICPC medalist teams (2016, 2017, 2018), mentor to two International Olympiad in Informatics (IOI) medalists (2014, 2020). PhD’2016 in Theoretical Computer Science.
- Владислав Исенбаев. Chief of AI (CAIO). Чемпион мира по программированию по версии ACM ICPC (2009). Бронзовый медалист Google Code Jam (2013).
- Майкл Фридман. Chief Science Officer (CSO). В 1986 году удостоен Филдсовской премии за работу над обобщённой гипотезой Пуанкаре. Индустриальный опыт: Microsoft Station Q, Google Quantum AI. Видимо, был научным руководителем PhD Евгении Бодни.
В команду также входят Евгений Капун – двукратный чемпион мира ACM ICPC (2009, 2012), исследователь, Михаил Кевер – двукратный чемпион мира ACM ICPC (2012, 2013), исследователь, Виталий Аксёнов – исследователь, Михаил Миллиган – исследователь. Всего в команде 16 человек.
Имеется информация о том, что командой заинтересовался один из основоположников глубокого обучения Ян ЛеКун. Вот мой текст про него.
Цель стартапа: «Создание систем ИИ, способных строго обосновывать свои рассуждения. Эта работа находится на стыке формальной логики и глубокого обучения, создавая надёжные механизмы рассуждения, готовые к внедрению в реальных условиях».
Стартап использует формальную верификацию. При этом ключевая технология базируется на преобразовании заданного кода в код на формальном языке доказательств LEAN4. Это позволяет математически доказывать корректность работы кода с точностью 100%. Такой подход полностью исключает наличие ошибок, в отличие от традиционных методов тестирования и анализа, которые не дают абсолютной гарантии отсутствия багов.
У команды есть собственная AI-модель Aleph, которая автоматически генерирует доказательство корректности, а также агент Noa, который проверяет существующий код на наличие ошибок. Система обеспечивает масштабируемость, сокращая время и затраты на ручную проверку, поскольку автоматизирует до 90% процесса с обязательным контролем со стороны человека. Технологии компании ориентированы на безопасность и надёжность кода в ответственных системах – например, в смарт-контрактах и системах с автопилотом.
В статье «Стартап математических гениев предлагает новый способ проверки работоспособности кода ИИ» сказано, что стартапы, такие как Harmonic AI и недавно запущенный Logical Intelligence, продвигают для обеспечения безошибочного кода модели ИИ, связанные с «формальной верификацией».
Расскажу об этих стартапах в порядке упоминания. Первому из них посвящена статья «Математический стартап генерального директора Robinhood оценивается почти в 900 миллионов долларов».
Harmonic AI – стартап в области ИИ, посвящённый математике. Его соучредителем является Влад Тенев (выпускник факультета математики Стэнфорда). Он генеральный директор известной компания Robinhood Markets Inc. Тенев сначала привлёк 75 миллионов долларов от инвестиционных фондов Sequoia и Index Ventures, а затем ещё 100 миллионов. Второй раунд финансирования возглавил фонд Kleiner Perkins при участии таких фондов как Sequoia Capital, Index Ventures и Paradigm. После этого стартап стал оцениваться в 875 миллионов долларов.
Это чуть ниже порога в $1 млрд, который сделал бы его «единорогом». Таков был преднамеренный выбор: «Мы не хотели принимать более выгодные предложения», – сказал Тенев, который собрал миллиарды в финансировании на Robinhood до первичного публичного размещения акций в 2021 году.
Генеральным директором этого стартапа является Тюдор Ахим, который ранее руководил стартапом по автономному вождению автомобиля.
Harmonic AI, основанный в 2023 году Теневом и Ахимом, стремится создавать системы ИИ, которые компания называет математическим суперинтеллектом для решения сложных математических задач. Стартап планирует сделать свою флагманскую модель Aristotle, доступной для исследователей в конце этого года. Указанная модель на International Mathematical Olympiad (IMO) 2025 года набрала достаточно баллов, чтобы получить золотую медаль.
«Наша ближайшая цель состоит в том, чтобы создать ИИ, который решает математические задачи на уровне, превосходящем любого человека, а следующая цель – это решение нерешённых математических задач, и их связь с проблемами физики и информатики» – сказал Тенев.
Harmonic использует математический подход, который должен дать преимущество перед большими языковыми моделями. Стартап стремится устранить проблему галлюцинаций, полагаясь на формальную верификацию. В этой модели проверяется каждый кусок вывода и каждый шаг в рассуждениях. Это совершенно другой подход к созданию моделей ИИ по сравнению с используемым сегодня. Тенев предполагает, что этот подход будет доминировать в будущем.
Теперь настала пора более подробно рассказать о Logical Intelligence – стартапе, идеологически близком рассмотренному. Известна фраза из фильма «Марсианин»: «Перед лицом превосходящих сил у меня остаётся только один выбор: мне придётся разгребать это дерьмо с помощью науки». Этим же занимается и стартап для улучшения качества генерируемого кода с помощью ИИ.
Журналист, написавший статью об этих двух стартапах, использующих формальную верификацию, беседовал с упомянутой выше Евой Бодней у Центра математических наук и приложений исследовательского центра Гарвардского университета, где она и часть её команды проводили ужин с Яном ЛеКуном! Она рассказала журналисту об основной проблеме больших языковых моделей на основе генеративного ИИ, которая состоит в том, что, несмотря на то, что модели становятся все более мощными, генерируемый ими код по-прежнему опасен для определённых случаев использования.
Logical Intelligence надеется решить эту проблему с помощью «формальной верификации». Для этого была создана модель с таким же названием, которая позволяет ИИ-агенту Aleph преобразовывать код длиной даже в десятки тысяч строк для возможности математических доказательств [его корректности].
Вот как стартап видит свою миссию: «Традиционные авторегрессионные модели LLM (Claude, ChatGPT-5, DeepSeek) ненадёжны для формальных рассуждений из-за галлюцинаций. Они требуют длительного и дорогостоящего времени вычислений».
Указанные модели формируют свой ответ по одному токену за один раз, причем каждый новый токен представляет собой статистическое предсказание, основанное на последовательности, которая ему предшествовала. Для прозы это мощный метод, позволяющий моделям генерировать плавный и связный текст. Однако для математических рассуждений этот подход принципиально ненадёжен. Модель не выполняет логическую дедукцию, а дополняет шаблон. Она действует как эксперт-лингвист-импровизатор, а не как логик, выводящий заключение.
Такие модели имеют критическую уязвимость: один неверный токен, сгенерированный на ранней стадии цепочки рассуждений – будь то неверный расчёт или едва заметная логическая ошибка –может необратимо сорвать весь процесс. Модель не имеет внутреннего механизма распознавания этой ошибки. Вместо этого она продолжает генерировать наиболее вероятные следующие токены на основе уже имеющей дефекты истории, что приводит к каскаду ошибок, делающих окончательный ответ недействительным. Структурированный возврат или восстановление отсутствуют.
Архитектура, обозначенная разработчиками стартапа как LI-1.0, позволяет ИИ проводить аудит, пересмотр, масштабирование по мере усложнения и верификацию подобно сверхразумному эксперту-математику, предоставляя более быстрые, надёжные и математически доказуемые правильные решения, делая ошибки невозможными.
Указанная архитектура сочетает не-авторегрессивные рассуждения, «энергетическое» моделирование и собственный интеграционный уровень, оптимизированный для формальных инструментов верификации, таких как Lean4, что опять-таки исключает математические ошибки.
Не-авторегрессивные рассуждения допускают глобальное уточнение и пересмотр промежуточных шагов, позволяя модели исправлять предыдущие ошибки и поддерживать связные и корректные цепочки рассуждений. Благодаря использованию методов вывода, основанных, например, на итеративном уточнении и параллельной выборке, может быть осуществлен возврат, оценка и глобальная корректировка возможных решений.
Это соответствует человеческому подходу к решению задач: предложение полных траекторий рассуждений, оценка их согласованности и выбор лучших. Такой подход позволяет также обеспечивать параллельный вывод, что отличает его от традиционных строго последовательных рассуждений, которые становятся узким местом в длинных доказательствах. Новый подход не только повышает точность, но и значительно сокращает время вывода, предоставляя результаты на несколько порядков быстрее, а, следовательно, и дешевле.
В результате перестраиваются основы логического интеллекта, открывая доступ к рассуждениям, которым можно доверять и проверять».
Несмотря на изложенное, некоторые эксперты по ИИ скептически относятся к тому, что по мере разработки ведущими компаниями в области ИИ более совершенных моделей рассуждений, формальные математические подходы, применяемые Harmonic и Logical Intelligence, будут широко востребованы.
Мнение скептиков основано в том числе и на следующих фактах: «На IMO 2025 экспериментальная модель от OpenAI смогла полностью решать пять из шести задач, что соответствует золотой медали и привести доказательства на обычном языке, в то время как на IMO 2024 задачи требовалось сначала перевести на «проверяемый» язык, а вместо человеко-читаемого доказательства каждой задачи оно выдавалось на языке Lean, который позволяет автоматически проверить его правильность. Этот результат соответствовал серебряной медали.
Все это так, но «караван», и не один, использующий новые подходы, продолжает идти…
А теперь вопрос: в чём причина написания этого текста? Ответ прост: четверо из участников стартапа Logical Intelligence бывшие студенты кафедры «Компьютерные технологии» университета ИТМО. Это Владислав Исенбаев (его бакалаврская работа «Разработка системы секвенирования ДНК с использованием paired-end данных» (2010), выполненная под моим руководством, приведена здесь), Евгений Капун (его бакалаврская работа «Разработка метода сравнения нуклеотидных последовательностей путём разбиения на фрагменты» (2010), выполненная под моим руководством, приведена здесь), Михаил Кевер (его магистерская диссертация «Теоретическое исследование вычислительной сложности задачи Jump-K» (2014), выполненная под руководством профессора В.Г. Парфёнова, приведена здесь) и Виталий Аксёнов – PhD’2018 in Computer Science: «Synchronization Cost in Parallel Programs and Concurrent Data Structures». Universite Paris-Diderot (L’Ecole Doctorale Sciencе Mathématiques de Paris Center) и ITMO University. Я был соруководителем этой работы.
А ещё я помню, как несколько раз общался с Евой Бодней, CEO компании. В то время она была студенткой физического факультета ИТМО. Ева сказала мне, что хочет перейти на физфак СПбГУ, во что я поверил. Потом она что-то говорила об учёбе в Беркли. Я отнёс это к тем самым галлюцинациям, которые они сейчас устраняют. Однако она не только доказала, что я был неправ, но и пошла значительно дальше, став PhD по сложнейшей тематике. Кстати, перед отъездом в Беркли она позвонила и попрощалась со мной, что у подавляющего числа молодых людей не принято.
Успеха и счастья вам, дорогие ребята!
