Showing 1–15 of 15 results for author: Murphy, L

Autoformalizing Euclidean Geometry

Authors: Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si

Abstract: Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs)… ▽ More Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs). One challenge in Euclidean geometry is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. To address this issue, we use theorem provers to fill in such diagrammatic information automatically, so that the LLM only needs to autoformalize the explicit textual steps, making it easier for the model. We also provide automatic semantic evaluation for autoformalized theorem statements. We construct LeanEuclid, an autoformalization benchmark consisting of problems from Euclid's Elements and the UniGeo dataset formalized in the Lean proof assistant. Experiments with GPT-4 and GPT-4V show the capability and limitations of state-of-the-art LLMs on autoformalizing geometry problems. The data and code are available at https://github.com/loganrjmurphy/LeanEuclid. △ Less

Submitted 27 May, 2024; originally announced May 2024.

Comments: Accepted to ICML 2024. The first two authors contributed equally

A Survey on Deep Learning for Theorem Proving

Authors: Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si

Abstract: Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in mathematical language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a pioneerin… ▽ More Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in mathematical language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a pioneering comprehensive survey of deep learning for theorem proving by offering i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; ii) a meticulous summary of available datasets and strategies for data generation; iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art; and iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, seeking to catalyze further research endeavors in this rapidly growing field. △ Less

Submitted 15 April, 2024; originally announced April 2024.

MILP for the Multi-objective VM Reassignment Problem

Authors: Takfarinas Saber, Anthony Ventresque, Joao Marques-Silva, James Thorburn, Liam Murphy

Abstract: Machine Reassignment is a challenging problem for constraint programming (CP) and mixed-integer linear programming (MILP) approaches, especially given the size of data centres. The multi-objective version of the Machine Reassignment Problem is even more challenging and it seems unlikely for CP or MILP to obtain good results in this context. As a result, the first approaches to address this problem… ▽ More Machine Reassignment is a challenging problem for constraint programming (CP) and mixed-integer linear programming (MILP) approaches, especially given the size of data centres. The multi-objective version of the Machine Reassignment Problem is even more challenging and it seems unlikely for CP or MILP to obtain good results in this context. As a result, the first approaches to address this problem have been based on other optimisation methods, including metaheuristics. In this paper we study under which conditions a mixed-integer optimisation solver, such as IBM ILOG CPLEX, can be used for the Multi-objective Machine Reassignment Problem. We show that it is useful only for small or medium-scale data centres and with some relaxations, such as an optimality tolerance gap and a limited number of directions explored in the search space. Building on this study, we also investigate a hybrid approach, feeding a metaheuristic with the results of CPLEX, and we show that the gains are important in terms of quality of the set of Pareto solutions (+126.9% against the metaheuristic alone and +17.8% against CPLEX alone) and number of solutions (8.9 times more than CPLEX), while the processing time increases only by 6% in comparison to CPLEX for execution times larger than 100 seconds. △ Less

Submitted 18 March, 2021; originally announced March 2021.

The Wireless Control Bus: Enabling Efficient Multi-hop Event-Triggered Control with Concurrent Transmissions

Authors: Matteo Trobinger, Gabriel de Albuquerque Gleizer, Timofei Istomin, Manuel Mazo Jr., Amy L. Murphy, Gian Pietro Picco

Abstract: Event-triggered control (ETC) holds the potential to significantly improve the efficiency of wireless networked control systems. Unfortunately, its real-world impact has hitherto been hampered by the lack of a network stack able to transfer its benefits from theory to practice specifically by supporting the latency and reliability requirements of the aperiodic communication ETC induces. This is pr… ▽ More Event-triggered control (ETC) holds the potential to significantly improve the efficiency of wireless networked control systems. Unfortunately, its real-world impact has hitherto been hampered by the lack of a network stack able to transfer its benefits from theory to practice specifically by supporting the latency and reliability requirements of the aperiodic communication ETC induces. This is precisely the contribution of this paper. Our Wireless Control Bus (WCB) exploits carefully orchestrated network-wide floods of concurrent transmissions to minimize overhead during quiescent, steady-state periods, and ensures timely and reliable collection of sensor readings and dissemination of actuation commands when an ETC triggering condition is violated. Using a cyber-physical testbed emulating a water distribution system controlled over a real-world multi-hop wireless network, we show that ETC over WCB achieves the same quality of periodic control at a fraction of the energy costs, therefore unleashing and concretely demonstrating its full potential for the first time. △ Less

Submitted 17 October, 2021; v1 submitted 26 January, 2021; originally announced January 2021.

Comments: To appear in ACM Transactions on Cyber-Physical Systems (TCPS), 28 pages

Janus: Efficient and Accurate Dual-radio Social Contact Detection

Authors: Timofei Istomin, Elia Leoni, Davide Molteni, Amy L. Murphy, Gian Pietro Picco, Maurizio Griva

Abstract: Determining when two individuals are within close distance is key to contain a pandemic, e.g., to alert individuals in real-time and trace their social contacts. Common approaches rely on either Bluetooth Low Energy (BLE) or ultra-wideband (UWB) radios, that nonetheless strike opposite tradeoffs for energy efficiency vs. accuracy of distance estimates. Janus reconciles these dimensions with a du… ▽ More Determining when two individuals are within close distance is key to contain a pandemic, e.g., to alert individuals in real-time and trace their social contacts. Common approaches rely on either Bluetooth Low Energy (BLE) or ultra-wideband (UWB) radios, that nonetheless strike opposite tradeoffs for energy efficiency vs. accuracy of distance estimates. Janus reconciles these dimensions with a dual-radio protocol enabling efficient and accurate social contact detection. Measurements show that Janus achieves weeks to months of autonomous operation, depending on the configuration. Several large-scale campaigns in real-world contexts confirm its reliability and practical usefulness in enabling insightful analysis of contact data. △ Less

Submitted 1 May, 2021; v1 submitted 5 January, 2021; originally announced January 2021.

Word meaning in minds and machines

Authors: Brenden M. Lake, Gregory L. Murphy

Abstract: Machines have achieved a broad and growing set of linguistic competencies, thanks to recent progress in Natural Language Processing (NLP). Psychologists have shown increasing interest in such models, comparing their output to psychological judgments such as similarity, association, priming, and comprehension, raising the question of whether the models could serve as psychological theories. In this… ▽ More Machines have achieved a broad and growing set of linguistic competencies, thanks to recent progress in Natural Language Processing (NLP). Psychologists have shown increasing interest in such models, comparing their output to psychological judgments such as similarity, association, priming, and comprehension, raising the question of whether the models could serve as psychological theories. In this article, we compare how humans and machines represent the meaning of words. We argue that contemporary NLP systems are fairly successful models of human word similarity, but they fall short in many other respects. Current models are too strongly linked to the text-based patterns in large corpora, and too weakly linked to the desires, goals, and beliefs that people express through words. Word meanings must also be grounded in perception and action and be capable of flexible combinations in ways that current systems are not. We discuss more promising approaches to grounding NLP systems and argue that they will be more successful with a more human-like, conceptual basis for word meaning. △ Less

Submitted 17 April, 2021; v1 submitted 4 August, 2020; originally announced August 2020.

Comments: In press at Psychological Review

Relational Pooling for Graph Representations

Authors: Ryan L. Murphy, Balasubramaniam Srinivasan, Vinayak Rao, Bruno Ribeiro

Abstract: This work generalizes graph neural networks (GNNs) beyond those based on the Weisfeiler-Lehman (WL) algorithm, graph Laplacians, and diffusions. Our approach, denoted Relational Pooling (RP), draws from the theory of finite partial exchangeability to provide a framework with maximal representation power for graphs. RP can work with existing graph representation models and, somewhat counterintuitiv… ▽ More This work generalizes graph neural networks (GNNs) beyond those based on the Weisfeiler-Lehman (WL) algorithm, graph Laplacians, and diffusions. Our approach, denoted Relational Pooling (RP), draws from the theory of finite partial exchangeability to provide a framework with maximal representation power for graphs. RP can work with existing graph representation models and, somewhat counterintuitively, can make them even more powerful than the original WL isomorphism test. Additionally, RP allows architectures like Recurrent Neural Networks and Convolutional Neural Networks to be used in a theoretically sound approach for graph classification. We demonstrate improved performance of RP-based graph representations over state-of-the-art methods on a number of tasks. △ Less

Submitted 14 May, 2019; v1 submitted 6 March, 2019; originally announced March 2019.

Comments: ICML 2019 Camera-Ready. Added to molecular experiments and balanced the classes of the validation folds for the synthetic-graph experiments. Clarified some discussions

WURBench: Toward Benchmarking Wake-up Radio-based Systems

Authors: Rajeev Piyare, Amy L. Murphy

Abstract: The performance of wake-up radios must be clearly measured and understood while designing and develo** robust, dependable, and affordable systems, considering both benefits and shortcomings. State-of-the-art WURs display significant diversity in their architecture, processing capability, energy consumption, and receiver sensitivity. Standard methodologies for benchmarking are crucial for quantit… ▽ More The performance of wake-up radios must be clearly measured and understood while designing and develo** robust, dependable, and affordable systems, considering both benefits and shortcomings. State-of-the-art WURs display significant diversity in their architecture, processing capability, energy consumption, and receiver sensitivity. Standard methodologies for benchmarking are crucial for quantitatively evaluating the performance of this emerging technology, however, currently, no accepted standard for such quantitative measurement exists. Further, there is no consensus on what objective evaluation procedures and metrics should be used to understand the performance of whole systems exploiting this technology. This lack of standardization has prevented researchers from comparing results and leveraging previous work that could otherwise avoid duplication and speed up the validation process. This paper leads toward an evaluation framework, a benchmark, to enable accurate and repeatable profiling of WUR-based systems, leading to more consistent and therefore comparable evaluations for current and future systems. △ Less

Submitted 16 November, 2018; originally announced November 2018.

Comments: 4 pages, position paper

Janossy Pooling: Learning Deep Permutation-Invariant Functions for Variable-Size Inputs

Authors: Ryan L. Murphy, Balasubramaniam Srinivasan, Vinayak Rao, Bruno Ribeiro

Abstract: We consider a simple and overarching representation for permutation-invariant functions of sequences (or multiset functions). Our approach, which we call Janossy pooling, expresses a permutation-invariant function as the average of a permutation-sensitive function applied to all reorderings of the input sequence. This allows us to leverage the rich and mature literature on permutation-sensitive fu… ▽ More We consider a simple and overarching representation for permutation-invariant functions of sequences (or multiset functions). Our approach, which we call Janossy pooling, expresses a permutation-invariant function as the average of a permutation-sensitive function applied to all reorderings of the input sequence. This allows us to leverage the rich and mature literature on permutation-sensitive functions to construct novel and flexible permutation-invariant functions. If carried out naively, Janossy pooling can be computationally prohibitive. To allow computational tractability, we consider three kinds of approximations: canonical orderings of sequences, functions with $k$-order interactions, and stochastic optimization algorithms with random permutations. Our framework unifies a variety of existing work in the literature, and suggests possible modeling and algorithmic extensions. We explore a few in our experiments, which demonstrate improved performance over current state-of-the-art methods. △ Less

Submitted 25 February, 2019; v1 submitted 5 November, 2018; originally announced November 2018.

Comments: This version clarifies and adds detail to some of the arguments

Journal ref: ICLR 2019

KRATOS: An Open Source Hardware-Software Platform for Rapid Research in LPWANs

Authors: Rajeev Piyare, Amy L. Murphy, Michele Magno, Luca Benini

Abstract: Long-range (LoRa) radio technologies have recently gained momentum in the IoT landscape, allowing low-power communications over distances up to several kilometers. As a result, more and more LoRa networks are being deployed. However, commercially available LoRa devices are expensive and propriety, creating a barrier to entry and possibly slowing down developments and deployments of novel applicati… ▽ More Long-range (LoRa) radio technologies have recently gained momentum in the IoT landscape, allowing low-power communications over distances up to several kilometers. As a result, more and more LoRa networks are being deployed. However, commercially available LoRa devices are expensive and propriety, creating a barrier to entry and possibly slowing down developments and deployments of novel applications. Using open-source hardware and software platforms would allow more developers to test and build intelligent devices resulting in a better overall development ecosystem, lower barriers to entry, and rapid growth in the number of IoT applications. Toward this goal, this paper presents the design, implementation, and evaluation of KRATOS, a low-cost LoRa platform running ContikiOS. Both, our hardware and software designs are released as an open- source to the research community. △ Less

Submitted 11 September, 2018; originally announced September 2018.

Comments: Accepted at WiMob 2018

On-Demand TDMA for Energy Efficient Data Collection with LoRa and Wake-up Receiver

Authors: Rajeev Piyare, Amy L. Murphy, Michele Magno, Luca Benini

Abstract: Low-power and long-range communication tech- nologies such as LoRa are becoming popular in IoT applications due to their ability to cover kilometers range with milliwatt of power consumption. One of the major drawbacks of LoRa is the data latency and the traffic congestion when the number of devices in the network increases. Especially, the latency arises due to the extreme duty cycling of LoRa en… ▽ More Low-power and long-range communication tech- nologies such as LoRa are becoming popular in IoT applications due to their ability to cover kilometers range with milliwatt of power consumption. One of the major drawbacks of LoRa is the data latency and the traffic congestion when the number of devices in the network increases. Especially, the latency arises due to the extreme duty cycling of LoRa end-nodes for reducing the overall energy consumption. To overcome this drawback, we propose a heterogeneous network architecture and an energy-efficient On-demand TDMA communication scheme improving both the device lifetime and the data latency of standard LoRa networks. We combine the capabilities of micro- watt wake-up receivers to achieve ultra-low power states and pure asynchronous communication together with the long-range connectivity of LoRa. Experimental results show a data reliability of 100% and a round-trip latency on the order of milliseconds with end devices dissipating less than 46 mJ when active and 1.83 μW during periods of inactivity, lasting up to 3 years on a 1200 mAh Lithium battery. △ Less

Submitted 11 September, 2018; originally announced September 2018.

Comments: Accepted at WiMob 2018

Using Social Media to Promote STEM Education: Matching College Students with Role Models

Authors: Ling He, Lee Murphy, Jiebo Luo

Abstract: STEM (Science, Technology, Engineering, and Mathematics) fields have become increasingly central to U.S. economic competitiveness and growth. The shortage in the STEM workforce has brought promoting STEM education upfront. The rapid growth of social media usage provides a unique opportunity to predict users' real-life identities and interests from online texts and photos. In this paper, we propose… ▽ More STEM (Science, Technology, Engineering, and Mathematics) fields have become increasingly central to U.S. economic competitiveness and growth. The shortage in the STEM workforce has brought promoting STEM education upfront. The rapid growth of social media usage provides a unique opportunity to predict users' real-life identities and interests from online texts and photos. In this paper, we propose an innovative approach by leveraging social media to promote STEM education: matching Twitter college student users with diverse LinkedIn STEM professionals using a ranking algorithm based on the similarities of their demographics and interests. We share the belief that increasing STEM presence in the form of introducing career role models who share similar interests and demographics will inspire students to develop interests in STEM related fields and emulate their models. Our evaluation on 2,000 real college students demonstrated the accuracy of our ranking algorithm. We also design a novel implementation that recommends matched role models to the students. △ Less

Submitted 1 July, 2016; originally announced July 2016.

Comments: 16 pages, 8 figures, accepted by ECML/PKDD 2016, Industrial Track

A Two-Prong Approach to Energy-Efficient WSNs: Wake-Up Receivers plus Dedicated, Model-Based Sensing

Authors: Usman Raza, Alessandro Bogliolo, Valerio Freschi, Emanuele Lattanzi, Amy L. Murphy

Abstract: Energy neutral operation of WSNs can be achieved by exploiting the idleness of the workload to bring the average power consumption of each node below the harvesting power available. This paper proposes a combination of state-of-the-art low-power design techniques to minimize the local and global impact of the two main activities of each node: sampling and communication. Dynamic power management is… ▽ More Energy neutral operation of WSNs can be achieved by exploiting the idleness of the workload to bring the average power consumption of each node below the harvesting power available. This paper proposes a combination of state-of-the-art low-power design techniques to minimize the local and global impact of the two main activities of each node: sampling and communication. Dynamic power management is adopted to exploit low-power modes during idle periods, while asynchronous wake-up and prediction-based data collection are used to opportunistically activate hardware components and network nodes only when they are strictly required. Furthermore, the concept of "model-based sensing" is introduced to push prediction-based data collection techniques as close as possible to the sensing elements. The results achieved on representative real-world WSN case studies show that the combined benefits of the design techniques adopted is more than linear, providing an overall power reduction of more than 3 orders of magnitude. △ Less

Submitted 18 March, 2016; v1 submitted 25 January, 2016; originally announced January 2016.

Comments: 30 pages, 7 figures, 5 tables

Ontology-Based Quality Evaluation of Value Generalization Hierarchies for Data Anonymization

Authors: Vanessa Ayala-Rivera, Patrick McDonagh, Thomas Cerqueus, Liam Murphy

Abstract: In privacy-preserving data publishing, approaches using Value Generalization Hierarchies (VGHs) form an important class of anonymization algorithms. VGHs play a key role in the utility of published datasets as they dictate how the anonymization of the data occurs. For categorical attributes, it is imperative to preserve the semantics of the original data in order to achieve a higher utility. Despi… ▽ More In privacy-preserving data publishing, approaches using Value Generalization Hierarchies (VGHs) form an important class of anonymization algorithms. VGHs play a key role in the utility of published datasets as they dictate how the anonymization of the data occurs. For categorical attributes, it is imperative to preserve the semantics of the original data in order to achieve a higher utility. Despite this, semantics have not being formally considered in the specification of VGHs. Moreover, there are no methods that allow the users to assess the quality of their VGH. In this paper, we propose a measurement scheme, based on ontologies, to quantitatively evaluate the quality of VGHs, in terms of semantic consistency and taxonomic organization, with the aim of producing higher-quality anonymizations. We demonstrate, through a case study, how our evaluation scheme can be used to compare the quality of multiple VGHs and can help to identify faulty VGHs. △ Less

Submitted 5 March, 2015; originally announced March 2015.

Comments: 18 pages, 7 figures, presented in the Privacy in Statistical Databases Conference 2014 (Ibiza, Spain)

ACM Class: H.2.0; D.2.0

Synthetic Data Generation using Benerator Tool

Authors: Vanessa Ayala-Rivera, Patrick McDonagh, Thomas Cerqueus, Liam Murphy

Abstract: Datasets of different characteristics are needed by the research community for experimental purposes. However, real data may be difficult to obtain due to privacy concerns. Moreover, real data may not meet specific characteristics which are needed to verify new approaches under certain conditions. Given these limitations, the use of synthetic data is a viable alternative to complement the real dat… ▽ More Datasets of different characteristics are needed by the research community for experimental purposes. However, real data may be difficult to obtain due to privacy concerns. Moreover, real data may not meet specific characteristics which are needed to verify new approaches under certain conditions. Given these limitations, the use of synthetic data is a viable alternative to complement the real data. In this report, we describe the process followed to generate synthetic data using Benerator, a publicly available tool. The results show that the synthetic data preserves a high level of accuracy compared to the original data. The generated datasets correspond to microdata containing records with social, economic and demographic data which mimics the distribution of aggregated statistics from the 2011 Irish Census data. △ Less

Submitted 13 November, 2013; originally announced November 2013.

Comments: 12 pages, 5 figures, 10 references

Report number: UCD-CSI-2013-03 MSC Class: 68-XX (Primary) ACM Class: H.2.7; K.4.1