Современные большие языковые модели (LLM), такие как GPT-4, DeepSeek или Gemini, сегодня активно внедряются в самые разные области, от помощи в написании кода до решения задач автоматизированного рассуждения. Однако при всей их впечатляющей продуктивности остаётся фундаментальный вопрос: насколько можно доверять результатам, выдаваемым такими моделями, если от решений требуется абсолютная точность и детерминированность? Несмотря на то, что LLM могут генерировать сложные формальные спецификации и даже формальные доказательства, они остаются по своей природе вероятностными...