Abstract
Many educational applications, from tutoring to problem generation, are built on a formal model of the operational knowledge for a given domain. These domain models consist of rewrite rules that experts apply to solve problems in the domain; e.g., factoring, \(ax + bx \rightarrow (a+b)x\), is one such rule for K-12 algebra. Domain models currently take hundreds of hours to create, and they differ widely in how well they meet educational objectives such as maximizing problem-solving efficiency. Rapid, objective-driven creation of domain models is a key challenge in the development of personalized educational tools.
This paper presents \(\textsc {RuleSy}_{}\), a new framework for computer-aided authoring of domain models for educational applications. \(\textsc {RuleSy}_{}\) takes as input a set of example problems (e.g., \(x + 1 = 2\)), a set of basic axiom rules for solving these problems (e.g., factoring), and a function expressing the desired educational objective. Given these inputs, it first synthesizes a set of sound tactic rules (e.g., combining like terms) that integrate multiple axioms into advanced problem-solving strategies. The axioms and tactics are then searched for a domain model that optimizes the objective. \(\textsc {RuleSy}_{}\) is based on new algorithms for mining tactic specifications from examples and axioms, synthesizing tactic rules from these specifications, and selecting an optimal domain model from the axioms and tactics.
We evaluate \(\textsc {RuleSy}_{}\) on the domain of K-12 algebra, finding that it recovers textbook tactics and domain models, discovers new tactics and models, and outperforms a prior tool for this domain by orders of magnitude. But \(\textsc {RuleSy}_{}\) generalizes beyond K-12 algebra: we also use it to (re)discover proof tactics for propositional logic, demonstrating its potential to aid in designing models for a variety of educational domains.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andersen, E., Gulwani, S., Popović, Z.: A trace-based framework for analyzing and synthesizing educational progressions. In: CHI (2013)
O’Rourke, E., Andersen, E., Gulwani, S., Popović, Z.: A framework for automatically generating interactive instructional scaffolding. In: Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems, CHI 2015, pp. 1545–1554. ACM, New York (2015)
Anderson, J.R., Corbett, A.T., Koedinger, K.R., Pelletier, R.: Cognitive tutors: Lessons learned. The Journal of the Learning Sciences 4(2), 167–207 (1995)
VanLehn, K.: Mind bugs: The origins of procedural misconceptions. MIT press (1990)
Murray, T.: Authoring intelligent tutoring systems: An analysis of the state of the art. International Journal of Artificial Intelligence in Education 10 (1999)
Liu, Y.E., Ballweber, C., O’rourke, E., Butler, E., Thummaphan, P., Popović, Z.: Large-scale educational campaigns. ACM Trans. Comput.-Hum. Interact. 22(2), 8:1–8:24 (2015)
Demski, J.: This time it’s personal: True student-centered learning has a lot of support from education leaders, but it can’t really happen without all the right technology infrastructure to drive it. and the technology just may be ready to deliver on its promise. THE Journal (Technological Horizons In Education) 39(1), 32 (2012)
Redding, S.: Getting personal: the promise of personalized learning. In: Handbook on Innovations in Learning, pp. 113–130 (2013)
Charles, R.I., Hall, B., Kennedy, D., Bellman, A.E., Bragg, S.C., Handlin, W.G., Murphy, S.J., Wiggins, G.: Algebra 1: Common Core. Pearson Education, Inc. (2012)
Sweller, J.: Cognitive load during problem solving: Effects on learning. Cognitive Science 12(2), 257–285 (1988)
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th Inter. Conf. on Architectural Support for Programming Languages and Operating Systems. ACM (2006)
Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (2014)
Alur, R., Bodík, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, pp. 1–25 (2015)
Dershowitz, N., Jouannaud, J.P.: Handbook of Theoretical Computer Science, vol. b, pp. 243–320. MIT Press, Cambridge (1990)
Butler, E., Torlak, E., Popović, Z.: A framework for parameterized design of rule systems applied to algebra. In: Micarelli, A., Stamper, J., Panourgia, K. (eds.) ITS 2016. LNCS, vol. 9684, pp. 320–326. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39583-8_36
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, New York Inc (2007)
Butler, E., Torlak, E., Popovic, Z.: Synthesizing optimal domain models for educational applications. Technical Report UW-CSE-17-10-02, University of Washington (2017). https://www.cs.washington.edu/tr/2017/10/UW-CSE-17-10-02.pdf
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Butler, E., Torlak, E., Popovic, Z.: Rulesy source code and data. https://github.com/edbutler/nonograms-rule-synthesis
Harel, G., Sowder, L.: Toward comprehensive perspectives on the learning and teaching of proof. Second Handbook of Research on Mathematics Teaching and Learning 2, 805–842 (2007)
Langley, P., Laird, J.E., Rogers, S.: Cognitive architectures: Research issues and challenges. Cognitive Systems Research 10(2), 141–160 (2009)
Laird, J.E., Newell, A., Rosenbloom, P.S.: Soar: An architecture for general intelligence. Artificial Intelligence 33(1), 1–64 (1987)
Anderson, J.R., Lebiere, C.: The atomic components of thought (1998)
Korf, R.E.: Macro-operators: A weak method for learning. Artificial Intelligence 26(1), 35–77 (1985)
Koedinger, K.R., Brunskill, E., Baker, R.S., McLaughlin, E.A., Stamper, J.: New potentials for data-driven intelligent tutoring system development and optimization. AI Magazine 34(3), 27–41 (2013)
Matsuda, N., Cohen, W.W., Koedinger, K.R.: Applying programming by demonstration in an intelligent authoring tool for cognitive tutors. In: Aaai Workshop on Human Comprehensible Machine Learning (technical report ws-05-04), pp. 1–8 (2005)
Li, N., Cohen, W., Koedinger, K.R., Matsuda, N.: A machine learning approach for automatic student model discovery. In: Educational Data Mining 2011 (2010)
Li, N., Schreiber, A.J., Cohen, W., Koedinger, K.: Efficient complex skill acquisition through representation learning. Advances in Cognitive Systems 2 (2012)
Jarvis, M.P., Nuzzo-Jones, G., Heffernan, N.T.: Applying machine learning techniques to rule generation in intelligent tutoring systems. In: Lester, J.C., Vicari, R.M., Paraguaçu, F. (eds.) ITS 2004. LNCS, vol. 3220, pp. 541–553. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30139-4_51
Schmid, U., Kitzelmann, E.: Inductive rule learning on the knowledge level. Cognitive Systems Research 12(3), 237–248 (2011)
Gulwani, S.: Example-based learning in computer-aided stem education. Communications of the ACM 57(8), 70–80 (2014)
Lazar, T., Bratko, I.: Data-driven program synthesis for hint generation in programming tutors. In: Trausan-Matu, S., Boyer, K.E., Crosby, M., Panourgia, K. (eds.) ITS 2014. LNCS, vol. 8474, pp. 306–311. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07221-0_38
Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (2013)
Tillmann, N., de Halleux, J., Xie, T., Bishop, J.: Constructing coding duels in Pex4Fun and Code Hunt. In: ISSTA, pp. 445–448. ACM (2014)
Lee, C.: DeduceIt: a tool for representing and evaluating student derivations. Stanford Digital Repository (2012). http://purl.stanford.edu/bg823wn2892
Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. In: Proceedings of the 2015 ACM SIGPLAN Inter. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, pp. 107–126. ACM (2015)
Liang, P., Jordan, M.I., Klein, D.: Learning programs: a hierarchical bayesian approach. In: Proceedings of the 27th International Conference on Machine Learning (ICML 2010), pp. 639–646 (2010)
Dershowitz, N., Jouannaud, J.P.: Rewrite systems. Citeseer (1989)
Oppen, D.C.: Reasoning about recursively defined data structures. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 151–157. ACM (1978)
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. ACM Sigplan Notices 45(1), 199–210 (2010)
Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science 174(8), 23–37 (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Butler, E., Torlak, E., Popović, Z. (2018). A Framework for Computer-Aided Design of Educational Domain Models. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-73721-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-73720-1
Online ISBN: 978-3-319-73721-8
eBook Packages: Computer ScienceComputer Science (R0)