Два профессора из Принстона, работающие в области компьютерных наук и операций, получили грант для исследования, которое может изменить подход к обеспечению безопасности в сложных технологиях. Профессор операций и финансового инжиниринга Амир Али Ахмади и профессор компьютерных наук Правеш Котари получили грант от Princeton AI Lab для проекта под названием «AI-Assisted Algebraic Proof Systems with Engineering Applications».
Цель их работы — использовать данные, специфичные для приложений, в сочетании с инструментами ИИ для масштабирования алгебраических систем доказательств, основанных на полуправильном программировании. Этот метод позволяет решать сложные задачи оптимизации, особенно в условиях неопределенности и безопасности, что критически важно в инженерных приложениях, где ошибки недопустимы.
Исследование будет сосредоточено на таких ключевых аспектах, как проверка безопасности роботизированных систем, автоматическое доказательство теорем в геометрии и алгоритмическая статистика, устойчивая к выбросам. Например, проверка безопасности включает в себя доказательство того, что система, такая как дрон или автономный автомобиль, всегда будет действовать безопасно в любых условиях.
Ахмади отметил, что их сотрудничество стало возможным благодаря общему интересу к оптимизации суммы квадратов, где он и Котари работают с разных сторон — теоретической и практической. Оптимизация суммы квадратов — это современная математическая техника, позволяющая исследователям проверять, как системы, описываемые полиномиальными уравнениями, ведут себя в различных условиях.
Несмотря на то, что грант не является крупным, он уже помог продвинуть проект. Дополнительная поддержка от Фонда инноваций Школы инженерии и прикладных наук позволит команде привлечь больше студентов и заложить основу для дальнейших исследований.
Первый проект команды включает интерпретацию алгоритмов суммы квадратов для нахождения числа раскраски графа. Это может быть полезно в различных приложениях, например, для определения минимального количества классов, необходимых для проведения всех курсов без конфликтов.
В долгосрочной перспективе Ахмади и Котари надеются, что их работа внесет вклад в одну из самых амбициозных задач в области искусственного интеллекта — автоматическое математическое доказательство. Это открывает новые горизонты для применения ИИ в решении сложных математических задач, что может значительно повлиять на развитие технологий в будущем.