Эксперимент по созданию quick-and-dirty пруверов для оценки завершаемости в рамках рубежного контроля (Антонина Непейвода, OSEDUCONF-2022)

Короткая ссылка: 20220520I

Докладчик: Антонина Непейвода

Изложение теоретической информатики без возможности «потрогать руками» приводит к тому, что студенты начинают скучать, особенно те, кто уже умеют программировать и не считают, что теория способна улучшить этот навык. Однако привычные студентам задачи серьёзно отличаются от тех, которые связаны с практическим применением достаточно сложной теории.
В частности, при разработке современных proof-assistant технологий или SMT-солверов учитывается изначальная неразрешимость задачи в общем виде и выбираются всевозможные аппроксимации её решения. В частности, такова задача проверки завершаемости систем переписывания термов (C некоторыми оговорками можно было бы также вести речь о завершаемости программ на функциональном языке).

Видео

on youtube

Презентация

Thesis

https://github.com/bmstu-iu9/TerminatorBattle2021

Ежегодное соревнование пруверов по оценке завершаемости проводится с 2003 года ^[1]. Мы постарались сохранить в эксперименте его главные черты:

никаких ограничений в языке реализации, при этом алгоритм (исходный код) решения должен быть открыт;
система тестов также доступна участникам в процессе соревнования;
никакого минимального набора тестов, которые прувер обязан точно проходить: подсчитывается лишь общее количество баллов за все тесты;
наличие в базе данных очень сложных тестов, которые (почти точно) не будут решены ни одним прувером («монстров»);
по желанию участники могут добавить к базе данных свои «секретные» тесты.

Было и два отличия. Во-первых, строить описание доказательства не требовалось, поскольку каждой команде пришлось бы ещё проектировать язык описания таких доказательств. Во-вторых, задача оценки завершаемости сложная и неоднозначная, а времени давалось слишком мало, чтобы успеть безупречно отладить пруверы, и дисквалификация за ошибки была бы чрезмерно жёстким решением в рамках рубежного контроля. В реальных состязаниях по завершаемости нет систем автоматической проверки генераторов доказательств, потому что нет навязанного единого способа строить такие доказательства, и бывали случаи, что правильному ответу соответствовало неправильное обоснование. Поэтому мы штрафовали неправильные ответы или формально правильные, но не обоснованные алгоритмом прувера^[2] ответы только баллами.

Участие в эксперименте проводилось на добровольной основе: студенты могли сами выбрать, хотят они писать письменную контрольную работу или разрабатывать прувер. Накануне соревнования командам были выданы по 5 пробных задач из разных классов. На следующий день был выложен скрипт тестирования TermBase, оценивающий результат работы пруверов на 100 различных системах переписывания термов, часть из которых была сгенерирована автоматически, часть — взята из студенческих работ, а часть — из базы данных соревнований по завершаемости TPDB. Код скрипта был полностью открыт, но написан на языке Рефал, и понять, как именно расшифровываются хеши тестов, было отдельной задачей (по желанию).

На «разборе полётов» выяснилось несколько выводов, которые студенты сделали при решении задачи.

На быстродействие при решении сложных задач больше влияет не язык реализации, а алгоритм. Участник, утверждающий, что проиграет по скорости, поскольку пишет на интерпретируемом языке Python, победил всех на самых коротких срезах, поскольку написал эффективный алгоритм предварительного анализа тестов.
Студенты сами отказались от идеи использовать нейросети для решения задачи (хотя это не запрещалось), поскольку минимальные изменения в синтаксисе теста могут привести к совершенно разным эффектам с точки зрения завершаемости, и нейросеть будет слишком часто ошибаться.
Правильный ответ не означает правильности программы. Если прувер формально корректно оценивал свойства «монстров», это позволяло сразу же построить тест, на котором выявлялось ошибочное поведение. Оказалось, что самый надёжный способ не получать штрафы — не пытаться ничего подгонять, а честно признаться, что решение построить не удалось.

В целом и по отзывам студентов опыт «игрушечной» научной разработки оказался положительным. Студенты убедились, что неразрешимые задачи решать можно и нужно, но без теоретической подготовки это не получится. Эксперимент также показал значительный разрыв в подготовке между студентами: несколько команд-добровольцев не смогли построить даже прототип прувера. Поэтому повторять такой опыт можно лишь будучи уверенными в том, что его участники хорошо владеют хотя бы базовыми алгоритмами синтаксического анализа и анализа графовых структур.

Примечания и ссылки

↑ C. March, H. Zantema The Termination Competition // Term Rewriting and Applications, 18th International Conference, {RTA} 2007, Paris, France, June 26—28, 2007, Proceedings, LNCS, 4533, pp.~303—313, 2007.
↑ В частности, любые определённые ответы на вопрос о завершаемости систем--«монстров».

[Zantema-1] C. March, H. Zantema The Termination Competition // Term Rewriting and Applications, 18th International Conference, {RTA} 2007, Paris, France, June 26—28, 2007, Proceedings, LNCS, 4533, pp.~303—313, 2007.

[2] В частности, любые определённые ответы на вопрос о завершаемости систем--«монстров».

[1]

[2]