Агенты Google нашли квантовые программы и доказали их свойства в Lean
Агенты синтезируют квантовые программы по формальной спецификации и доказывают в Lean их корректность и стоимость.
Формальная проверка работает для программ на тысячах кубитов, которые нельзя полноценно симулировать классически.
Для задач термоядерного синтеза, фотохимии и метаболизма лекарств стоимость схем снизилась в 11, 8 и 2,5 раза.
В квантовой арифметике агенты улучшили прежнюю базовую линию в 290 раз.
Почему важно
Формальные доказательства позволяют агентам искать алгоритмы за пределами доступной симуляции без подмены надежности тестами на малых примерах.