Автоматическая проверка правильности решения задач

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

В системах автоматизированного обучения проверка знаний и навыков учащихся является одним из самых важных элементов. Существует множество различных способов проверки знаний и умений, существенно варьирующихся в зависимости от предметной области. Применительно к рассматриваемой предметной области – дискретной математике – можно выделить три способа проверки знаний и умений:

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

Наиболее значимыми для выработки устойчивых навыков являются задачи "на построение". Существует несколько методов проверки правильности решения задач «на построение». Самым распространенным является проверка ответа (или открытое тестирование) – то есть сравнение ответа, найденного студентом, с заранее заданным ответом. Открытое тестирование легко автоматизируется, но имманентно обладает рядом общеизвестных недостатков.

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

Идея состоит в том, чтобы применить для решения задачи автоматической проверки правильности решения подход, показавший неплохие результаты в символическом искусственном интеллекте. А именно, формулировка задачи и ответ, включая все промежуточные результаты, записываются как формулы некоторой специально придуманной формальной теории (для заданной предметной области). В таком случае решение задачи – это вывод в придуманной формальной теории. От системы не требуется автоматически искать вывод – это обычно трудная, а для некоторых формальных теорий алгоритмически неразрешимая проблема. От системы требуется автоматически проверить, что предъявленная последовательность формул действительно является выводом (то есть, получена по правилам вывода заданной формальной теории). А это уже не очень трудная задача, примерно равная по сложности синтаксическому анализу формального текста. Основная трудность состоит в придумывании подходящей формальной теории для заданной предметной области. 

Очевидно, что предлагаемый подход не является универсальным – не для всех предметных областей и не для всех классов задач в этих предметных областях возможно придумать хорошую формальную теорию и выразительный язык предметной области. 

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