Basis заставила LLM доказать, что семантика языка совпадает с реальным интерпретатором
Ship Your Interpreter
Исследователи из Basis поручили LLM написать формальную семантику небольшого языка WHILE и доказать в Lean, что она совпадает с настоящим интерпретатором на C, скомпилированным в RISC-V. Тесты не спасают: ранняя версия проходила весь набор, но расходилась с бинарником на именах функций длиной 59 символов. Доказательство вскрыло такие детали реализации, которые вручную никто не записывает.
Тестирование помогает, но, как мы показываем ниже, семантика может пройти все тесты и всё равно быть неверной.