автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.06, диссертация на тему:Модели и алгоритмы верификации решений задач в системах электронного обучения

На правах рукописи

005534150

Перченок Олег Владимирович

МОДЕЛИ И АЛГОРИТМЫ ВЕРИФИКАЦИИ РЕШЕНИЙ ЗАДАЧ В СИСТЕМАХ ЭЛЕКТРОННОГО ОБУЧЕНИЯ

Специальность: 05.13.06 — «Автоматизация и управление технологическими процессами и производствами (образование)»

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата технических наук

З ОКТ 2013

Санкт-Петербург - 2013

005534150

Работа выполнена в Санкт-Петербургском государственном электротехническом университете «ЛЭТИ» им. В.И. Ульянова (Ленина) на кафедре высшей математики

№2

Научный руководитель: Поздняков Сергей Николаевич,

доктор педагогических наук, профессор

Официальные оппоненты: Новиков Федор Александрович,

доктор технических наук, старший научный сотрудник, Санкт-Петербургский государственный политехнический университет, Институт прикладной математики и механики, профессор

Бабаев Сергей Александрович, кандидат технических наук, доцент, Балтийский государственный технический университет «Военмех» им. Д.Ф. Устинова, кафедра «Инжиниринг и менеджмент качества», профессор

Ведущая организация: Санкт-Петербургский государственный

университет аэрокосмического приборостроения

Защита диссертации состоится 24 октября 2013 г. в 15.30 на заседании диссертационного совета Д212.227.06 в Санкт-Петербургском национальном исследовательском университете информационных технологий, механики и оптики (НИУ ИТМО) по адресу: 197101, г. Санкт-Петербург, Кронверкский пр., д. 49, конференц-зал ЦИО.

С диссертацией можно ознакомиться в библиотеке НИУ ИТМО.

Автореферат разослан 20 сентября 2013г.

Ученый секретарь диссертационного совета к. ф.-м. н.

Л?

Лобанов И.С.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

• использование узкого класса задач (ответ с множественным выбором, ввод

числа);

• статичность, которая является потенциальным источником копирования;

• возможные авторские ошибки в формулировках задач;

• возможные ошибки в подготовке эталонных ответов.

Данные недостатки возникают из-за отсутствия средств автоматизации для адекватного описания задачи. Задача описывается неформализованным текстом, при помощи которого невозможно автоматически проверить ее решение. Если при этом составитель задачи допустит ошибку, то правильное решение задачи будет оценено как неверное. Другой проблемой систем электронного обучения является единственность правильного ответа. Данный факт позволяет учащимся легко скопировать ответ в случае его случайного попадания в свободный доступ.

Для решения перечисленных проблем разрабатывается программные средства по составлению и решению задач для систем ЭО, в которых описание задач строится на формальной модели предмета. Решение задачи осуществляется студентом (или учеником) в предметной среде на основе инструментов, являющихся существенными для данного класса задач. Оно автоматически верифицируется системой на формальном описании задачи и не требует предварительного решения задачи автором или проверяющим. Для составления формального описания задач необходимо вводить модели их структуры, а для автоматической верификации задач необходима разработка алгоритмов верификации. Поэтому создание новых моделей и алгоритмов верификации решений задач актуально.

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

В соответствии с указанной целью в работе сформулированы и решены следующие задачи:

1) анализ проблем верификации решений задач в современных системах ЭО;

2) разработка математической модели самопроверяемой задачи;

3) создание модели представления знаний об абстрактных самопроверяемых задачах;

4) разработка модели абстрактного предметно-ориентированного языка для описания условий задач;

5) введение модели жизненного цикла программного средства по решению и составлению самопроверяемых задач;

6) создание алгоритмов верификации самопроверяемых задач;

7) разработка предметно-ориентированных языков для записи условий задач по геометрии и цифровой обработке сигналов;

8) разработка программных средств для решения и составления задач по геометрии и по цифровой обработке сигналов на основе разработанных моделей и алгоритмов;

9) разработка учебных систем удаленного управления устройствами с целью дальнейшего введения самопроверяемых задач в данной области;

10) экспериментальное исследование результатов диссертации практике.

Объектом исследования являются программные модули систем ЭО, обеспечивающие верификацию решений задач.

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

Методы исследования. При решении поставленных задач использовалась теория формальных языков, теория искусственного интеллекта, теория алгоритмов.

Положения, выносимые на защиту:

1) разработана математическая модель самопроверяемой задачи;

2) создана модель представления знаний об абстрактных самопроверяемых задачах;

3) разработана модель абстрактного предметно-ориентированного языка для описания условий задач;

4) разработана модель жизненного цикла программного средства для решения и составления самопроверяемых задач;

5) созданы алгоритмы верификации самопроверяемых задач;

6) разработан предметно-ориентированный язык описания задач на построение по геометрии;

7) разработан предметно-ориентированный язык описания задач в области цифровой обработки сигналов;

8) разработано программное средство по решению и составлению задач на построение по геометрии;

9) создано программное средство по решению и составлению задач для цифровой обработки сигналов;

10) разработаны программные средства - учебные системы удаленного управления робототехническими устройствами для изучения центробежной силы и равномерного движения по окружности;

11) проведен эксперимент по исследованию разработанных программных средств в двух учебных заведениях.

Научная новизна. Следующие результаты диссертации обладают научной новизной:

1) новая математическая модель самопроверяемых задач, которая приспосабливает структуру условия задачи для автоматической верификации и устанавливает взаимосвязи между математическими объектами «самопроверяемая задача», «абстрактный класс самопроверяемых задач», «предметно-ориентированный класс самопроверяемых задач», «верификатор задачи»;

2) модель абстрактного предметно-ориентированного языка описания условий задач, описывающая абстрактный синтаксис нового класса предметно-ориентированных языков, определяющая составные части описания задачи, приспособленной для автоматической верификации: неформальные условия, верификационные условия, инструментальные ограничения и параметры генерации;

3) алгоритмы автоматической верификации решений, впервые разработанные для поддержки самопроверяемых задач классов PlotProblem, CodeProblem и ExpressionProblem, позволяющие установить правильность решения студента или учащегося путем применения к нему верификационных условий, заданных преподавателем или учителем при составлении задачи.

Достоверность научных результатов и выводов. Подтверждается корректным обоснованием постановок задач, точной формулировкой критериев, проведённым анализом базовых работ в исследуемой области, а также актами внедрения.

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

Внедрение результатов. Результаты диссертационного исследования были использованы при проведении в Санкт-Петербургском государственном электротехническом университете «ЛЭТИ» им. В.И. Ульянова-Ленина научно-исследовательской работы «Программа стратегического развития СПбГЭТУ ЛЭТИ» (2012-2013, тема № ВМ-2-24): разработано и внедрено два программных продукта (имеются свидетельство о регистрации программы «Система ЭО, обеспечивающая автоматическую проверку решения математических задач по описанию их условий» № 2012611757 от 16.02.2012 г. и свидетельство о регистрации «Программы составления автоматически верифицируемых задач в области цифровой обработки сигналов» № 2013610852 от 9.01.2013 г.). Программное средство по геометрии внедрено в образовательный процесс в средней школе № 521 Санкт-Петербурга с углубленным изучением математики и информатики, а также на курсах повышения квалификации учителей в обществе с ограниченной ответственностью «ИНТОКС» (г. Санкт-Петербург). Работа поддержана грантом правительства Санкт-Петербурга для студентов и аспирантов в 2012 г. (Диплом серии ПСП № 12286).

Апробация результатов работы. Основные положения и результаты работы докладывались и обсуждались на VII международной научно-методической конференции "Дистанционное обучение - образовательная среда XXI века" (Минск, декабрь 2011 г.); на XVIII Международной научно-методической конференции "Современное образование: содержание, технологии, качество» (СПб, апрель 2012 г); на XII Южно-Российской межрегиональной научно-практической

конференции-выставки «Информационных технологии в образовании - 2012» (Ростов-на-Дону, ноябрь 2012 г); на IV Всероссийской научно-практической конференции «Информационные технологии в образовании» (Саратов, ноябрь 2012 г.); на XVII Санкт-Петербургской Ассамблее молодых ученых и специалистов (СПб, декабрь 2012 г.); на 12-ом международном конгрессе по математическому образованию ICME-12 (Сеул, Корея, июль 2012 г.); на XIX Международной научно-методической конференции "Современное образование: содержание, технологии, качество» (СПб, апрель 2013 г).

Публикации. По теме диссертации опубликованы 10 научных работ, включая 3 статьи в изданиях, рекомендованных ВАК РФ [1-3], 6 работ в материалах международных, национальных и региональных конференций [4,5,7-10] и 1 коллективную монографию [6]. Получено 2 свидетельства об официальной регистрации программы для ЭВМ [11,12].

Личный вклад автора. Содержание диссертации и положения, выносимые на защиту, отражают персональный вклад автора в опубликованные работы. Подготовка к публикации некоторых полученных результатов проводилась совместно с соавторами, причём в шести публикациях из десяти вклад автора был определяющим [1-3, 5, 7-9]. Все представленные в диссертации результаты получены лично автором.

Структура и объем диссертации. Диссертация состоит из введения, 5 глав, заключения, библиографии (65 пунктов) и приложений. Общий объем диссертации 130 страниц, из них 125 страниц основного текста, включая 50 рисунков.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновывается актуальность диссертационной работы, определяются цель и задачи исследования, формулируются научная новизна, практическая ценность, апробация и достоверность результатов.

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

Одна из основных проблем модулей контроля знаний в системах ЭО состоит в том, что преподавателю приходится «вручную» составлять много вариантов задач и решать их, при незаконном проникновении в базу данных легко узнать правильное решение. Кроме этого, если преподаватель ошибется в решении задачи, то обучаемый, даже правильно решив задачу, получит сообщение об ошибке. Такие проблемы возникают в системах ЭО, в которых условия задач и правильные (эталонные) решения хранятся в базе данных. При этом алгоритм верификации состоит в сравнении решения обучаемого с эталонным решением. Если они совпадают, то задача решена верно, в противном случае обучаемый допустил ошибку. В качестве примера приведен тренажер работы с СУБД MySQL (составление запросов), рассмотренный в статье Г.Н. Семенова, С.А. Саргсяна, С.А. Науменко «SQL-тренажер по дисциплине «Управление данными»».

Другая проблема верификации задач состоит в статичности тестовых наборов. Для ее иллюстрации в диссертации приведено описание подхода к верифика-

ции задач по информатике А.В. Лямина и О.Е. Вашенкова из статьи «Методика формирования эталонных наборов входных и выходных данных для анализа результатов выполнения заданий с неразрешимым множеством правильных ответов». Данная проблема характерна также для метода А.С. Станкевича.

Ранее существовали формализованные модели задачи, однако для них имелась проблема избыточности в случае их применения для верификации решений. Формализация задачи была описана в работах Башмаковых. Созданная авторами модель представляет собой кортеж из десяти компонентов:

М,= (A, D, С, Ms, Мт, V, К, Mas, Ov, Оа), где А - цель (что требуется от обучаемого, какую деятельность необходимо выполнить); D — исходные данные; С - ограничения, которые должны быть учтены при решении задачи ; Ms - модель ситуации (в зависимости от назначения и вида компьютерного средства обучения этот компонент может соответствовать моделям изучаемого объекта, среды профессиональной деятельности и т.д.); Msu - информационная модель, описывающая способ преставления М„ а также средства оперирования ею в рамках компьютерного средства обучения; V — результаты (ответы); Vu - описание способа ввода результата; Mas - эталонная модель деятельности; О,, -функция оценивания результата; Оа - функция оценивания деятельности.

Для решения перечисленных проблем в диссертации предлагается подход к разработке программного обеспечения контроля знаний для систем ЭО, согласно которому описание задачи строится на формальной модели предмета. Решение задачи осуществляется студентом (или учеником) в предметной среде на основе инструментов, являющихся существенными для данного класса задач. Оно автоматически верифицируется программой на формальном описании задачи и не требует предварительного решения задачи автором или проверяющим. Для составления формального описания задач необходимо вводить модели их структуры, а для автоматической верификации задач необходима разработка алгоритмов верификации.

Во второй главе описываются модели самопроверяемой задачи (математическая модель и модель представления знаний об абстрактных задачах), модель жизненного цикла программного обеспечения по составлению и решению самопроверяемых задач и алгоритмы верификации задач классов CodeProblem, Plot-Problem, ExpressionProblem.

Определение 2.1. Описанием условия самопроверяемой задачи называется тройка

P = (T,F,G),

где:

Т-шаблон неформального условия задачи (например: шаблон текста задачи с поясняющими изображениями);

F— формальное условие задачи, Fe'F, где 4х - множество всех возможных формальных условий задачи данного класса;

G — кортеж генерируемых параметров, G = (gl,g2,....gi,.■■&„). Определение 2.2 Абстрактным классом самопроверяемых задач называется класс, обобщающий задачи из нескольких предметных областей.

Определение 2.3. Верификатором задачи называется предикат

V : х £) —> {false, true),

где:

D- множество всех возможных решений задачи данного класса;

Ч* - множество всех возможных формальных условий задачи данного класса.

Верификатор принимает значение true, если задача решена верно.

Определение 2.4. Предметно-ориентированным классом самопроверяемых задач называется класс, обобщающий задачи из конкретной предметной области и описываемый следующим кортежем:

C = (LP,LS,C1, П>),

где:

Lp - предметно-ориентированный язык описания условия задач данного класса;

Ls — предметно-ориентированный язык описания решения задач данного класса;

£i - множество всех возможных инструментов решения задач данного класса;

Q' — множество инструментов, по умолчанию доступных для решения задач данного класса, П'с£1;

v : xFxZ)—> {false, true} - верификатор задачи.

Абстрактная модель, на основе которой возможно построение предметно-ориентированных языков описания условия задачи LP, изображена на рисунке 1 в виде UML-диаграммы классов. Описание задачи состоит из заголовка и четырех списков: неформальных условий, параметров генерации, ограничений на множество инструментов, доступных при ее решении, и верификационных условий.

Рисунок 1 - Абстрактная модель предметно-ориентированных языков описания условия задачи Ьр

На основе абстрактной модели можно построить абстрактную грамматику языка, которая, будучи записанной в форме Бэкуса-Наура, имеет следующий вид:

Описание ::= Заголовок НеформальноеУсловие* ПараметрГенерации* Инструмен-талыюеОграничение* ВерификационноеУсловие* (1)

Модель представления знаний об абстрактной самопроверяемой задаче (онтология) содержит описание класса всех самопроверяемых задач и его абстрактных подклассов. Модель изображена на рисунке 2 в виде концептуального графа (Concept map). Подклассы класса Problem различаются типом среды, в которой решаются задачи или общим видом записи решения, и являются абстрактными (см. определение 2.2), так как не содержат указание на конкретную предметную область, а только на некоторые общие черты различных областей. Задачи класса PlotProblem решаются в графической среде, в которой создается чертеж. Это могут быть задачи по геометрии на построение (среда - система динамической геометрии), по микросхемотехнике на составление схем (среда — система автоматизированного проектирования). К классу CodeProblem относятся задачи по программированию, решаемые в инструментальных средах разработки (например, MATLAB, IntelliJ IDEA). Класс ExpressionProblem содержит задачи, решение которых записывается в виде выражения (например, задачи по физике без конкретных числовых значений).

PfObiem

1

liasParam

{объектное свойство}

Parameter J

hasTlHe (свойство типа даннї;х}_

hasTextTifrsptate ¡саойсіво тапа данных)

^ xaiislrrig j

Является подклассом

^xsdistfjfigJ

[cotfePrafeiemj

Рисунок 2 — Концептуальный граф онтологии абстрактных задач

Для того, чтобы наполнить задачу предметно-ориентированным содержанием, предлагается использовать онтологические модели предметных областей. Полная модель самопроверяемой задачи получается слиянием онтологий абстрактной самопроверяемой задачи и предметных областей.

Представленная в диссертации модель жизненного цикла (рисунок 3) позволяет спроектировать модули контроля знаний для систем ЭО на основании онтологии абстрактных задач (рисунок 2), модели абстрактного предметно-ориентированного языка для описания условий задач (рисунок 1) и алгоритмов верификации.

Метапреподаватель

Составление

( онтологии \предм стной области.

[ Разработка > / предметао-І ориентированных

\ ЯЗЫКОВ у

[есть заме

Программист

'Проверка языков ■ на реализуемость

(Проектирование и реализация программного обеспечения

[есть замечания по инте л гсть замечания по языкам

Рисунок 3 - Модель жизненного цикла программного средства составления и решения самопроверяемых задач

Схема алгоритмов верификации решений для задач класса СоёеРгоЫега (алгоритм 3.1) изображена на рисунке 4 в форме иМЬ-диаграмм деятельности. Сложность (трудоемкость) алгоритма 3.1 имеет следующую оценку:

о(П«,).

/=і

где Пі - количество значений і-того параметра верификации а,

Третья глава посвящена разработке предметно-ориентированных языков для записи задач на построение по геометрии и по цифровой обработке сигналов (ЦОС), а также программной реализации разработанных моделей и алгоритмов в

разработке двух программных средств: для составления и решения задач на построение по геометрии и для поддержки задач по ЦОС.

_ I

Г Инициализация параметров верификации и констант )

( Азд=1тие )

( Проверка выполнения конечных условий ) [нет] ^ [да]

(задание значений вспомогательных переменных )

I _

( Запуск скрипта-решения студента )

I

(проверка правильности ответа) [да] [нет]

Присваивание параметрам верификации значений для следующей итерации

(^Проверка истинности іїад) [Аад==Ь-ие] ^Х^ [Аад==(аІ5е]

I

( Фиксация правильности решения) ( Фиксация неправильности решения)

Рисунок 4 - Блок-схема алгоритма верификации задач класса СоёеРгоЫеш

Для решения задач на построение по геометрии было разработано программное средство WiseTasksGeometry (Wise tasks - умные задачи). Программа использует свободно распространяемую систему динамической геометрии GeoGebra для построения чертежей.

Программное средство WiseTasksDSP (DSP - digital signal processing, ЦОС) предназначено для составления и решения задач в области ЦОС в системе MATLAB.

Согласно классификации самопроверяемых задач (рисунок 2), задачи по геометрии относятся к классу PlolProblem, а задачи в области ЦОС в системе MATLAB - к классу CodeProblem.

Программные средства написаны на языке Java. При проектировании архитектуры программ использовались следующие модели представления знаний:

• онтологическая модель абстрактной самопроверяемой задачи (рисунок 2);

• онтология предметной области для задач на построение по геометрии;

• онтология предметной области для задач по ЦОС в системе MATLAB. Программные средства включают модули учителя (преподавателя) и ученика

(студента), предназначенные соответственно для составления и решения задач. Верификация задач в программах реализована по разработанным автором алгоритмам, описанным во второй главе работы.

В диссертации приведен пример задачи по геометрии (рисунок 5): «Постройте квадрат ABCD со стороной, равной отрезку KL, заданному на чертеже».

Задана Вид Редэкглооганиг Помсшь

^^^■■¿-^^■■■■■■•""••у;.-.............

і Заголовок: Постройте квлдрат ¡угяаэм: псстрайте квдлрзт авто съ гтсронло. равное длине отрезка KL. При вводе ответа обозначьте отрезки следунедим образом; АВ=аВС=Ь СО=С DA=d ІИнструменты: Прямая по двум точкам Параллельная прямая Перпендикулярная пряная окружность по центру а радиусу Отрезок по двум точкам Окружность по центру и точке ¡Предикаты: і а - | с \ і а ¡1 j с

:. j а перп. j b

___ о_______

-4 -3 -2 -1 0 12 3 4 5 8

Рисунок 5 - Задача в модуле учителя

В соответствии с абстрактной грамматикой предметно-ориентированного языка описания условий (1) был разработан предметно-ориентированный язык

описания условия геометрической задачи. Полученная грамматика в расширенной форме Бэкуса-Наура:

Описание ::= Заголовок ТекстовоеУсловие Инструменты Предикаты Заголовок ::= "Заголовок: " Текст ТекстовоеУсловие ::= "Условие: " Текст

Инструменты ::= "Инструменты:" {Инструмент}! "Не ограничивать ученика" Предикаты ::= {Предикат}

Инструмент ::= "Прямая по двум точкам" | "Параллельная прямая" | "Точка" | "Перпендикулярная прямая" | "Окружность по центру и радиусу" | "Середина отрезка" | "Отрезок по двум точкам" | "Угол заданной величины" | "Окружность по центру и точке" | "Угол по трем точкам" | "Луч по двум точкам" Предикат ::= ТочкаЛежитНаПрямой | ПрямыеИлиОтрезкиПараллельны | ПрямыеИлиОт-резкиПерпендикулярны | СерединаОтрезка | ОтрезкиРавны | УглыРавны | ТочкаЛежит-НаОтрезке | ТочкаЛежитНаОкружности | ПрямаяКасаетсяОкружности | ВеличинаУгла [ ДлинаОтрезка

Сравнение программного средства \¥ізеТазкзОеоте1:гу с существующими в мире неполными аналогами приведено в таблице 1.

Таблица 1 - Сравнение средств электронного обучения геометрии

Параметр Живая математика Cabri, Cinderella 1С: Мат Конструктор Auto Graph WiseTasks Geometry

Наличие предметно- ориентированного языка Да Да Да Да Да

«Ручная» верификация Да Да Да Нет Да

Верификация базовых отношений Нет Да Да Да Да

Наличие средств для описания задач Нет Нет Нет Нет Да

Сокращенная грамматика разработанного языка описания условия задачи по ЦОС приведена ниже в расширенной форме Бэкуса-Наура:

Описание ::= Заголовок ТекстовоеУсловие [Изображение] Инструменты Верификатор

Заголовок ::= "Заголовок: " Текст

ТекстовоеУсловие ::= "Условие: " Текст

Изображение ::= "Изображение к условию: " ИмяФайла

Инструменты ::= "Инструменты:" [{Инструмент}]

Верификатор ::= "Верификатор:" КодФункцииВерификатора

Инструмент ::= ТипИиструмента Идентификатор

ТипИнструмента::= "Функция" | "Элемснт"|"Набор функций'Т'Набор элементов"

КодФункцииВерификатора ::= НачФрагментКода "Решение;" КонФрагментКода

В диссертации приведен пример структурированной задачи по ЦОС (рисунок 6).

_в.13Ш

Примеры задач:

;Заголовок: Определение верхней граничной частоты спектра аналогового сигнала '" І Условие: Дан исходный аналоговый сигнал sin) олш-ы N (значения находятся s мг аналогового сигнала), частота дискретизации дискретного сигнала Fs. частоту спектра аналогового сигнала (Fupi по 19%-ному критерию и npd для представления данного сигнала в дискретном виде без потерь инфо8 значение true. Если не подходит, присвоить isOK=false и задать мини* которой выполняется условие теоремы Котельникова.

Изображение к условию:

Инструмен-ы: Набор функций Sintjnal Processing Toclbox

Функция (ft Функция юзх

Верификатор: function ver=ver_freqs{)

N=1080;

і I § " """ і : >

:<л (Ctrl »DELETE)

нажмете CttWIposeJi ддя выборз вариант»« вшща

Рисунок 6 - Модуль преподавателя системы \ViseTasksDSP

Задача посвящена нахождению верхней граничной частоты спектра аналогового (непрерывного) сигнала и проверки частоты дискретизации дискретного сиг-

нала на допустимость для точного (без потерь информации) восстановления исходного аналогового сигнала из дискретного на основе теоремы Котельникова.

Программное средство \ViseTasksDSP в перспективе может также использоваться для составления и решения ряда других известных в ЦОС задач.

Четвертая глава посвящена описанию созданных в рамках проекта «Виртуальный музей занимательной науки» учебных систем удаленного управления ро-бототехническими устройствами. Автор участвовал в проектировании образовательного комплекса «Виртуальный музей занимательной науки», одним из компонентов которого является сеть виртуальных лабораторий. Управлять лабораториями можно дистанционно с помощью \\^еЬ-портала. В связи с этим планируется введение самопроверяемых задач в области удаленного управления устройствами. В диссертации описаны два опытных экспоната виртуальной лаборатории по физике: для изучения центробежной силы (рисунок 7) и равномерного движения по окружности.

лаборатория виртуального музея занимательной науки спбгэту лэти

Экспонат "Центробежная сила"

Экспонат состоит из двигателя, стержня и ло'.астеи. Пластмассовый стержень вставлен в полый вал двигателя. На верху стержня с двух сторон прикоеплены оси, на которых подвешены лопасти. При вращении двига-е/:я лопасти нань'нагот отклоняться от стержня в разные стороны благодаря центробежной силе, угол отклонения лопастей от вертикали увеличивается при росте скорости вращения двигателя

введите скорость вращения двигателя Сот -160 об/мин до 1Ё0 об/мин): j \

Рисунок 7 - Веб-страница экспоната «Центробежная сила»

Пятая глава описывает эксперименты по внедрению результатов диссертации в средней общеобразовательной школе № 521 г. Санкт-Петербурга с углубленным изучением математики и информатики, а также на курсах повышения квалификации учителей «ИНТОКС» (г. Санкт-Петербург). Школьный эксперимент состоял в применении программного средства WiseTasksGeometry для изучения темы «Построение с помощью циркуля и линейки» на уроках геометрии в 8 «А» классе (22 человека). Внедрение результатов диссертации на курсах повышения квалификации состояло во включении темы, посвященной WiseTasksGeomery, в курс изучения компьютерных образовательных средств. Курс был испытан на группе учителей из десяти человек. Результаты экспериментов приведены в таблице 2.

Таблица 2 - Результаты экспериментов по исследованию п рограммы \ViseTasksGeometry

Показатель До использования программы При использовании программы Уменьшение значения показателя

Время, достаточное для освоения учениками нового материала по теме «Построение с помощью циркуля и линейки», академические часы 3 2 33%

Среднее время подготовки учителя к уроку, минуты 120 80 33%

Среднее время проверки учителем решения задачи, минуты 3 0,3 90%

ЗАКЛЮЧЕНИЕ

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

1. Выполнен анализ проблем верификации задач в системах ЭО. Установлено, что на данный момент существуют проблемы использования узкого класса задач, статичности, авторских ошибок в формулировках задач и ошибок в подготовке эталонных ответов.

2. Разработана математическая модель самопроверяемых задач, которая приспособила структуру описания задачи для автоматической верификации.

3. Введена модель абстрактного предметно-ориентированного языка описания условий задач, позволяющая при создании систем ЭО разрабатывать на ее основе конкретные предметно-ориентированные языки.

4. Составлена модель представления знаний об абстрактных самопроверяемых задачах, позволяющая классифицировать задачи, поддерживаемые в системах ЭО.

5. Разработаны алгоритмы верификации задач, позволяющие автоматически верифицировать задачи различных классов.

6. Представлена модель организации жизненного цикла программных средств для решения и составления самопроверяемых задач.

7. Введенные в работе модели использованы в процессе разработки предметно-ориентированных языков для записи условий задач по геометрии и по ЦОС.

8. Рассмотренные в работе модели и алгоритмы использованы в процессе разработки двух программных средств: ^^еТазкзОеотейу для составления и решения задач на построение по геометрии и \ViseTasksDSP для составления и решения задач в области ЦОС.

9. В рамках проекта «Виртуальный музей занимательной науки» разработаны учебные системы удаленного управления устройствами с целью дальнейшего введения самопроверяемых задач в данной области.

10. Осуществлено внедрение результатов диссертации в учебный процесс. В результате эксперимента по использованию системы у учеников повысился интерес к предмету геометрии, на 33% возросла скорость усвоения нового материала и укрепились знания теорем и аксиом, применяемых для решения предложенных за-

дач. У учителей сократилось время подготовки задач к уроку (на 33%) и время на проверку решений учеников (на 90%).

СПИСОК ОПУБЛИКОВАННЫХ РАБОТ ПО ТЕМЕ ДИССЕРТАЦИИ

Публикации в изданиях, рекомендованных ВАК России

1. Перченок О.В. Автоматизация проверки решения геометрических задач по описанию их условий на предметно-ориентированном языке [Текст]/Поздняков С.Н., Перченок О.В., Посов И.А.//Компьютерные инструменты в образовании. -СПб. - 2012. -№ 1.-С. 37-44.

2. Перченок О.В. Автоматизация верификации решения задач в области цифровой обработки сигналов [Текст]/Перчепок О.В., Клионский Д.М. //Компьютерные инструменты в образовании. - СПб. - 2012. - № 3. - С. 28-37.

3. Перченок О.В. Реализация идеи удаленной лаборатории в образовательном комплексе «Виртуальный музей занимательной науки» [Электронный ре-сурс]/Перченок О.В.// Образовательные технологии и общество. - 2012. - №1. - С. 453467. - URL: http://ifets.ieee.org/russian/depository/vl5_il/pdC5.pdf (дата обращения: 28.04.2012).

Публикации в других изданиях и материалах конференций

4. Перченок О.В. Система электронного обучения, обеспечивающая автоматическую проверку решения геометрических задач по описанию их условий [Текст]/Поздняков С.Н., Перченок О.В., Посов И.А.// Материалы VII международной научно-методической конференции "Дистанционное обучение - образовательная среда XXI века", 9-10 ноября 2011. Тезисы доклада. - Минск, 2011. - С. 295296.

5. Перченок О.В. Разработка системы электронного обучения для автоматической верификации решений задач по описанию условия на предметно-ориентированных языках [Текст]/Перчснок О.В.// Материалы XVIII Международной научно-методической конференции "Современное образование: содержание, технологии, качество", 18 апреля 2012. Тезисы доклада. - СПб, 2012. - Т. 1. — С. 223-224.

6. Генерация математических задач и верификация решений в автоматизированных системах поддержки обучения. [Текст]/ Манцеров Д.И., Перченок О.В., Поздняков С.Н. и др.- СПб - Изд-во СПбГЭТУ ЛЭТИ. - 2012. - 154 С.

7. Перченок О.В. Автоматизация верификации решений геометрических задач с использованием предметно-ориеитированного подхода. [Текст]/Перченок О.В. // Сборник научных трудов участников XII Южно-Российской межрегиональной научно-практической конференции-выставки «Информационных технологий в образовании - 2012», 15-16 ноября 2012. Тезисы доклада. - Ростов-на-Дону. - 2012. - С. 75.

8. Перченок О.В. Предметно-ориентированный подход к автоматизации верификации задач [Текст]/Перченок О.В.//Информациош1ые технологии в образовании: Материалы IV Всероссийской научно-практической конференции, 9-10 ноября 2012. Тезисы доклада. - Саратов. - 2012. - С. 207-209.

9. Перченок О.В. Система электронного обучения, обеспечивающая автоматическую проверку математических задач по описанию их условий [Текст] /Перченок О.В.// XVII Санкт-Петербургская Ассамблея молодых ученых и специалистов. Сборник тезисов, 10-15 декабря 2012. Тезисы доклада. - СПб. - 2012. - С. 42.

10. Перченок О.В. Тренажер по решению задач в области цифровой обработки сигналов с помощью инженерно-математического пакета МАТЬАВ [Текст]/Клионский Д.М., Перченок О.В.// Материалы XIX Международной научно-методической конференции "Современное образование: содержание, технологии, качество", 24 апреля 2013. Тезисы доклада.-СПб, 2013.-Т. 1.-С. 149-151.

11. Перченок О.В. Система электронного обучения, обеспечивающая автоматическую проверку решения математических задач по описанию их условий / О.В. Перченок, С.Н. Поздняков, И.А. Посов // Свидетельство об официальной регистрации программы для ЭВМ № 2012611757 от 16 февраля 2012 г.

12. Перченок О.В. Программа составления автоматически верифицируемых задач в области цифровой обработки сигналов / Д.М. Клионский, О.В. Перченок // Свидетельство об официальной регистрации программы для ЭВМ № 2013610852 от 9 января 2013 г.

Перченок Олег Владимирович Модели и алгоритмы верификации решений задач в системах электронного

обучения Автореферат диссертации на соискание учёной степени кандидата технических наук Подписано в печать 10.09.2013. Заказ № 435 Отпечатано с готового оригинал-макета Формат 60*90/16. Усл. печ. л. 1. Тираж 100 экз.

Копировальный центр «Рикон» 195176, Санкт-Петербург, пр. Металлистов, д. 62

Санкт-Петербургский государственный электротехнический университет «ЛЭТИ» им. В.И. Ульянова (Ленина)

На правах рукописи

04201363348 Перченок Олег Владимирович

МОДЕЛИ И АЛГОРИТМЫ ВЕРИФИКАЦИИ РЕШЕНИЙ ЗАДАЧ В СИСТЕМАХ ЭЛЕКТРОННОГО ОБУЧЕНИЯ

Специальность: 05.13.06 - Автоматизация и управление технологическими процессами и производствами (образование)

ДИССЕРТАЦИЯ на соискание ученой степени кандидата технических наук

Научный руководитель: д.п.н. Поздняков С.Н.

Санкт-Петербург - 2013

Содержание

Введение...................................................................................................................5

Глава 1. Верификация задач в системах электронного обучения......................5

1.1 Множественность форм представления знания как основа использования компьютерной поддержки предметного обучения..............11

1.1.1 Множественность форм представления знаний в обучении математике......................................................................................................12

1.1.2 Использование возможностей множественности представления знаний в обучении дискретной математике в технических вузах...........15

1.1.3 Использование возможностей множественности представления знаний в организации и поддержке исследовательской деятельности ... 19

1.2 Подходы к верификации задач по программированию...........................20

1.3 Верификация задач по математике............................................................25

1.3.1 Предметно-ориентированные языки...................................................25

1.3.2 Верификация задач по геометрии.......................................................27

1.3.3 Верификация задач по алгебре............................................................30

1.4 Выводы к первой главе...............................................................................32

Глава 2. Модели и алгоритмы верификации задач............................................33

2.1. Математическая модель самопроверяемой задачи и абстрактная модель языка описания условия....................................................................................33

2.2. Онтология самопроверяемых задач..........................................................36

2.3 Модель жизненного цикла системы электронного обучения, обеспечивающей поддержку самопроверяемых задач..................................38

2.4 Алгоритмы верификации задач..................................................................41

2.4.1 Алгоритм верификации задач класса Сос1еРгоЫет...........................41

2.4.2 Алгоритм верификации задач класса РЫРгоЫет.............................43

2.4.3 Алгоритм верификации задач класса ЕхргеззюпРгоЫет.................46

2.5 Выводы ко второй главе.............................................................................48

Глава 3. Реализация систем электронного обучения, обеспечивающих поддержку самопроверяемых задач....................................................................49

3.1 Система электронного обучения WiseTasksGeometry.............................49

3.1.1 Онтология предметной области...........................................................50

3.1.2 Описание системы.................................................................................54

3.1.3 Сравнение с другими системами динамической геометрии.............64

3.2 Система электронного обучения WiseTasksDSP......................................70

3.2.1 Онтология предметной области...........................................................72

3.2.2 Описание системы.................................................................................72

3.2.4 Сравнение с другими пособиями по изучению MATLAB...............81

3.3 Выводы к третьей главе..............................................................................82

Глава 4. Разработка учебных систем удаленного управления устройствами. 84

4.1 Виртуальный музей занимательной науки...............................................84

4.2 Разработка экспоната «Центробежная сила»............................................88

4.2.1 Физическая реализация........................................................................88

4.2.2 Программная реализация.....................................................................89

4.3 Спецкурс «Удаленное управление устройствами»..................................92

4.4 Экспонат «Равномерное движение по окружности»...............................93

4.5 Выводы к четвертой главе..........................................................................95

Глава 5. Экспериментальное использование результатов диссертации.........97

5.1 Опытная апробация рабочей версии системы WiseTasksGeometry.... 97

5.2 Тестирование второй рабочей версии продукта.................................105

5.2.1 Тестирование полноты решения функциональных задач.............105

5.2.2 Тестирование удобства использования и эксплуатации................107

5.2.3 Прочие виды тестирования...............................................................108

5.3 Доработка рабочей версии по результатам опытной эксплуатации. 109

5.4 Внедрение в средней школе..................................................................111

5.5 Выводы к пятой главе...............................................................................118

Заключение..........................................................................................................120

Литература...........................................................................................................122

3

Приложение А

Введение

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

• использование узкого класса задач (ответ с множественным выбором, ввод числа);

• статичность, которая является потенциальным источником копирования;

• возможные авторские ошибки в формулировках задач;

• возможные ошибки в подготовке эталонных ответов.

Данные недостатки возникают из-за отсутствия средств автоматизации для адекватного описания задачи. Задача описывается неформализованным текстом, при помощи которого невозможно автоматически проверить ее решение. Если при этом составитель задачи допустит ошибку, то правильное решение задачи будет оценено как неверное. Другой проблемой систем электронного обучения является единственность правильного ответа. Данный факт позволяет учащимся легко скопировать ответ в случае его случайного попадания в свободный доступ.

Для решения перечисленных проблем разрабатывается программные средства по составлению и решению задач для систем ЭО, в которых описание задач строится на формальной модели предмета. Решение задачи осуществляется студентом (или учеником) в предметной среде на основе инструментов, являющихся существенными для данного класса задач. Оно автоматически верифицируется системой на формальном описании задачи и не требует предварительного решения задачи автором или проверяющим. Для составления формального описания задач необходимо вводить модели их структуры, а для автоматической верификации задач необходима разработка алгоритмов верификации. Поэтому создание новых моделей и алгоритмов верификации решений задач актуально.

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

В соответствии с указанной целью в работе сформулированы и решены следующие задачи:

1) анализ проблем верификации решений задач в современных системах ЭО;

2) разработка математической модели самопроверяемой задачи;

3) создание модели представления знаний об абстрактных самопроверяемых задачах;

4) разработка модели абстрактного предметно-ориентированного языка для описания условий задач;

5) введение модели жизненного цикла программного средства по решению и составлению самопроверяемых задач;

6) создание алгоритмов верификации самопроверяемых задач;

7) разработка предметно-ориентированных языков для записи условий задач по геометрии и цифровой обработке сигналов;

8) разработка программных средств для решения и составления задач по геометрии и по цифровой обработке сигналов на основе разработанных моделей и алгоритмов;

9) разработка учебных систем удаленного управления устройствами с целью дальнейшего введения самопроверяемых задач в данной области;

10) экспериментальное исследование результатов диссертации практике.

Объектом исследования являются программные модули систем ЭО, обеспечивающие верификацию решений задач.

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

Методы исследования. При решении поставленных задач использовалась теория формальных языков, теория искусственного интеллекта, теория алгоритмов.

Положения, выносимые на защиту:

1) разработана математическая модель самопроверяемой задачи;

2) создана модель представления знаний об абстрактных самопроверяемых задачах;

3) разработана модель абстрактного предметно-ориентированного языка для описания условий задач;

4) разработана модель жизненного цикла программного средства для решения и составления самопроверяемых задач;

5) созданы алгоритмы верификации самопроверяемых задач;

6) разработан предметно-ориентированный язык описания задач на построение по геометрии;

7) разработан предметно-ориентированный язык описания задач в области цифровой обработки сигналов;

8) разработано программное средство по решению и составлению задач на построение по геометрии;

9) создано программное средство по решению и составлению задач для цифровой обработки сигналов;

10) разработаны программные средства - учебные системы удаленного управления робототехническими устройствами для изучения центробежной силы и равномерного движения по окружности;

11) проведен эксперимент по исследованию разработанных программных средств в двух учебных заведениях.

Научная новизна. Следующие результаты диссертации обладают

научной новизной:

1) новая математическая модель самопроверяемых задач, которая

приспосабливает структуру условия задачи для автоматической

верификации и устанавливает взаимосвязи между математическими

7

объектами «самопроверяемая задача», «абстрактный класс самопроверяемых задач», «предметно-ориентированный класс самопроверяемых задач», «верификатор задачи»;

2) модель абстрактного предметно-ориентированного языка описания условий задач, описывающая абстрактный синтаксис нового класса предметно-ориентированных языков, определяющая составные части описания задачи: неформальные условия, верификационные условия, инструментальные ограничения и параметры генерации;

3) алгоритмы верификации решений, впервые разработанные для поддержки самопроверяемых задач классов Р1о1РгоЫет, Сос1еРгоЫет и ЕхргеззюпРгоЫет, позволяющие установить правильность решения студента или учащегося путем применения к нему верификационных условий, заданных преподавателем или учителем при составлении задачи.

Достоверность научных результатов и выводов. Подтверждается корректным обоснованием постановок задач, точной формулировкой критериев, проведённым анализом базовых работ в исследуемой области, а также актами внедрения.

Практическая значимость работы подтверждается результатами экспериментального исследования разработанного программного средства для составления и решения задач по геометрии. При использовании программы у учеников повысился интерес к предмету геометрии, возросла на 33% скорость усвоения нового материала и укрепились знания теорем и аксиом, применяемых для решения предложенных задач. У учителей сократилось время подготовки задач к уроку (на 33%) и время на проверку решений учеников (благодаря автоматической верификации на 90%).

Внедрение результатов. Результаты диссертационного исследования

были использованы при проведении в Санкт-Петербургском

государственном электротехническом университете «ЛЭТИ» им. В.И.

Ульянова-Ленина научно-исследовательской работы «Программа

8

стратегического развития СПбГЭТУ ЛЭТИ» (2012-2013, тема № ВМ-2-24): разработано и внедрено два программных продукта (имеются свидетельство о регистрации программы «Система ЭО, обеспечивающая автоматическую проверку решения математических задач по описанию их условий» № 2012611757 от 16.02.2012 г. и свидетельство о регистрации «Программы составления автоматически верифицируемых задач в области цифровой обработки сигналов» № 2013610852 от 9.01.2013 г.). Программное средство по геометрии внедрено в образовательный процесс в средней школе № 521 Санкт-Петербурга с углубленным изучением математики и информатики, а также на курсах повышения квалификации учителей в обществе с ограниченной ответственностью «ИНТОКС» (г. Санкт-Петербург). Работа поддержана грантом правительства Санкт-Петербурга для студентов и аспирантов в 2012 г. (Диплом серии ПСП № 12286).

Апробация результатов работы. Основные положения и результаты работы докладывались и обсуждались на VII международной научно-методической конференции "Дистанционное обучение - образовательная среда XXI века" (Минск, декабрь 2011 г.); на XVIII Международной научно-методической конференции "Современное образование: содержание, технологии, качество» (СПб, апрель 2012 г); на XII Южно-Российской межрегиональной научно-практической конференции-выставки

«Информационных технологии в образовании - 2012» (Ростов-на-Дону, ноябрь 2012 г); на IV Всероссийской научно-практической конференции «Информационные технологии в образовании» (Саратов, ноябрь 2012 г.); на XVII Санкт-Петербургской Ассамблее молодых ученых и специалистов (СПб, декабрь 2012 г.); на 12-ом международном конгрессе по математическому образованию ICME-12 (Сеул, Корея, июль 2012 г.); на XIX Международной научно-методической конференции "Современное образование: содержание, технологии, качество» (СПб, апрель 2013 г).

Публикации. По теме диссертации опубликованы 10 научных работ,

включая 3 статьи в изданиях, рекомендованных ВАК РФ, 6 работ в

9

материалах международных, национальных и региональных конференций и 1 коллективную монографию.

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

Глава 1. Верификация задач в системах электронного обучения

1.1 Множественность форм представления знания как основа использования компьютерной поддержки предметного обучения

В основе инструментального подхода лежит теория информационной среды обучения [1]. Теория информационной среды базируется на многообразии форм, в которых аккумулируется и передаётся знание. Другой важной особенностью теории является то, что в ней при оценке педагогической эффективности использования компьютера в обучении на первое место выдвигается принципиальная роль инструментальных средств. Этот вывод базируется на работах Выготского [2] и Леонтьева [3], посвященных роли орудий в развитии ребенка и процессам интериоризации, происходящим в процессе деятельности человека. Развивая идеи об использовании инструментов в образовании, Dubinsky [4] вводит понятие инкапсуляции, предлагая рассматривать процессы интериоризации (Леонтьев, Выготский) во взаимосвязи с процессами инкапсуляции, которые описывают процесс абстрагирования понятий. Одним из важных выводов, полученных в этих исследованиях, является то, что результаты Пиаже [5] относительно когнитивных механизмов, лежащих в основе индивидуального познания, не отличаются принципиально у старших и младших школьников. Thurston [6] в своих работах (1995) развивает идеи Выготского, рассматривая как важную часть обучения его контекст, связанный с неформальным общением учителя и ученика, позволяющий ученику копировать приемы мышления своего учителя. Он объясняет, как в рамках некоторого предметного поля знаний люди развивают область общего знания и общей техники работы с ним. Ключом к этому аспекту коммуникации являются не символы или картинки, но инкапсулированные в простых понятиях сложные идеи. Dorfler (1993, 2000) [7,8] развивает идеи Выготского в теории распределенного познания, в соответствии с которой познание является функцией не только индивидуума,

но и его окружения. Он рассматривает компьютер как современный мощный инструмент когнитивной технологии, что является обобщением работ Pea (1987) [9] и Dreyñis (1994) [10]. В этих работах познание рассматривается в зависимости от всех подходящих познавательных инструментов, имеющихся в распоряжении обучаемого. В контексте этих исследований это познавательное окружение включает не только компьютер, но и все ресурсы, которые могут быть доступны посредством компьютера.

1.1.1 Множественность форм представления знаний в обучении математике

Формирование информационной среды процесса обучения требует изучения форм, в которых передается знание. Даже беглый взгляд на преподавание любого предмета показывает постоянное изменение этих форм и параллельное существование различных форм. Формы представления знаний зависят и от самого предмета. На эволюцию форм влияет развитие предмета и изменение взглядов на психологию обучения. В конечном счете, предметный и психологический фактор синтезируются в методических воззрениях. Анализ различных подходов к преподаванию с точки зрения форм представления знания был сделан в работе [1]. Приведем кратко основные результаты, сформулированные в монографии [1].

Представление знания моделя�