An official website of the United States government
Many data extraction tasks of practical relevance require not only syntactic pattern matching but also semantic reasoning about the content of the underlying text. While regular expressions are very well suited for tasks that require only syntactic pattern matching, they fall short for data extraction tasks that involve both a syntactic and semantic component. To address this issue, we introduce semantic regexes, a generalization of regular expressions that facilitates combined syntactic and semantic reasoning about textual data. We also propose a novel learning algorithm that can synthesize semantic regexes from a small number of positive and negative examples. Our proposed learning algorithm uses a combination of neural sketch generation and compositional type-directed synthesis for fast and effective generalization from a small number of examples. We have implemented these ideas in a new tool called Smore and evaluated it on representative data extraction tasks involving several textual datasets. Our evaluation shows that semantic regexes can better support complex data extraction tasks than standard regular expressions and that our learning algorithm significantly outperforms existing tools, including state-of-the-art neural networks and program synthesis tools.
more »
« less
Syntactic Reasoning and Cognitive Load in Algebra
In the context of proofs, researchers have distinguished between syntactic reasoning and semantic reasoning; however, this distinction has not been well-explored in areas of mathematics education below formal proof, where student reasoning and justification are also important. In this paper we draw on theories of cognitive load and syntactic versus semantic proof-production to explicate a definition for syntactic reasoning outside the context of formal proof, using illustrative examples from algebra.
more »
« less
- Award ID(s):
- 1760491
- PAR ID:
- 10481793
- Editor(s):
- Cook, S.; Infante, N.
- Publisher / Repository:
- Proceedings for the 25th Annual Conference on Research in Undergraduate Mathematics Education, RUME, http://sigmaa.maa.org/rume/Site/Proceedings.html
- Date Published:
- Journal Name:
- Proceedings for the 25th Annual Conference on Research in Undergraduate Mathematics Education, RUME, http://sigmaa.maa.org/rume/Site/Proceedings.html
- Volume:
- 25
- Subject(s) / Keyword(s):
- Syntactic reasoning Semantic reasoning Cognitive load Algebra
- Format(s):
- Medium: X
- Location:
- Omaha, Nebraska, USA
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Rigorous, mathematical reasoning, i.e., proof, is the foundation of any undergraduate computer science education. However, students find mathematical proof exceedingly challenging, but also at the same time do not see its relevance to programming. We address these concerns with Snowflake, an educational proof assistant designed to help undergraduates overcome these difficulties when authoring mathematical proof. Snowflake does this by operating in a context where mathematical proof is introduced alongside programming in either a CS1 or CS2 context. The lens that we use to unite the two concepts is program correctness, a topic that immediately makes relevant the concept of formal reasoning as students are perpetually faced with the issue of whether their code is correct. Snowflake is a proof assistant designed for the needs of undergraduates in courses that closely time programming and proof. It is a web-based application that helps students author proofs not only in the context of program correctness in-the-small, but also other topics found in discrete mathematics courses. We report on the design of Snowflake, the kinds of reasoning it enables, and our plans to deploy Snowflake in the classroom.more » « less
-
MLM has attracted much attention over the last two decades. MLM activities include philosophical discussions about ontologies, requirements and relevant services, and development of theories, languages, and tools. Approaches differ in their support for MLM concepts on the levels of syntax, semantics and pragmatics. The Mediation-based MLM (MedMLM), is a formal theory that defines a multilevel model as an ordered collection of levels that are inter-related by mediators, and can be enriched by inter-level relationships and interactions. The levels of MedMLM are plain class models, and the mediators define inter-level instantiation relations. MedMLM is unique in supporting a modular architecture of levels and mediators. This paper introduces the MedMLM software modeling tool, that is built on top of the FOModeLer class modeling tool. The tool supports MLM construction, querying and reasoning, meta-reasoning, validation, syntax verification, and plain computation. We also compare the MedMLM tool with older MLM approaches using semantic, syntactic, and pragmatic MLM criteria.more » « less
-
Semantic relationships, such as hyponym–hypernym, cause–effect, meronym–holonym etc., between a pair of entities in a sentence are usually reflected through syntactic patterns. Automatic extraction of such patterns benefits several downstream tasks, including, entity extraction, ontology building, and question answering. Unfortunately, automatic extraction of such patterns has not yet received much attention from NLP and information retrieval researchers. In this work, we propose an attention-based supervised deep learning model, ASPER, which extracts syntactic patterns between entities exhibiting a given semantic relation in the sentential context. We validate the performance of ASPER on three distinct semantic relations—hyponym–hypernym, cause–effect, and meronym–holonym on six datasets. Experimental results show that for all these semantic relations, ASPER can automatically identify a collection of syntactic patterns reflecting the existence of such a relation between a pair of entities in a sentence. In comparison to the existing methodologies of syntactic pattern extraction, ASPER’s performance is substantially superior.more » « less
-
Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique oftransactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers oninteraction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
