2020 Fiscal Year Research-status Report
Automatic generation of programming questions by symbolic execution
| Project/Area Number |
20K12106
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
斎藤 俊則 星槎大学, 教育実践研究科, 准教授 (80434447)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | プログラミング教育 / 情報教育 / プログラミング言語 / 記号実行 / 定理証明 / 仕様記述・検証 / ソフトウェアテスト |
|---|
| Outline of Annual Research Achievements |
本研究では，(a)選択式・○×式のプログラミングの試験問題を自動生成する手法，および，(b)一般的なプログラミング試験問題の自動採点手法の開発を目指している．2020年度は，(a)に関しては方向性に関する議論を行うにとどめ，主として(b)の開発を行った．
既存の自動採点方法として，入力を多数用意して答案による出力と正解出力を比較する方法があるが，この方法では，誤答を正解と判定する可能性がある．これに対し，プログラムが満足すべき性質を表明として記述し，記号実行によってその表明が成り立つことを確認できれば，確実に正答であると判断できる．しかし一般には，表明が成り立つことを判定することは困難である．そこで，プレスバーガー算術の充足可能性判定が決定可能であることに注目した．プログラミング言語として，プレスバーガー算術で表現できることしか記述できないものを作成すればよい．条件付き繰返し文に適切な制約を導入することによって，この性質を満たすプログラミング言語を設計した．条件を満たす要素のカウント，バブルソート，二分探索など，プログラミング初学者が学ぶアルゴリズムを表現することができるように，定数長配列も扱うことができるようにした．
以上の手法を実装したツールを試作した．解答作成用のプログラミング言語は，C/Java風の手続き型言語とし，パーザと記号実行を行う処理系を，Python言語を用いて開発した．プレスバーガー算術の充足可能性判定器としてはZ3を用い，そのPython言語バインディングを利用した．
初学者が学ぶアルゴリズムを実装させる試験問題に対する解答例を用いて，試作したツールの評価を行った．誤った解答の検出に対してはおおむね十分な性能を持つことがわかった．正解の確認に関しては，予想通り性能上の問題があったが，出題方式を短冊式とする場合には現実的な解となりうることが確認された．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
試験問題の自動生成手法については，方向性の検討にとどまって，詳細な技術開発には至らなかった．一方で，答案の評価手法については，具体的な手法を確立しただけにとどまらず，2020年度に予定していなかったツールの試作まで進めることができた．総合的に判断しておおむね順調な進展と言うことができる．
|
| Strategy for Future Research Activity |
選択式・○×式の試験問題を用意したプログラムから多数自動生成する手法については，引き続き検討を進める．
答案評価手法については，昨年度に試作したツールの使用条件に合致する具体的な問題例を多数作成し，実際にプログラミング初学者に受験をしてもらうことで，その効果を測定する．そのために，Web上で受験できるCBT(computer-based testing)のシステムを作成する．
|
| Causes of Carryover |
本年度は新型コロナ対策のため、出張ができなかったため。次年度の出張および機材購入に使用する。
|
Research Products
(2 results)
