Факт-чекинг: право ответить «не могу проверить»

Режим facts — то, ради чего язык поделён на два класса программ (глава «Два класса программ») и ради чего терпят консервативный анализ завершения (глава «Тотальность»). Все примеры главы проверены на flang 0.7.29.

Задача

Есть утверждение. Оно пришло снаружи — из ответа языковой модели, из строки в отчёте, из пункта регламента:

«Клиенту положена скидка».

И есть данные: суммы заказов, порог, признак постоянного клиента. Вопрос: подтверждается ли утверждение этими данными — и можно ли на ответ опереться.

Режим не оценивает правдоподобие текста, не ищет фактов в интернете и ничего не знает о мире. Он вычисляет утверждение по правилам, которые вы записали заранее, на данных, которые вы подготовили. Поэтому его ответ — не мнение, а вычисление.

Три входа

$ flang facts факты.flang --facts факты.json \
    --claims '["«Сумма больше порога» от суммы, порог равно да"]' --pretty

Первый вход — программа: правила, записанные тотальными функциями.

модуль «Проверка суммы»

тотальная функция «Сумма списка»
  принимает элементы: список числа
  возвращает число
  пример «Три числа»
    дано элементы равно [10, 20, 30]
    ожидается 60
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то голова плюс «Сумма списка» от хвоста

тотальная функция «Сумма больше порога»
  принимает суммы: список числа, порог: число
  возвращает признак
  пример «Набрал»
    дано суммы равно [10, 20]
    дано порог равно 25
    ожидается да
  пример «Не набрал»
    дано суммы равно [1, 2]
    дано порог равно 10
    ожидается нет
  («Сумма списка» от суммы) больше порог

Ту же сумму можно взять из стандартной библиотеки (использует «Lists», глава «Стандартная библиотека») — здесь она выписана, чтобы программа читалась одним файлом.

Второй вход — факты, обычный JSON-объект:

{
  "суммы": [1200, 800, 400],
  "порог": 2000,
  "постоянный": true
}

Форма значений та же, что у --args команды run и у значений в примерах: список — массив, запись — объект, признак — true/false.

Третий вход — утверждения, JSON-массив строк. Каждая имеет вид <терм> <оператор> <терм>, и в ответе появляется по одной записи на каждую.

Ответ

{
  "ok": true,
  "results": [
    {
      "claim": "«Сумма больше порога» от суммы, порог равно да",
      "holds": true,
      "why": "«Сумма больше порога» от факта «суммы», факта «порог» = да; требование «равно да» выполнено",
      "steps": [ … ],
      "status": "verified"
    }
  ]
}

2400 больше 2000, утверждение подтверждается, код возврата 0. Спросим обратное — то же самое с ожиданием нет:

{
  "ok": false,
  "results": [
    {
      "claim": "«Сумма больше порога» от суммы, порог равно нет",
      "holds": false,
      "why": "«Сумма больше порога» от факта «суммы», факта «порог» = да, а утверждение требует «равно нет». Исходные факты — «суммы»: [1200,800,400]; «порог»: 2000",
      "steps": [ … ],
      "status": "refuted"
    }
  ]
}

Код возврата 1. Поле why называет вычисленное значение, требование и исходные факты отдельно. Ответ «не выполнено» без вычисленного значения оставляет спорящего ни с чем; ответ с числом переводит спор из «инструмент неправ» в «данные не те» или «правило не то».

Третий ответ — на утверждение о функции без пометки тотальная:

{
  "claim": "«Обратный счёт» от н равно 0",
  "holds": false,
  "why": "функция «Обратный счёт» не помечена как «тотальная»; факт-чекинг допускает только тотальные функции — иначе ответ может не наступить",
  "status": "refused"
}

Здесь тоже holds: false, но означает это совсем другое.

Три исхода, а не два

«Утверждение ложно» и «я не могу это проверить» — разные ответы, и система, которая их смешивает, вводит в заблуждение ровно тогда, когда её ответ нужнее всего. Различайте их по полю status: код возврата у опровержения и у отказа одинаковый — 1. Код 2 означает, что сломался сам вызов: не назван файл, не разобран JSON, не связалась программа.

Причины отказа, проверенные запуском на 0.7.29 (текст why дословно):

• функция не тотальная — функция «Обратный счёт» не помечена как «тотальная»; …;
• функции нет в программе — функция «Нет такой» не найдена в программе;
• в фактах нет нужного поля — не передан факт «нет_поля» для аргумента «элементы»;
• типы не сходятся — вычисление «Сумма списка» остановлено: операция «add» допустима только для чисел, получено строка и число [FLANG_TYPE];
• строка утверждения не разобрана — не удалось разобрать утверждение: ожидалось «<что-то> <оператор> <что-то>», …;
• вычисление не уложилось в предел шагов — … исчерпала лимит шагов (5) на глубине вызовов 1. Ответ не может быть дан за отведённый бюджет.

Последний случай — тоже ответ, а не сбой: «не досчитали за отведённый бюджет». Предел задаётся ключом --steps N, по умолчанию 10 000.

Грамматика утверждений и почему она такая узкая

Термы:

Операторов шесть: равно, не равно, больше, меньше, не больше, не меньше. Английская запись тоже читается: fact «порог» is greater than 1000, факт «порог» equals 2000.

И всё. Ни скобок, ни арифметики (факт «порог» равно 2000 плюс 1 — отказ), ни двух сравнений подряд, ни «и» между ними (… больше 1000 и факт «порог» меньше 3000 — отказ).

Почему бы не разрешить в утверждении выражение языка? Потому что утверждение приходит снаружи — от человека, от модели, из документа. Разрешить в нём произвольное выражение значит согласиться исполнять чужой код:

• тотальность пришлось бы доказывать на лету для каждого утверждения, вместо одной проверки уже собранной программы;
• утверждение перестало бы быть данными. Сейчас его можно записать в журнал, показать пользователю, сравнить с прошлым, положить в тест;
• размылась бы ответственность. Сейчас правила — ваши, утверждение — чужое. С произвольным выражением автор утверждения становится соавтором правил.

Узость грамматики — та же цена, которую платит весь язык: выразительность обменивается на проверяемость.

Что делать, когда утверждение не выражается

Вся логика живёт в программе, в утверждении остаётся только применение.

Нужно проверить: «скидка положена, потому что клиент постоянный и набрал больше порога». Связка «и» в утверждении запрещена, но в языке она есть (и притом), поэтому условие уезжает в функцию:

модуль «Скидка»

тотальная функция «Сумма списка»
  принимает элементы: список числа
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то голова плюс «Сумма списка» от хвоста

тотальная функция «Скидка по сумме»
  принимает постоянный: признак, сумма: число, порог: число
  возвращает признак
  постоянный и притом (сумма больше порог)

тотальная функция «Скидка положена»
  принимает суммы: список числа, порог: число, постоянный: признак
  возвращает признак
  пример «Постоянный и набрал»
    дано суммы равно [1200, 800, 400]
    дано порог равно 2000
    дано постоянный равно да
    ожидается да
  пример «Набрал, но не постоянный»
    дано суммы равно [1200, 800, 400]
    дано порог равно 2000
    дано постоянный равно нет
    ожидается нет
  «Скидка по сумме» от постоянный и («Сумма списка» от суммы) и порог

утверждение «без постоянства скидки нет»
  для всех сумма: число
  для всех порог: число
  утверждаем («Скидка по сумме» от нет и сумма и порог) равен нет

Утверждение снова однооператорное:

«Скидка положена» от суммы, порог, постоянный равно да

Правило при этом:

• тотально — значит, допущено к факт-чекингу;
• снабжено примерами, которые гоняет flang test (примеров 2, прошло 2, не прошло 0);
• переводится командой flang emit в C, Go, Rust, Python, JavaScript и другие языки (глава «Кодогенерация»), если ту же скидку нужно считать внутри продукта;
• лежит в одном месте. Правило, размазанное по строкам утверждений, не имеет ни автора, ни тестов, ни истории изменений.

Последний блок программы — утверждение … для всех — это соседний инструмент. facts проверяет утверждение на ваших данных. Утверждение в программе говорит о всех входах сразу, и его доказывает компилятор при сборке:

$ flang check скидка.flang --proof
…
  утверждение «без постоянства скидки нет» — доказано сведением цели с телом функции: … — утверждение обо ВСЕХ входах, а не о написанных; …
скидка.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1, … — код возврата 0

Не каждое такое утверждение доказывается: если компилятор не справился, отчёт говорит «объявлено, не доказано» и check --proof выходит кодом 3. Подробнее — в главе «Чего в языке пока нет».

Почему нельзя обойтись пределом шагов

Возражение: у вычисления и так есть предел шагов. Зациклившаяся функция упрётся в него и получит отказ. Зачем тогда отказывать нетотальным заранее?

Затем, что предел защищает от вечности, но не даёт предсказуемости. Функция, укладывающаяся в предел на сегодняшних данных, не обязана уложиться на завтрашних: на одних входах утверждение будет проверяться, а на других, внешне похожих, — нет. И такой отказ говорит не о правиле, а о размере входа.

Отказ по классу приходит до вычисления, зависит только от текста программы и потому одинаков всегда — как ошибка компиляции против ошибки во время работы.

Обратное тоже верно: компилятор flang, написанный на самом flang, тотальным быть не обязан и имеет право упереться в предел шагов — он обещает «разобрать или отказать», а не «ответить». Пометка тотальная — не знак качества, а обязательство перед вызывающим, и факт-чекинг — то место, где это обязательство действительно взято.

След в ответе

В каждом ответе есть массив steps: разбор утверждения, проверка тотальности, прочитанные факты, вычисление с аргументами и итоговое сравнение. Это не отладочный вывод. У следа три потребителя:

• человек, который не согласен с ответом, — ему нужно не «нет», а «вот из каких фактов и по какому правилу получилось нет»;
• журнал — через год вопрос «почему тогда отказали» задают всерьёз, и честный ответ — сохранённый след вместе с версией правил;
• тесты — раз why и steps попадают в журналы и на экраны, это наблюдаемое поведение, и изменение текста — изменение поведения.

Встраивание

Вывод — JSON в stdout, код возврата 1 при ok: false. Отсюда две схемы.

В сборке. Утверждения лежат файлом рядом с правилами, шаг проверки падает, если хоть одно перестало подтверждаться. Набор утверждений становится регрессионным тестом на бизнес-правила: поменяли порог — сразу видно, какие обещания перестали быть правдой.

В конвейере с агентом. Модель формулирует утверждение, инструмент отвечает. Модель хорошо формулирует и плохо считает; язык хорошо считает и ничего не формулирует. Отказ здесь — сигнал: спросили о том, чего в правилах нет. Дописать правило дешевле, чем принять правдоподобный ответ модели за проверенный. Зачем вообще проверять ответ агента отдельным механизмом — глава «Проверка результата» трека про ИИ-агентов.

Факты вы готовите сами. flang facts принимает --facts факты.json и не ходит за данными никуда — ни в файлы, ни в сеть, ни к часам. Это ограничение режима, а не языка: программа на flang может читать файлы и ходить в сеть через flang io (глава «Синтаксис по факту»). Соединить одно с другим можно, но это будет уже ваша программа, а не встроенный режим.

Чем это отличается от остальных способов

Языковая модель отвечает всегда — и именно поэтому её ответ нельзя отличить от знания. flang facts отвечает не всегда, зато различает «нет» и «не могу».

Цена

• Правила надо написать заранее. Если они меняются чаще, чем приходят утверждения, режим не окупится.
• Факты надо подготовить. Встроенного способа их достать у режима нет.
• Грамматика узкая: составное утверждение требует функции под каждое сочетание условий.

Отсюда область применимости: правила стабильнее утверждений. Тарифы, допуски, регламенты, условия скидок, критерии соответствия — правило живёт годами, а утверждений о нём проходят тысячи. Для проверки произвольных высказываний о мире режим не годится и не притворяется.

Что здесь стоит унести

1. Система, обязанная отвечать, обязана уметь отказаться. Ответ, который есть всегда, — ответ, которому нельзя доверять.
2. Отказ несёт причину и не равен отрицанию. «Нет» и «не знаю» — разные ответы.
3. Проверяемость покупается сужением. Узкий вход — условие, при котором о нём вообще можно что-то доказать.
4. Логику держите в проверяемом коде, а не в строке запроса.

Что дальше

Это последняя глава о самом языке. Куда идти дальше:

• К предшественнику — FTS: язык исполняемых спецификаций, из которого flang вырос, и требования, проверяемые до реализации.
• К устройству языков вообще — Компиляторы и языки: лексер, парсер, типы и кодогенерация в учебном изложении.
• К проверке того, что делает агент — ИИ-агенты, особенно проверка результата и режимы отказов.
• К рассуждению как таковому — Логика и аргументация: чем подтверждение отличается от неопровержения.
• К проверкам в конвейере — Тестирование: тест, который не может упасть, ничего не проверяет.

Общая карта треков портала — в дорожной карте.

Всё написанное здесь проверено запуском на flang 0.7.29. Если что-то разошлось с вашей версией — проверяйте так же: flang facts файл.flang --claims '[…]' отвечает за доли секунды.