"Ещё одна важная новость из мира эйай: Стартап Harmonic запустил приложение с чатботом, став первым общедоступным математическим эйай-сервисом с формальной проверкой результата. А скоро обещают и API для компаний выкатить. Обычный* генеративный ИИ работает примерно как ребёнок, которого родители научили, что ветер дует, потому что деревья качаются, и он говорит: ""ветер дует"". А почему он дует? И дует ли? Другими словами, если попросить ChatGPT или Claude расписать математическую формулу, то он её... как бы сказать... попробует угадать в формате ""я зделяль"". Но ответить и пояснить за свой генеративный базар не сможет. Можно ли такой формуле доверять и закладывать её в серьёзные расчёты - судите сами. А ИИшка от Harmonic под названием ""Aristotle"" работает не так. Генеративный ИИ (LLM) предлагает гипотезу или часть решения и передаёт её в специальный доказательный движок, который всё проверяет с точки зрения формальной логики, аксиом, мат. определений. Алгоритмически, то бишь. Весь процесс происходит на Lean - это такой интерактивный инструмент доказательства теорем. По сути, специальный язык программирования и формальной логики, где каждое утверждение должно быть доказано шаг за шагом, а пруф должен быть проверяем машиной. Если движок ""Аристотеля"" не может верифицировать решение от LLM, то генерится другое решение. Потом его снова проверяют. И так по новой, пока проверка не будет пройдена. И лишь тогда решение выплюнется юзеру. За счёт этого Harmonic не галлюционирует, и (по идее) его можно использовать для взрослых математических и логических задач. От академической математики до инженерии, фин. анализа и даже юридических рассуждений. * Генеративный ИИ теперь обычный, дожили, хех 😈 Дизраптор"