Search for: All records

Reactive synthesis holds the promise of generating automatically a verifiably correct program from a high-level specification. A popular such specification language is Linear Temporal Logic (LTL). Unfortunately, synthesizing programs from general LTL formulas, which relies on first constructing a game arena and then solving the game, does not scale to large instances. The specifications from practical applications are usually large conjunctions of smaller LTL formulas, which inspires existing compositional synthesis approaches to take advantage of this structural information. The main challenge here is that they solve the game only after obtaining the game arena, the most computationally expensive part in the procedure. In this work, we propose a compositional synthesis technique to tackle this difficulty by synthesizing a program for each small conjunct separately and composing them one by one. While this approach does not work for general LTL formulas, we show here that it does work for Safety LTL formulas, a popular and important fragment of LTL. While we have to compose all the programs of small conjuncts in the worst case, we can prune the intermediate programs to make later compositions easier and immediately conclude unrealizable as soon as some part of the specification is found unrealizable. By comparing our compositional approach with a portfolio of all other approaches, we observed that our approach was able to solve a notable number of instances not solved by others. In particular, experiments on scalable conjunctive benchmarks showed that our approach scale well and significantly outperform current Safety LTL synthesis techniques. We conclude that our compositional approach is an important contribution to the algorithmic portfolio of Safety LTL synthesis. 

Step-based tutoring consists in breaking down complicated problem-solving procedures into individual steps whose inputs can be immediately evaluated to promote effective student learning. Here, recent progress on the extension of a step-based tutoring for linear circuit analysis to cover new topics requiring complex, multi-step solution procedures is described. These topics include first and second-order transient problems solved using classical differential equation approaches. Students use an interactive circuit editor to modify the circuit appropriately for each step of the analysis, followed by writing and solving equations using methods of their choice as appropriate. Initial work on Laplace transform-based circuit analysis is also discussed. Detailed feedback is supplied at each step along with fully worked examples, supporting introductory multiple-choice tutorials and YouTube videos, and a full record of the student's work is created in a PDF document for later study and review. Further, results of a comprehensive independent evaluation involving both quantitative and qualitative analysis and users across four participating institutions are discussed. Overall, students had very favorable experiences using the step-based system across Fall 2020 and Spring 2021. At least 48% of students in the Fall 2020 semester and 60% of students in the Spring 2021 semester agreed or strongly agreed with all survey questions about positive features of the system. Those who had used the step-based system and the commercial MasteringEngineering system preferred the former by 69% to 12% margins in surveys. Instructors were further surveyed and 86% would recommend the system to others. 

Step-based tutoring consists in breaking down complicated problem-solving procedures into individual steps whose inputs can be immediately evaluated to promote effective student learning. Here, recent progress on the extension of a step-based tutoring for linear circuit analysis to cover new topics requiring complex, multi-step solution procedures is described. These topics include first and second-order transient problems solved using classical differential equation approaches. Students use an interactive circuit editor to modify the circuit appropriately for each step of the analysis, followed by writing and solving equations using methods of their choice as appropriate. Initial work on Laplace transform-based circuit analysis is also discussed. Detailed feedback is supplied at each step along with fully worked examples, supporting introductory multiple-choice tutorials and YouTube videos, and a full record of the student's work is created in a PDF document for later study and review. Further, results of a comprehensive independent evaluation involving both quantitative and qualitative analysis and users across four participating institutions are discussed. Overall, students had very favorable experiences using the step-based system across Fall 2020 and Spring 2021. At least 48% of students in the Fall 2020 semester and 60% of students in the Spring 2021 semester agreed or strongly agreed with all survey questions about positive features of the system. Those who had used the step-based system and the commercial MasteringEngineering system preferred the former by 69% to 12% margins in surveys. Instructors were further surveyed and 86% would recommend the system to others. 

In the Adapter-Design Pattern, a programmer implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. In this work, we presented a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an Adaptee and a Target transducers, and the aim is to synthesize an Adapter transducer that, when composed with the Adaptee, generates a behavior that is equivalent to the behavior of the Target. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduced a special form of specification format, called Separated GR(k), which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solved the realizability and the synthesis problems for Separated GR(k), and showed how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR(k) synthesis. We then described a tool, called SGR(k), which we have implemented based on the above approach and showed, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases. 

Step-based tutoring systems are known to be more effective than traditional answer-based systems. They however require that each step in a student’s work be accepted and evaluated automatically to provide effective feedback. In the domain of linear circuit analysis, it is frequently necessary to allow students to draw or edit circuits on their screen to simplify or otherwise transform them. Here, the interface developed to accept such input and provide immediate feedback in the Circuit Tutor system is described, along with systematic assessment data. Advanced simplification methods such as removing circuit sections that are removably hinged, voltage-splittable, or current-splittable are taught to students in an interactive tutorial and then supported in the circuit editor itself. To address the learning curve associated with such an interface, ~70 video tutorials were created to demonstrate exactly how to work the randomly generated problems at each level of each of the tutorials in the system. A complete written record or “transcript” of student’s work in the system is being made available, showing both incorrect and correct steps. Introductory interactive (multiple choice) tutorials are now included on most topics. Assessment of exercises using the interactive editor was carried out by professional evaluators for several institutions, including three that heavily serve underrepresented minorities. Both quantitative and qualitative methods were used, including focus groups, surveys, and interviews. Controlled, randomized, blind evaluations were carried out in three different course sections in Spring and Fall 2019 to evaluate three tutorials using the interactive editor, comparing use of Circuit Tutor to both a commercial answer-based system and to conventional textbook-based paper homework. In Fall 2019, students rated the software a mean of 4.14/5 for being helpful to learn the material vs. 3.05/5 for paper homework (HW), p < 0.001 and effect size d = 1.11σ. On relevant exam questions that semester, students scored significantly (p = 0.014) higher with an effect size of d = 0.64σ when using Circuit Tutor compared to paper HW in one class section, with no significant difference in the other section. 

We present a simple approach to improve direct speech-to-text translation (ST) when the source language is low-resource: we pre-train the model on a high-resource automatic speech recognition (ASR) task, and then fine-tune its parameters for ST. We demonstrate that our approach is effective by pre-training on 300 hours of English ASR data to improve SpanishEnglish ST from 10.8 to 20.2 BLEU when only 20 hours of Spanish-English ST training data are available. Through an ablation study, we find that the pre-trained encoder (acoustic model) accounts for most of the improvement, despite the fact that the shared language in these tasks is the target language text, not the source language audio. Applying this insight, we show that pre-training on ASR helps ST even when the ASR language differs from both source and target ST languages: pre-training on French ASR also improves Spanish-English ST. Finally, we show that the approach improves performance on a true low-resource task: pre-training on a combination of English ASR and French ASR improves Mboshi-French ST, where only 4 hours of data are available, from 3.5 to 7.1 BLEU. 

Step-based tutoring systems, in which each step of a student’s work is accepted by a computer using special interfaces and provided immediate feedback, are known to be more effective in promoting learning than traditional and more common answer-based tutoring systems, in which only the final (usually numerical) answer is evaluated. Prior work showed that this approach can be highly effective in the domain of linear circuit analysis in teaching topics involving relatively simple solution procedures. Here, we demonstrate a novel application of this approach to more cognitively complex, multi-step procedures used to analyze linear circuits using the superposition and source transformation methods. Both methods require that students interactively edit a circuit diagram repeatedly, interspersed with the writing of relevant equations. Scores on post-tests and student opinions are compared using a blind classroom-based experiment where students are randomly assigned to use either the new system or a commercially published answer-based tutoring system on these topics. Post-test scores are not statistically significantly different but students prefer the step-based system by a margin of 84 to 11% for superposition and 68 to 23% for source transformations.