DeepMind представила AlphaProof Code — систему доказательств корректности кода

Google DeepMind представила AlphaProof Code — систему, которая доказывает корректность программ формально, то есть машинно проверяемым рассуждением, а не тестами. Это развитие AlphaProof, которая раньше решала олимпиадные математические задачи.

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