Большие языковые модели делают формальную верификацию ПО возможной в гораздо большем масштабе
Anthropic использовала Claude, чтобы за несколько недель доказать свойства безопасности более чем в сотне реальных open-source библиотек, получив машинно-проверенные доказательства отсутствия сбоев вплоть до уровня ассемблера и обнаружив баги, скрывавшиеся годами. Раньше формальная верификация была возможна лишь для небольших кодовых баз. Это важно, потому что показывает: ИИ способен принести математические гарантии корректности в open-source цепочку поставок в масштабе, недостижимом для людей.
ИСТОЧНИКИ
- Anthropic Research2026-10-22 00:00
- Anthropic2026-10-22 22:01