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