ИИ без галлюцинаций: как Lean 4 заставляет модели доказывать правду

Современные большие языковые модели демонстрируют впечатляющие способности, но остаются ненадёжными и могут галлюцинировать, выдавая ошибочные факты за правду. В ответ на это появляется Lean 4 - открытый язык программирования и помощник для формальных доказательств (theorem prover), который приносит математическую строгость в мир ИИ. Именно строгость и проверка по логике делают Lean 4 ключевым инструментом для создания надёжных и безопасных систем. 

Lean 4 сочетает в себе два аспекта: это язык программирования и механизм формальной верификации. Любое утверждение или программа в Lean 4 должно пройти строгую проверку через надёжное ядро (trusted kernel), и результат либо доказан корректным, либо отвергается. Такой подход исключает неясность - результат либо верен, либо нет. 

В отличие от нейросетей, которые ведут себя вероятностно и могут давать разные ответы на один и тот же запрос, Lean 4 работает детерминированно. То есть при тех же входных данных проверка доказательства всегда даёт один и тот же вывод, и любой шаг рассуждений можно проаудировать. Это обеспечивает прозрачность и предсказуемость - свойства, без которых сложно доверять ИИ в важных сценариях.

Ярким примером применения является стартап Harmonic AI. Их система, называемая Aristotle, решает математические задачи, генерируя доказательства в Lean 4. Только после того, как доказательство проходит проверку Lean, система выдаёт ответ пользователю. По словам основателей, это делает ответы без галлюцинаций. Более того, в решении задач Международной математической олимпиады (IMO) он выступал как «золото», но при этом с формальными доказательствами.

Lean 4 полезен не только для математики. Он может применяться при написании программного кода с гарантией безопасности.