Модели сделали математическую проверку кода применимой к большим проектам — Anthropic

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

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

В обсуждении на Hacker News спорят о границе: спецификацию по-прежнему пишет человек, и неверно сформулированное требование доказывается так же успешно, как верное.