Ещё одна важная новость из мира эйай:

Стартап Harmonic запустил приложение с чатботом, став первым общедоступным математическим эйай-сервисом с формальной проверкой результата. А скоро обещают и API для компаний выкатить.

Обычный* генеративный ИИ работает примерно как ребёнок, которого родители научили, что ветер дует, потому что деревья качаются, и он говорит: "ветер дует". А почему он дует? И дует ли?

Другими словами, если попросить ChatGPT или Claude расписать математическую формулу, то он её... как бы сказать... попробует угадать в формате "я зделяль". Но ответить и пояснить за свой генеративный базар не сможет. Можно ли такой формуле доверять и закладывать её в серьёзные расчёты - судите сами.

А ИИшка от Harmonic под названием "Aristotle" работает не так. Генеративный ИИ (LLM) предлагает гипотезу или часть решения и передаёт её в специальный доказательный движок, который всё проверяет с точки зрения формальной логики, аксиом, мат. определений. Алгоритмически, то бишь.

Весь процесс происходит на Lean - это такой интерактивный инструмент доказательства теорем. По сути, специальный язык программирования и формальной логики, где каждое утверждение должно быть доказано шаг за шагом, а пруф должен быть проверяем машиной.

Если движок "Аристотеля" не может верифицировать решение от LLM, то генерится другое решение. Потом его снова проверяют. И так по новой, пока проверка не будет пройдена. И лишь тогда решение выплюнется юзеру.

За счёт этого Harmonic не галлюционирует, и (по идее) его можно использовать для взрослых математических и логических задач. От академической математики до инженерии, фин. анализа и даже юридических рассуждений.

* Генеративный ИИ теперь обычный, дожили, хех 😈

Дизраптор