Кафедра математической логики и теории алгоритмов

Механико-математического факультета МГУ


Искусственный интеллект. Автоматизация доказательства

К числу наиболее бурно развивающихся сегодня областей применения компьютеров относится так называемое машинное обучение. С самого начала создания и применения компьютеров в 1950-ых гг. предпринимались попытки использовать компьютеры не просто для быстрых вычислений по заданному заранее относительно несложному алгоритму, но и для автоматизации не до конца описанных, или при формализации приводящих к переборным задачам, видов интеллектуальной деятельности человека. В последние десятилетия в данной области — искусственно интеллекте, были достигнуты огромные успехи. Исследованиями в данном направлении на кафедре занимается наш выпускник, сотрудник МИАН и руководитель Департамента больших данных и информационного поиска ВШЭ Владимир Владимирович Подольский.

Появление компьютера, как инструмента автоматизации интеллектуальной деятельности человека, закономерно привело и к созданию компьютерных инструментов автоматизации построения и проверки математических доказательств. Все студенты кафедры знакомятся с одним из наиболее известных таким инструментов — системой Coq — в практическом курсе, разработанном В.Н. Крупским и С.Л. Кузнецовым для студентов 3-го курса кафедры. Участвовать в занятиях Coq-практикума могут и другие студенты мехмата, а также других факультетов и университетов.