Хоар и ИИ

Хоар указал на фундаментальную проблему.

Деньги и учёные не отменяют теорему Райса (1953):

«Никакое нетривиальное свойство программы нельзя вычислить алгоритмически».

Что это значит для ИИ

Свойство «Цена обновилась правильно» — можно доказать тройкой Хоара. Здесь у нас есть чёткое формальное определение: цена в Bitrix24 должна равняться цене в Google Sheets.

Свойство «Нейросеть распознала кошку» — нельзя доказать тройкой Хоара. Потому что непонятно, что значит «правильно». Это статистическое понятие, а не формально-логическое.

Свойство «LLM не сгенерирует оскорбление» — нельзя доказать тройкой Хоара. Нельзя перебрать все возможные входы и выходы, а само понятие «оскорбление» размыто и зависит от контекста.

Свойство «Модель справедлива к расе/полу» — нельзя доказать тройкой Хоара. Это неформализуемое понятие, которое невозможно выразить в терминах пред- и постусловий.

Ирония

Хоар сам создал язык CSP (Communicating Sequential Processes), который повлиял на Go и Erlang. Он не против сложных систем. Он против иллюзии, что любую программу можно формально верифицировать.

«Недоказуемость — не повод не пытаться. Это повод не обещать невозможное». — примерно так.

Проверка нейросетью нейросети — это статистика, а не верификация.

Почему проверка нейросетью нейросети не решает проблему

Что вы получаете:

Вероятность ошибки, например 0.1 процента. Оценку на тестовой выборке. Согласие двух чёрных ящиков.

Чего вы не получаете:

Гарантию отсутствия ошибок. Доказательство для всех возможных входов. Формальную спецификацию.

Пример

Две нейросети проверяют, не сгенерировала ли первая оскорбление.

• Первая: «Ты дурак» — не оскорбление (99% уверена)
• Вторая: «Ты дурак» — не оскорбление (97% уверена)

Обе ошиблись. А вы уверены, что правильно.

Что нужно для тройки Хоара

{нейросеть_не_сгенерирует_оскорбление} LLM {постусловие}

Чтобы это работало, нужно:

1. Формально определить «оскорбление» (невозможно)
2. Доказать, что для всех возможных промптов ответ безопасен (невозможно)

Итог

Нейросети не дают гарантий. Хоар — про гарантии. Это разные вселенные.

Хоар, скорее всего, оценил бы:

1. Честность — признание границ применимости
2. Точность — различение статистической корректности и формальной верификации
3. Отсутствие иллюзий — «недоказуемость — не повод не пытаться»

А ещё он бы сказал: «Теперь напишите мне формальную спецификацию для "оскорбления"». И мы бы ответили: «мы работаем над этим».