Путь к совершенному ПО: Искусственный интеллект в автоматической формальной верификации

При написании высококачественного программного обеспечения не обойтись без этапа формальной верификации . Несмотря на то, что наша жизнь уже была в некоторой степени упрощена, благодаря таким помощникам доказательства как Coq и Isabelle/HOL, обучающим модель предсказывать один шаг доказательства за раз, оптимизация формальной верификации еще не была достигнута. Новый метод автоматической генерации доказательств – модель Baldur . Данный метод основывается на использовании больших языковых моделей, возможности восстановления доказательства и исправления благодаря указанию ошибки и добавлению контекста. Baldur превосходит все существующие подходы, он может самостоятельно полностью за раз доказывать 47.9% теорем, и даже этот результат – не предел. В данной статье я познакомлю Вас со всей теоретической и практической подноготной данной модели, этапами реализации и оценки метода, чтобы стать чуточку ближе к созданию идеального ПО! Приятного прочтения :)

https://habr.com/ru/companies/bothub/articles/792196/

#ии #ии_и_машинное_обучение #программное_обеспечение #формальная_верификация #проверка_кода #доказательство_теорем #isabelle #thor #компиляторы #baldur