-
Aya Dataset: An Open-Access Collection for Multilingual Instruction Tuning
Authors:
Shivalika Singh,
Freddie Vargus,
Daniel Dsouza,
Börje F. Karlsson,
Abinaya Mahendiran,
Wei-Yin Ko,
Herumb Shandilya,
Jay Patel,
Deividas Mataciunas,
Laura OMahony,
Mike Zhang,
Ramith Hettiarachchi,
Joseph Wilson,
Marina Machado,
Luisa Souza Moura,
Dominik Krzemiński,
Hakimeh Fadaei,
Irem Ergün,
Ifeoma Okoh,
Aisha Alaagib,
Oshan Mudannayake,
Zaid Alyafeai,
Vu Minh Chien,
Sebastian Ruder,
Surya Guthikonda
, et al. (8 additional authors not shown)
Abstract:
Datasets are foundational to many breakthroughs in modern artificial intelligence. Many recent achievements in the space of natural language processing (NLP) can be attributed to the finetuning of pre-trained models on a diverse set of tasks that enables a large language model (LLM) to respond to instructions. Instruction fine-tuning (IFT) requires specifically constructed and annotated datasets.…
▽ More
Datasets are foundational to many breakthroughs in modern artificial intelligence. Many recent achievements in the space of natural language processing (NLP) can be attributed to the finetuning of pre-trained models on a diverse set of tasks that enables a large language model (LLM) to respond to instructions. Instruction fine-tuning (IFT) requires specifically constructed and annotated datasets. However, existing datasets are almost all in the English language. In this work, our primary goal is to bridge the language gap by building a human-curated instruction-following dataset spanning 65 languages. We worked with fluent speakers of languages from around the world to collect natural instances of instructions and completions. Furthermore, we create the most extensive multilingual collection to date, comprising 513 million instances through templating and translating existing datasets across 114 languages. In total, we contribute four key resources: we develop and open-source the Aya Annotation Platform, the Aya Dataset, the Aya Collection, and the Aya Evaluation Suite. The Aya initiative also serves as a valuable case study in participatory research, involving collaborators from 119 countries. We see this as a valuable framework for future research collaborations that aim to bridge gaps in resources.
△ Less
Submitted 9 February, 2024;
originally announced February 2024.
-
A Formalized Extension of the Substitution Lemma in Coq
Authors:
Maria J. D. Lima,
Flávio L. C. de Moura
Abstract:
The substitution lemma is a renowned theorem within the realm of lambda-calculus theory and concerns the interactional behaviour of the metasubstitution operation. In this work, we augment the lambda-calculus's grammar with an uninterpreted explicit substitution operator, which allows the use of our framework for different calculi with explicit substitutions. Our primary contribution lies in verif…
▽ More
The substitution lemma is a renowned theorem within the realm of lambda-calculus theory and concerns the interactional behaviour of the metasubstitution operation. In this work, we augment the lambda-calculus's grammar with an uninterpreted explicit substitution operator, which allows the use of our framework for different calculi with explicit substitutions. Our primary contribution lies in verifying that, despite these modifications, the substitution lemma continues to remain valid. This confirmation was achieved using the Coq proof assistant. Our formalization methodology employs a nominal approach, which provides a direct implementation of the alpha-equivalence concept. The strategy involved in variable renaming within the proofs presents a challenge, specially on ensuring an exploration of the implications of our extension to the grammar of the lambda-calculus.
△ Less
Submitted 24 September, 2023;
originally announced September 2023.
-
Zero-shot performance of the Segment Anything Model (SAM) in 2D medical imaging: A comprehensive evaluation and practical guidelines
Authors:
Christian Mattjie,
Luis Vinicius de Moura,
Rafaela Cappelari Ravazio,
Lucas Silveira Kupssinskü,
Otávio Parraga,
Marcelo Mussi Delucis,
Rodrigo Coelho Barros
Abstract:
Segmentation in medical imaging is a critical component for the diagnosis, monitoring, and treatment of various diseases and medical conditions. Presently, the medical segmentation landscape is dominated by numerous specialized deep learning models, each fine-tuned for specific segmentation tasks and image modalities. The recently-introduced Segment Anything Model (SAM) employs the ViT neural arch…
▽ More
Segmentation in medical imaging is a critical component for the diagnosis, monitoring, and treatment of various diseases and medical conditions. Presently, the medical segmentation landscape is dominated by numerous specialized deep learning models, each fine-tuned for specific segmentation tasks and image modalities. The recently-introduced Segment Anything Model (SAM) employs the ViT neural architecture and harnesses a massive training dataset to segment nearly any object; however, its suitability to the medical domain has not yet been investigated. In this study, we explore the zero-shot performance of SAM in medical imaging by implementing eight distinct prompt strategies across six datasets from four imaging modalities, including X-ray, ultrasound, dermatoscopy, and colonoscopy. Our findings reveal that SAM's zero-shot performance is not only comparable to, but in certain cases, surpasses the current state-of-the-art. Based on these results, we propose practical guidelines that require minimal interaction while consistently yielding robust outcomes across all assessed contexts. The source code, along with a demonstration of the recommended guidelines, can be accessed at https://github.com/Malta-Lab/SAM-zero-shot-in-Medical-Imaging.
△ Less
Submitted 5 May, 2023; v1 submitted 28 April, 2023;
originally announced May 2023.
-
Debiasing Methods for Fairer Neural Models in Vision and Language Research: A Survey
Authors:
Otávio Parraga,
Martin D. More,
Christian M. Oliveira,
Nathan S. Gavenski,
Lucas S. Kupssinskü,
Adilson Medronha,
Luis V. Moura,
Gabriel S. Simões,
Rodrigo C. Barros
Abstract:
Despite being responsible for state-of-the-art results in several computer vision and natural language processing tasks, neural networks have faced harsh criticism due to some of their current shortcomings. One of them is that neural networks are correlation machines prone to model biases within the data instead of focusing on actual useful causal relationships. This problem is particularly seriou…
▽ More
Despite being responsible for state-of-the-art results in several computer vision and natural language processing tasks, neural networks have faced harsh criticism due to some of their current shortcomings. One of them is that neural networks are correlation machines prone to model biases within the data instead of focusing on actual useful causal relationships. This problem is particularly serious in application domains affected by aspects such as race, gender, and age. To prevent models from incurring on unfair decision-making, the AI community has concentrated efforts in correcting algorithmic biases, giving rise to the research area now widely known as fairness in AI. In this survey paper, we provide an in-depth overview of the main debiasing methods for fairness-aware neural networks in the context of vision and language research. We propose a novel taxonomy to better organize the literature on debiasing methods for fairness, and we discuss the current challenges, trends, and important future work directions for the interested researcher and practitioner.
△ Less
Submitted 10 November, 2022;
originally announced November 2022.
-
Bounds on Covering Codes in RT spaces using Ordered Covering Arrays
Authors:
André Guerino Castoldi,
Emerson Luiz do Monte Carmelo,
Lucia Moura,
Daniel Panario,
Brett Stevens
Abstract:
In this work, constructions of ordered covering arrays are discussed and applied to obtain new upper bounds on covering codes in Rosenbloom-Tsfasman spaces (RT spaces), improving or extending some previous results.
In this work, constructions of ordered covering arrays are discussed and applied to obtain new upper bounds on covering codes in Rosenbloom-Tsfasman spaces (RT spaces), improving or extending some previous results.
△ Less
Submitted 30 July, 2022;
originally announced August 2022.
-
Locating modifications in signed data for partial data integrity
Authors:
Thaís Bardini Idalino,
Lucia Moura,
Ricardo Felipe Custódio,
Daniel Panario
Abstract:
We consider the problem of detecting and locating modifications in signed data to ensure partial data integrity. We assume that the data is divided into $n$ blocks (not necessarily of the same size) and that a threshold $d$ is given for the maximum amount of modified blocks that the scheme can support. We propose efficient algorithms for signature and verification steps which provide a reasonably…
▽ More
We consider the problem of detecting and locating modifications in signed data to ensure partial data integrity. We assume that the data is divided into $n$ blocks (not necessarily of the same size) and that a threshold $d$ is given for the maximum amount of modified blocks that the scheme can support. We propose efficient algorithms for signature and verification steps which provide a reasonably compact signature size, for controlled sizes of $d$ with respect to $n$. For instance, for fixed $d$ the standard signature size gets multiplied by a factor of $O(\log n)$, while allowing the identification of up to $d$ modified blocks. Our scheme is based on nonadaptive combinatorial group testing and cover-free families.
△ Less
Submitted 31 July, 2022;
originally announced August 2022.
-
Ordered Covering Arrays and Upper Bounds on Covering Codes in NRT spaces
Authors:
André Guerino Castoldi,
Emerson L. Monte Carmelo,
Lucia Moura,
Daniel Panario,
Brett Stevens
Abstract:
This work shows several direct and recursive constructions of ordered covering arrays using projection, fusion, column augmentation, derivation, concatenation and cartesian product. Upper bounds on covering codes in NRT spaces are also obtained by improving a general upper bound. We explore the connection between ordered covering arrays and covering codes in NRT spaces, which generalize similar re…
▽ More
This work shows several direct and recursive constructions of ordered covering arrays using projection, fusion, column augmentation, derivation, concatenation and cartesian product. Upper bounds on covering codes in NRT spaces are also obtained by improving a general upper bound. We explore the connection between ordered covering arrays and covering codes in NRT spaces, which generalize similar results for the Hamming metric. Combining the new upper bounds for covering codes in NRT spaces and ordered covering arrays, we improve upper bounds on covering codes in NRT spaces for larger alphabets. We give tables comparing the new upper bounds for covering codes to existing ones.
△ Less
Submitted 31 July, 2022;
originally announced August 2022.
-
Modification tolerant signature schemes: location and correction
Authors:
Thais Bardini Idalino,
Lucia Moura,
Carlisle Adams
Abstract:
This paper considers malleable digital signatures, for situations where data is modified after it is signed. They can be used in applications where either the data can be modified (collaborative work), or the data must be modified (redactable and content extraction signatures) or we need to know which parts of the data have been modified (data forensics). A \new{classical} digital signature is val…
▽ More
This paper considers malleable digital signatures, for situations where data is modified after it is signed. They can be used in applications where either the data can be modified (collaborative work), or the data must be modified (redactable and content extraction signatures) or we need to know which parts of the data have been modified (data forensics). A \new{classical} digital signature is valid for a message only if the signature is authentic and not even one bit of the message has been modified. We propose a general framework of modification tolerant signature schemes (MTSS), which can provide either location only or both location and correction, for modifications in a signed message divided into $n$ blocks. This general scheme uses a set of allowed modifications that must be specified. We present an instantiation of MTSS with a tolerance level of $d$, indicating modifications can appear in any set of up to $d$ message blocks. This tolerance level $d$ is needed in practice for parametrizing and controlling the growth of the signature size with respect to the number $n$ of blocks; using combinatorial group testing (CGT) the signature has size $O(d^2 \log n)$ which is close to the \new{best known} lower bound \new{of $Ω(\frac{d^2}{\log d} (\log n))$}. There has been work in this very same direction using CGT by Goodrich et al. (ACNS 2005) and Idalino et al. (IPL 2015). Our work differs from theirs in that in one scheme we extend these ideas to include corrections of modification with provable security, and in another variation of the scheme we go in the opposite direction and guarantee privacy for redactable signatures, in this case preventing any leakage of redacted information.
△ Less
Submitted 31 July, 2022;
originally announced August 2022.
-
Nested Cover-Free Families for Unbounded Fault-Tolerant Aggregate Signatures
Authors:
Thais Bardini Idalino,
Lucia Moura
Abstract:
Aggregate signatures are used to create one short proof of authenticity and integrity from a set of digital signatures. However, one invalid signature in the set invalidates the entire aggregate, giving no information on which signatures are valid. Hartung et al. (2016) propose a fault-tolerant aggregate signature scheme based on combinatorial group testing. Given a bound $d$ on the number of inva…
▽ More
Aggregate signatures are used to create one short proof of authenticity and integrity from a set of digital signatures. However, one invalid signature in the set invalidates the entire aggregate, giving no information on which signatures are valid. Hartung et al. (2016) propose a fault-tolerant aggregate signature scheme based on combinatorial group testing. Given a bound $d$ on the number of invalid signatures among $n$ signatures to be aggregated, this scheme uses $d$-cover-free families to determine which signatures are invalid. These combinatorial structures guarantee a moderate increase on the size of the aggregate signature that can reach the best possible compression ratio of $O(\frac{n}{\log n})$, for fixed $d$, coming from an information theoretical bound. The case where the total number of signatures grows dynamically (unbounded scheme) was not satisfactorily solved in their original paper, since explicit constructions had constant compression ratios. In the present paper, we propose efficient solutions for the unbounded scheme, relying on sequences of $d$-cover-free families that we call {\em nested families}. Some of our constructions yield high compression ratio close to \rmv{the information theoretical bound}\todo{the best known upper bound}. We also propose the use of $(d,λ)$-cover-free families to support the loss of up to $λ-1$ parts of the aggregate.
△ Less
Submitted 31 July, 2022;
originally announced August 2022.
-
Ordered Orthogonal Array Construction Using LFSR Sequences
Authors:
André Guerino Castoldi,
Lucia Moura,
Daniel Panario,
Brett Stevens
Abstract:
We present a new construction of ordered orthogonal arrays (OOA) of strength $t$ with $(q + 1)t$ columns over a finite field $\mathbb{F}_{q}$ using linear feedback shift register sequences (LFSRs). OOAs are naturally related to $(t, m, s)$-nets, linear codes, and MDS codes. Our construction selects suitable columns from the array formed by all subintervals of length $\frac{q^{t}-1}{q-1}$ of an LFS…
▽ More
We present a new construction of ordered orthogonal arrays (OOA) of strength $t$ with $(q + 1)t$ columns over a finite field $\mathbb{F}_{q}$ using linear feedback shift register sequences (LFSRs). OOAs are naturally related to $(t, m, s)$-nets, linear codes, and MDS codes. Our construction selects suitable columns from the array formed by all subintervals of length $\frac{q^{t}-1}{q-1}$ of an LFSR sequence generated by a primitive polynomial of degree $t$ over $\mathbb{F}_{q}$. We prove properties about the relative positions of runs in an LFSR which guarantee that the constructed OOA has strength $t$. The set of parameters of our OOAs are the same as the ones given by Rosenbloom and Tsfasman (1997) and Skriganov (2002), but the constructed arrays are different. We experimentally verify that our OOAs are stronger than the Rosenbloom-Tsfasman-Skriganov OOAs in the sense that ours are "closer" to being a "full" orthogonal array. We also discuss how our OOA construction relates to previous techniques to build OOAs from a set of linearly independent vectors over $\mathbb{F}_{q}$, as well as to hypergraph homomorphisms.
△ Less
Submitted 30 July, 2022;
originally announced August 2022.
-
Structure-aware combinatorial group testing: a new method for pandemic screening
Authors:
Thais Bardini Idalino,
Lucia Moura
Abstract:
Combinatorial group testing (CGT) is used to identify defective items from a set of items by grouping them together and performing a small number of tests on the groups. Recently, group testing has been used to design efficient COVID-19 testing, so that resources are saved while still identifying all infected individuals. Due to test waiting times, a focus is given to non-adaptive CGT, where group…
▽ More
Combinatorial group testing (CGT) is used to identify defective items from a set of items by grouping them together and performing a small number of tests on the groups. Recently, group testing has been used to design efficient COVID-19 testing, so that resources are saved while still identifying all infected individuals. Due to test waiting times, a focus is given to non-adaptive CGT, where groups are designed a priori and all tests can be done in parallel. The design of the groups can be done using Cover-Free Families (CFFs). The main assumption behind CFFs is that a small number $d$ of positives are randomly spread across a population of $n$ individuals. However, for infectious diseases, it is reasonable to assume that infections show up in clusters of individuals with high contact (children in the same classroom within a school, households within a neighbourhood, students taking the same courses within a university, people seating close to each other in a stadium). The general structure of these communities can be modeled using hypergraphs, where vertices are items to be tested and edges represent clusters containing high contacts. We consider hypergraphs with non-overlapping edges and overlapping edges (first two examples and last two examples, respectively). We give constructions of what we call structure-aware CFF, which uses the structure of the underlying hypergraph. We revisit old CFF constructions, boosting the number of defectives they can identify by taking the hypergraph structure into account. We also provide new constructions based on hypergraph parameters.
△ Less
Submitted 16 February, 2022;
originally announced February 2022.
-
NeuraHealth: An Automated Screening Pipeline to Detect Undiagnosed Cognitive Impairment in Electronic Health Records with Deep Learning and Natural Language Processing
Authors:
Tanish Tyagi,
Colin G. Magdamo,
Ayush Noori,
Zhaozhi Li,
Xiao Liu,
Mayuresh Deodhar,
Zhuoqiao Hong,
Wendong Ge,
Elissa M. Ye,
Yi-han Sheu,
Haitham Alabsi,
Laura Brenner,
Gregory K. Robbins,
Sahar Zafar,
Nicole Benson,
Lidia Moura,
John Hsu,
Alberto Serrano-Pozo,
Dimitry Prokopenko,
Rudolph E. Tanzi,
Bradley T. Hyman,
Deborah Blacker,
Shibani S. Mukerji,
M. Brandon Westover,
Sudeshna Das
Abstract:
Dementia related cognitive impairment (CI) is a neurodegenerative disorder, affecting over 55 million people worldwide and growing rapidly at the rate of one new case every 3 seconds. 75% cases go undiagnosed globally with up to 90% in low-and-middle-income countries, leading to an estimated annual worldwide cost of USD 1.3 trillion, forecasted to reach 2.8 trillion by 2030. With no cure, a recurr…
▽ More
Dementia related cognitive impairment (CI) is a neurodegenerative disorder, affecting over 55 million people worldwide and growing rapidly at the rate of one new case every 3 seconds. 75% cases go undiagnosed globally with up to 90% in low-and-middle-income countries, leading to an estimated annual worldwide cost of USD 1.3 trillion, forecasted to reach 2.8 trillion by 2030. With no cure, a recurring failure of clinical trials, and a lack of early diagnosis, the mortality rate is 100%. Information in electronic health records (EHR) can provide vital clues for early detection of CI, but a manual review by experts is tedious and error prone. Several computational methods have been proposed, however, they lack an enhanced understanding of the linguistic context in complex language structures of EHR. Therefore, I propose a novel and more accurate framework, NeuraHealth, to identify patients who had no earlier diagnosis. In NeuraHealth, using patient EHR from Mass General Brigham BioBank, I fine-tuned a bi-directional attention-based deep learning natural language processing model to classify sequences. The sequence predictions were used to generate structured features as input for a patient level regularized logistic regression model. This two-step framework creates high dimensionality, outperforming all existing state-of-the-art computational methods as well as clinical methods. Further, I integrate the models into a real-world product, a web app, to create an automated EHR screening pipeline for scalable and high-speed discovery of undetected CI in EHR, making early diagnosis viable in medical facilities and in regions with scarce health services.
△ Less
Submitted 20 June, 2022; v1 submitted 12 January, 2022;
originally announced February 2022.
-
Using Deep Learning to Identify Patients with Cognitive Impairment in Electronic Health Records
Authors:
Tanish Tyagi,
Colin G. Magdamo,
Ayush Noori,
Zhaozhi Li,
Xiao Liu,
Mayuresh Deodhar,
Zhuoqiao Hong,
Wendong Ge,
Elissa M. Ye,
Yi-han Sheu,
Haitham Alabsi,
Laura Brenner,
Gregory K. Robbins,
Sahar Zafar,
Nicole Benson,
Lidia Moura,
John Hsu,
Alberto Serrano-Pozo,
Dimitry Prokopenko,
Rudolph E. Tanzi,
Bradley T. Hyman,
Deborah Blacker,
Shibani S. Mukerji,
M. Brandon Westover,
Sudeshna Das
Abstract:
Dementia is a neurodegenerative disorder that causes cognitive decline and affects more than 50 million people worldwide. Dementia is under-diagnosed by healthcare professionals - only one in four people who suffer from dementia are diagnosed. Even when a diagnosis is made, it may not be entered as a structured International Classification of Diseases (ICD) diagnosis code in a patient's charts. In…
▽ More
Dementia is a neurodegenerative disorder that causes cognitive decline and affects more than 50 million people worldwide. Dementia is under-diagnosed by healthcare professionals - only one in four people who suffer from dementia are diagnosed. Even when a diagnosis is made, it may not be entered as a structured International Classification of Diseases (ICD) diagnosis code in a patient's charts. Information relevant to cognitive impairment (CI) is often found within electronic health records (EHR), but manual review of clinician notes by experts is both time consuming and often prone to errors. Automated mining of these notes presents an opportunity to label patients with cognitive impairment in EHR data. We developed natural language processing (NLP) tools to identify patients with cognitive impairment and demonstrate that linguistic context enhances performance for the cognitive impairment classification task. We fine-tuned our attention based deep learning model, which can learn from complex language structures, and substantially improved accuracy (0.93) relative to a baseline NLP model (0.84). Further, we show that deep learning NLP can successfully identify dementia patients without dementia-related ICD codes or medications.
△ Less
Submitted 12 November, 2021;
originally announced November 2021.
-
Universal Policies for Software-Defined MDPs
Authors:
Daniel Selsam,
Jesse Michael Han,
Leonardo de Moura,
Patrice Godefroid
Abstract:
We introduce a new programming paradigm called oracle-guided decision programming in which a program specifies a Markov Decision Process (MDP) and the language provides a universal policy. We prototype a new programming language, Dodona, that manifests this paradigm using a primitive 'choose' representing nondeterministic choice. The Dodona interpreter returns either a value or a choicepoint that…
▽ More
We introduce a new programming paradigm called oracle-guided decision programming in which a program specifies a Markov Decision Process (MDP) and the language provides a universal policy. We prototype a new programming language, Dodona, that manifests this paradigm using a primitive 'choose' representing nondeterministic choice. The Dodona interpreter returns either a value or a choicepoint that includes a lossless encoding of all information necessary in principle to make an optimal decision. Meta-interpreters query Dodona's (neural) oracle on these choicepoints to get policy and value estimates, which they can use to perform heuristic search on the underlying MDP. We demonstrate Dodona's potential for zero-shot heuristic guidance by meta-learning over hundreds of synthetic tasks that simulate basic operations over lists, trees, Church datastructures, polynomials, first-order terms and higher-order terms.
△ Less
Submitted 21 December, 2020;
originally announced December 2020.
-
Natural Language Processing to Detect Cognitive Concerns in Electronic Health Records Using Deep Learning
Authors:
Zhuoqiao Hong,
Colin G. Magdamo,
Yi-han Sheu,
Prathamesh Mohite,
Ayush Noori,
Elissa M. Ye,
Wendong Ge,
Haoqi Sun,
Laura Brenner,
Gregory Robbins,
Shibani Mukerji,
Sahar Zafar,
Nicole Benson,
Lidia Moura,
John Hsu,
Bradley T. Hyman,
Michael B. Westover,
Deborah Blacker,
Sudeshna Das
Abstract:
Dementia is under-recognized in the community, under-diagnosed by healthcare professionals, and under-coded in claims data. Information on cognitive dysfunction, however, is often found in unstructured clinician notes within medical records but manual review by experts is time consuming and often prone to errors. Automated mining of these notes presents a potential opportunity to label patients wi…
▽ More
Dementia is under-recognized in the community, under-diagnosed by healthcare professionals, and under-coded in claims data. Information on cognitive dysfunction, however, is often found in unstructured clinician notes within medical records but manual review by experts is time consuming and often prone to errors. Automated mining of these notes presents a potential opportunity to label patients with cognitive concerns who could benefit from an evaluation or be referred to specialist care. In order to identify patients with cognitive concerns in electronic medical records, we applied natural language processing (NLP) algorithms and compared model performance to a baseline model that used structured diagnosis codes and medication data only. An attention-based deep learning model outperformed the baseline model and other simpler models.
△ Less
Submitted 12 November, 2020;
originally announced November 2020.
-
Sealing Pointer-Based Optimizations Behind Pure Functions
Authors:
Daniel Selsam,
Simon Hudon,
Leonardo de Moura
Abstract:
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing pure functional programming languages all su…
▽ More
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing pure functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.
△ Less
Submitted 30 May, 2020; v1 submitted 3 March, 2020;
originally announced March 2020.
-
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Authors:
Sebastian Ullrich,
Leonardo de Moura
Abstract:
In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries. Most ITPs support such extensions in the form of restrictive "syntax sugar" substitutions and other ad hoc mechanisms, which are too rudimentary to support many desirable…
▽ More
In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries. Most ITPs support such extensions in the form of restrictive "syntax sugar" substitutions and other ad hoc mechanisms, which are too rudimentary to support many desirable abstractions. As a result, libraries are littered with unnecessary redundancy. Tactic languages in these systems are plagued by a seemingly unrelated issue: accidental name capture, which often produces unexpected and counterintuitive behavior. We take ideas from the Scheme family of programming languages and solve these two problems simultaneously by proposing a novel hygienic macro system custom-built for ITPs. We further describe how our approach can be extended to cover type-directed macro expansion resulting in a single, uniform system offering multiple abstraction levels that range from supporting simplest syntax sugars to elaboration of formerly baked-in syntax. We have implemented our new macro system and integrated it into the new version of the Lean theorem prover, Lean 4. Despite its expressivity, the macro system is simple enough that it can easily be integrated into other systems.
△ Less
Submitted 12 April, 2022; v1 submitted 28 January, 2020;
originally announced January 2020.
-
Tabled Typeclass Resolution
Authors:
Daniel Selsam,
Sebastian Ullrich,
Leonardo de Moura
Abstract:
Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean's burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impedi…
▽ More
Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean's burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impediments to ongoing progress. The two most devastating limitations of existing procedures are exponential running times in the presence of diamonds and divergence in the presence of cycles. We present a new procedure, tabled typeclass resolution, that solves both problems by tabling, which is a generalization of memoizing originally introduced to address similar limitations of early logic programming systems. We have implemented our procedure for the upcoming version (v4) of Lean, and have confirmed empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Although tabling is notoriously difficult to implement, our procedure is notably lightweight and could easily be implemented in other systems. We hope our new procedure facilitates even more sophisticated uses of typeclasses in both software development and interactive theorem proving.
△ Less
Submitted 21 January, 2020; v1 submitted 13 January, 2020;
originally announced January 2020.
-
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Authors:
Sebastian Ullrich,
Leonardo de Moura
Abstract:
Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. On the other hand, having an exact reference count of each value can enable optimizations, such as destructive updates. We explore these optimization opportunities in the context of…
▽ More
Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. On the other hand, having an exact reference count of each value can enable optimizations, such as destructive updates. We explore these optimization opportunities in the context of an eager, purely functional programming language. We propose a new mechanism for efficiently reclaiming memory used by nonshared values, reducing stress on the global memory allocator. We describe an approach for minimizing the number of reference counts updates using borrowed references and a heuristic for automatically inferring borrow annotations. We implemented all these techniques in a new compiler for an eager and purely functional programming language with support for multi-threading. Our preliminary experimental results demonstrate our approach is competitive and often outperforms state-of-the-art compilers.
△ Less
Submitted 5 March, 2020; v1 submitted 15 August, 2019;
originally announced August 2019.
-
Learning a SAT Solver from Single-Bit Supervision
Authors:
Daniel Selsam,
Matthew Lamm,
Benedikt Bünz,
Percy Liang,
Leonardo de Moura,
David L. Dill
Abstract:
We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalize…
▽ More
We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.
△ Less
Submitted 11 March, 2019; v1 submitted 10 February, 2018;
originally announced February 2018.
-
Congruence Closure in Intensional Type Theory
Authors:
Daniel Selsam,
Leonardo de Moura
Abstract:
Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT), which form the basis of many interactive theorem provers. The main source of expressiveness in these logics is dependent typ…
▽ More
Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence closure algorithms can support any of the expressive logics based on intensional type theory (ITT), which form the basis of many interactive theorem provers. The main source of expressiveness in these logics is dependent types, and yet existing congruence closure procedures found in interactive theorem provers based on ITT do not handle dependent types at all and only work on the simply-typed subsets of the logics. Here we present an efficient and proof-producing congruence closure procedure that applies to every function in ITT no matter how many dependencies exist among its arguments, and that only relies on the commonly assumed uniqueness of identity proofs axiom. We demonstrate its usefulness by solving interesting verification problems involving functions with dependent types.
△ Less
Submitted 9 May, 2017; v1 submitted 16 January, 2017;
originally announced January 2017.
-
Elaboration in Dependent Type Theory
Authors:
Leonardo de Moura,
Jeremy Avigad,
Soonho Kong,
Cody Roux
Abstract:
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a co…
▽ More
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean's elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved.
△ Less
Submitted 17 December, 2015; v1 submitted 16 May, 2015;
originally announced May 2015.
-
A Formalization of the Theorem of Existence of First-Order Most General Unifiers
Authors:
Andréia B Avelar,
André L Galdino,
Flávio LC de Moura,
Mauricio Ayala-Rincón
Abstract:
This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the textbook proofs that are based on proving the correctness of the well-known Robinson's first-order unification algorithm. The formalization was applied inside…
▽ More
This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the textbook proofs that are based on proving the correctness of the well-known Robinson's first-order unification algorithm. The formalization was applied inside a PVS development for term rewriting systems that provides a complete formalization of the Knuth-Bendix Critical Pair theorem, among other relevant theorems of the theory of rewriting. In addition, the formalization methodology has been proved of practical use in order to verify the correctness of unification algorithms in the style of the original Robinson's unification algorithm.
△ Less
Submitted 28 March, 2012;
originally announced March 2012.
