VERINA: оценка больших языковых моделей на основе генерации проверяемого кода с формальными доказательствами
Проблема верификации при генерации кода на основе LLM Большие языковые модели (LLM) демонстрируют высокие результаты в программировании и широко используются в таких инструментах, как Cursor и GitHub Copilot, для повышения производительности разработчиков. Однако из-за их вероятностной природы LLM не могут предоставить формальные гарантии для генерируемого кода. Сгенерированный код часто содержит ошибки, и при использовании генерации … Читать далее