Anthropic использовала свою модель Claude, чтобы создавать математические доказательства безопасности уже существующего кода. По данным The Decoder, в итоге получилось около 180 миллионов строк кода доказательств для 123 библиотек с открытым исходным кодом. При этом модель наткнулась на ошибки, которые не выявило многолетнее тестирование.
Что означает формальная верификация
Классические тесты проверяют, выдаёт ли программа ожидаемый результат в отдельных выбранных ситуациях. Однако они охватывают лишь те случаи, о которых кто-то подумал. Формальная верификация, напротив, математически доказывает, что программа обладает определённым свойством, причём для всех возможных входных данных, а не только для выборочных. Само доказательство тоже является кодом, который проверяющая программа контролирует шаг за шагом.
Загвоздка в том, что писать такие доказательства трудоёмко и для этого нужны специальные знания. Поэтому метод пока в основном применяют там, где ошибки были бы особенно дорогими. Именно здесь и работает этот подход. Если доказательства создаёт ИИ, затраты могут заметно снизиться.
Почему это интересно разработчикам
По данным источника, Anthropic хочет в ближайшее время сделать формальную верификацию с помощью ИИ такой же практичной, как сегодняшние стандартные тесты. Это стало бы ещё одним шагом в автоматизации разработки программного обеспечения: ИИ не только пишет код, но и подтверждает его корректность.
Из краткого сообщения неясно, сколько человеческого контроля для этого нужно и для каких видов ошибок действуют доказательства. Доказательство убедительно лишь настолько, насколько убедительно свойство, которое оно подтверждает. Тем, кто использует библиотеки с открытым исходным кодом, можно следить за развитием событий. Но полагаться на это стоит только тогда, когда появятся более подробные сведения.
