-
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.
-
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.
-
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.
