Как формальные методы могут помочь прунить спейс если объяснить на пальцах?
Например мы хотим генерить код, в данном случае мы можем на каждом этапе генерации токена проверять удовлетворяет ли корректному синтаксису полученная строка.

Другой пример если мы ставим какой то constraint на аутпут LLM. Например a && b, понятно если a=false, нет смысла дальше проверять эту ветку дерева.

Математически мы используем производные от строк, так называемые Brzozowski derivatives, пример теоремы определенной формальной абстракции которые позволяют сохранить Soundness при прунинге спейса с сonstraints, на практике мы хотим получить гарантии soundness, а не completeness