A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material

CiteSeerX - Document Details (Isaac Councill, Lee Giles, Pradeep Teregowda):
of 5
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
  A corpus of tutorial dialogs on theorem proving;the influence of the presentation of the study-material. Christoph Benzm ¨uller † , Helmut Horacek † , Henri Lesourd † ,Ivana Kruijff-Korbayova ∗ , Marvin Schiller † , Magdalena Wolska ∗ † Fachrichtung Informatik   ∗ Fachrichtung Allgemeine Linguistik Universit¨at des Saarlandes, Postfach 15 11 50, D-66041 Saarbr¨ucken, Germany { chris,horacek,henri,schiller }, { korbay,magda } Abstract We present a new corpus of tutorial dialogs on mathematical theorem proving that was collected in a Wizard-of-Oz setup. Our studyis a follow up on a previous experiment conducted in a similar simulated environment. A major difference between the current and theprevious experimental setup was that in this study we varied the presentation of the study-material withwhich the subjects were provided.One sub-group of the subjects was presented with a highly formalized presentation consisting mainly of formulas, while the other witha presentation mainly in natural language. Our goal was to obtain more data on the kind of mixed-language that is characteristic of informal mathematical discourse. We hypothesized that the language style of the subjects’ interaction with the simulated system willreflect the style of presentation of the study-material. In the paper we briefly present the experimental setup, the corpus, and a preliminaryquantitative results of the corpus analysis. 1. Introduction In the D IALOG 1 project (Benzm¨uller et al., 2003a),we are investigating and modeling semantic and pragmaticphenomena in student-tutor dialogs on problem solvingskills in mathematics. Our goal is to empirically investi-gate the use of flexible natural language dialog in tutoringmathematics, and to develop a prototype tutoring systemgradually embodying the empirical findings.In (Wolska et al., 2004), we presented an annotated cor-pus of tutorial dialogs on theorem proving collected in aWizard-of-Oz setup (Benzm¨uller et al., 2003b) in whichsubjects interact with a system simulated by a human “wiz-ard” (Fraser and Gilbert, 1991; Dahlb¨ack et al., 1993;Maulsbyet al., 1993). As noted in (Zinn, 2003; Wolska andKruijff-Korbayov´a, 2004; Horacek and Wolska, 2005), theprominent property of the language of mathematical textsis that it consists of interleaved natural and (semi-) formallanguage: conventionalizedmathematicalexpressions. Fol-lowinguponthepreviousstudy,we presentanewcorpusof tutorial dialogs on mathematical theorem proving collectedin a recently completed experiment conducted in a simi-lar simulated environment. Our goal was to obtain moredata onthe kind of mixed-languageinteractionas discussedin (Horacek and Wolska, 2005).The previous study dealt with the domain of naive settheory. For the second experiment, we chose the domainof binary relations. The reason for the choice of a differentdomain was, among others, to facilitate future investiga-tion the scalability of our input interpretation component.A major difference in the experimental setup was that inthe recently completed follow-up experiment we varied thepresentation of the study-material with which the subjects 1 The D IALOG project isacollaboration between the ComputerScience and Computational Linguistics departments of Universityof the Saarland as part of the Collaborative Research Center on  Resource-Adaptive Cognitive Processes , SFB 378 ( ). were provided: highly formalized presentation consistingmainly of formulas vs. presentation in natural language.Our aim was to elicit the mixed-language style of informalproofs. The hypothesis was that the language style of thesubjects’ interaction with the simulated system will reflectthe style of presentation of the study-material. In the lastsection of this paper, we present a preliminary data analy-sis with respect to this question.Below, we present the setup of the corpus collectionexperiment, in particular, pointing out differences with re-spect to the previous study, the corpus itself, and the pre-liminary quantitative results of a comparative study of thedialogs obtained in the two conditions. 2. The corpus collection experiment We invited thirty seven subjects to participate in the ex-periment. The subjects were Saarland University studentsof different educational backgrounds. A prerequisite forparticipation was that the candidate subjects had taken atleast one mathematics course at the university level. Thesubjects were informed that they were interacting with aconversational system with natural language capabilities.We provided the subjects with background reading ma-terial for the domain of binary relations (see Section 2.1.)and allowed a study time before starting the tutoring ses-sion. Next, we asked the subjects to prove four theoremsusing the system ( R ,  S  , and  T   are binary relations on a set M  ): W.  ( R ◦ S  ) − 1 =  S  − 1 ◦ R − 1 A.  ( R ∪ S  ) ◦ T   = ( R ◦ T  ) ∪ ( S   ◦ T  ) B.  ( R ∪ S  ) ◦ T   = ( T  − 1 ◦ S  − 1 ) − 1 ∪ ( T  − 1 ◦ R − 1 ) − 1 C.  ( R ∪ S  ) ◦ S   = ( S   ◦ ( S   ∪ S  ) − 1 ) − 1 E.  Assume  R  is asymmetric. If   R  is not empty (i.e.  R   =  ∅ ,then  R   =  R − 1 ) Exercises  W. ,  A. ,  B. , and  C. 2 build upon each other inthat once solved, they may be used in the subsequent exer- 2 Exercise  C.  is a theorem if   S   is a symmetric relation, but not  Sind  A,B  Mengen und gilt ∀ x ( x  ∈  A  ⇒  x  ∈  B ) , so heißt  A  eine  Teilmenge  von  B . Man schreibtdaf¨ur A  ⊆  B .Sind  A,B  Mengen und gilt daß jedes Element vonA auch Element von B ist, so heißt  A  eine  Teil-menge  von  B . Man schreibt daf¨ur A  ⊆  B .  If   A  and   B  are sets and   ∀ x ( x  ∈  A  ⇒  x  ∈  B )  holds,then  A  is called a subset of   B . We write A  ⊆  B . If   A  and   B  are sets and it is the case that every element of   A  is also an element of   B  , then  A  is called a subset of  B . We write A  ⊆  B . Figure 1: Presentation of the Subset definition in the “formal” (left) and “verbose” (right) material. Theorem Sei  R  eine Relation in einer Menge  M  . Es gilt:  R  = ( R − 1 ) − 1 Proof  Eine Relation ist definiert als eine Menge von Paaren. Die obige Gleichheit ist demnach eine Gleichung zwis-chen zwei Mengen. Mengengleichungen kann man nach dem Prinzip der Extensionalitaet dadurch beweisen,dass man zeigt, das jedes Element der ersten Menge auch Element der zweiten Menge ist. Sei also  ( a,b )  einPaar in  M   ×  M  , dann ist zu zeigen  ( a,b )  ∈  R  genau dann wenn  ( a,b )  ∈  ( R − 1 ) − 1 .  ( a,b )  ∈  ( R − 1 ) − 1 giltnach Definition der Umkehrrelation genau dann wenn  ( b,a )  ∈  R − 1 und dies gilt nach erneuter Definition derUmkehrrelation genau dann wenn  ( a,b )  ∈  R , was zu zeigen war.  Let   R  be a relation on a set   M  . Prove:  R  = ( R − 1 ) − 1  A relation is defined as a set of pairs. The above equation expresses an equality between sets. Set equality can be provenby The Principle of Extensionality, where one shows that every element of one set is also an element of the other set. Let  ( a,b )  be a pair on  M   × M  . We have to show that   ( a,b )  ∈  R  if and only if   ( a,b )  ∈  ( R − 1 ) − 1 .  ( a,b )  ∈  ( R − 1 ) − 1 holds bydefinition of the inverse relation if and only if   ( b,a )  ∈  R − 1 and this again holds by the definition of the inverse relation if and only if   ( a,b )  ∈  R  , which was to be proven. Figure 2: Example proof.cises. Exercise  W.  was a warm-up exercise and exercise  E. was presented only to those subjects who had difficulties incompleting the initial exercise.We instructed the subjects to enter proof steps, ratherthan complete proofs at once, to encourage dialog with thesystem, as well as to think aloud while solving the exer-cises. The language of the dialogs was German. The di-alogs were typed using keyboard and/or buttons availableon the user interface (see Section 2.2.). Both the wizardsand the subjects were free in the way they formulated theirturns. 2.1. The study material The subjects were provided with preparatory material(adaptedfrom (Bronsteinand Semendjajew,1991))review-ing the notions, definitions, and basic theorems in binaryrelations, and were allowed 25 minutes to revise beforestarting the tutoring session. They were divided into twogroups: a sub-group of twenty subjects was provided witha formalized presentation of the study material, while theother sub-group was presented with material that avoidedformalization, and used natural language verbalization in- in the general case. The expectation was that the subjects wouldbe able to provide an argument for this. stead. In Figure 1, we show the definition of a subset as itappeared in both versions to illustrate the difference. Thesubjectswerealsoprovidedwithanexampleproofofasim-ple theorem, shown in Figure 2, that used a mixture of nat-ural language and mathematical expressions. 2.2. The interface The interaction between the subject and the wizard wasmediated by a chat environment with a Graphical User In-terface (GUI) that consisted of a customized version of theTeXmacs  3 editor; a L A TEX editor operating in the  what- you-see-is-what-you-get   mode. The advantage of usingTeXmacs was that the subjects were given multiple alter-natives for inserting mathematical expressions: traditionalGUI buttons with symbols, srcinal L A TEX commands (e.g. \ cup ), as well as German translations of the L A TEX com-mands (e.g.  \ Vereinigung  for the set union). 4 Addi-tionally, the GUI supported  copy and paste  functionality 3 4 All the available commands were printed on a handout. Priorto starting the tutoring sessions, the subjects were instructed onusing the GUI (in particular, shown the different input modes forformulas) byoneof theexperimenters, and hadafew minutestimeto familiarize themselves with the GUI in a typing exercise.  min max mean median stdFM nl 49.00 354.00 173.85 158.50 87.53FM math 0.00 80.00 11.65 4.00 19.24VM nl 93.00 364.00 209.88 210.00 70.32VM math 1.00 48.00 16.82 14.00 13.74 Table 4: Distribution of natural language vs. symbolic to-kens in the wizard turns per session in the two conditions.use fewerandshorterformulas. Thelargemaximalformulalength in both conditions, we believe, might be an artifactof the interface’s  copy and paste  mechanism. Discussion  A preliminary analysis of the corpus data re-veals differences in the use of natural language vs. formu-las. One of the factors contributing to this difference maybe the format of the presentation of the study material hav-ing a priming effect. However, other factors may includethe wizard’s style of interaction and the alignment effect,or the individualmathematical skills of the student. Table 4shows the distribution of the natural language vs. symbolictokens per session in the wizard turns. We do not showthe formula length counts because the wizards sometimescopied even lengthy subjects’ formulas into their turns, forinstance, while asking clarification questions. Althoughthere is little difference between the two conditions here,a difference may be in the specifics of styles of subject-wizard pairs and have to do with the mathematical skills of the student. We plan to investigate this in the future. 4. Related work With respect to tutorial dialog corpora,a numberof col-lections of tutorial dialogs have been analyzed, a selectionof which can be found at the CIRCLE website. 7 (Tomkoand Rosenfeld, 2004) study of the effect of instructionsabout the system’s language capabilities given to partici-pants of a Wizard-of-Oz experiment with a speech-baseddialog system. The goal was to investigate how easily theusers can be persuaded to use a restricted input style. Thestudy finds that all uses were adapting their language tothe system’s language. (Dahlqvist et al., 1999) presents astudy on presentational formats and implications on learn-ing in the domain of physics. The effect of linguistic align-ment in interactions with dialog systems has been widelystudied(Ringle and Halstead-Nussloch,1989; Zoltan-Ford,1991; Brennan and Ohaeri, 1994). 5. Conclusion The paper presents a new corpus of tutorial dialogs onmathematical problem solving collected in a Wizard-of-Ozsetup. In order to elicit a mixed-language style of interac-tion, we divided the subjects into two groups and providedthem with different presentations of the material (formal-ized and verbose). We hypothesized that the format of thestudymaterialmayinfluencetheway thesubjectswouldin-teract with the system. The analysis of the corpus revealeddifferences in the language used by the subjects related to 7˜circle/Archive.htm the style of presentation, which confirms our hypothesis.However, investigation of other factors that may have in-fluenced the subjects, such as individual differences in theinteraction styles between subject-wizard pairs is needed. 6. References C. Benzm¨uller, A. Fiedler, M. Gabsdil, H. Horacek, I.Kruijff-Korbayov´a, M. Pinkal, J. Siekmann, D. Tso-valtzi, B.Q. Vo, and M. Wolska. 2003a. Tutorial dialogson mathematical proofs. In  Proc. of the IJCAI WorkshoponKnowledgeRepresentationandAutomatedReasoning for E-Learning Systems , pp. 12–22.C. Benzm¨uller, A. Fiedler, M. Gabsdil, H. Horacek, I.Kruijff-Korbayov´a, M. Pinkal, J. Siekmann, D. Tso-valtzi, B.Q. Vo, and M. Wolska. 2003b. A Wizard-of-Oz experiment for tutorial dialogues in mathematics. In  AIED-03 Supplementary Proc. , Advanced Technologiesfor Mathematics Education, pp. 471–481.S.E. Brennan and J.O. Ohaeri. 1994. Effects of messagestyle on users’ attributions toward agents. In  CHI -94:Conference companion on Human factors in computingsystems , pp. 281–282.I.N. Bronstein and K.A. Semendjajew. 1991.  Taschenbuchder Mathematik  . Teubner.N. Dahlb¨ack, A. J¨onsson, and L. Ahrenberg. 1993. Wizardof Oz studies: why and how. In  Proc. of the 1st Inter-national Conference on Intelligent User Interfaces , pp.193–200.P. Dahlqvist, R. Ramberg, and Y. Waern. 1999. The effectsof different presentation formats on learning. In  Euro- pean Association for Research on Learning and Instruc-tion .N.M. Fraser and G.N. Gilbert. 1991. Simulating speechsystems.  Computer Speech and Language , 5:81–99.H. Horacek and M. Wolska. 2005. Interpretation of mixedlanguage input in a mathematics tutoring system. In Proc. of the AIED-05 Workshop on Mixed Language Ex- planations in Learning Environments , pp. 27–34.D.Maulsby,S. Greenberg,andR. Mander. 1993. Prototyp-ing an intelligent agent through Wizard of Oz. In  Con- ference on Human Factors in Computing Systems , pp.277–285. ACM Press.M.D. Ringle and R. Halstead-Nussloch. 1989. Shapinguser input: a strategy for natural language dialogue de-sign.  Interacting with Computers , 1(3):227–244.S.TomkoandR.Rosenfeld. 2004. Shapingspokeninputinuser-initiative systems. In  The 8th International Confer-ence on Spoken Language Processing , pp. 2825–2828.M. Wolska and I. Kruijff-Korbayov´a. 2004. Analysis of Mixed Natural and Symbolic Language Input in Math-ematical Dialogs. In  Proc. of the 42nd Meeting of the Association for Computational Linguistics , pp. 25–32.M. Wolska, B.Q. Vo, D. Tsovaltzi, I. Kruijff-Korbayov´a,E.Karagjosova, H. Horacek, M. Gabsdil, A. Fiedler, andC. Benzm¨uller. 2004. An annotated corpus of tutorialdialogs on mathematical theorem proving. In  Proc. of  International Conference on Language Resources and  Evaluation , pp. 1007–1010.C. Zinn. 2003. A Computational Framework For Under-  standing Mathematical Discourse.  Logic Journal of the IGPL , 11(4):457–484.E. Zoltan-Ford. 1991. How to get people to say and typewhat computers can understand.  International Journalof Man-Machine Studies , 34(4):527–547.
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!