Concept

Automated reasoning

Related publications (27)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024

REFINER: Reasoning Feedback on Intermediate Representations

Boi Faltings, Robert West, Antoine Bosselut, Maxime Jean Julien Peyrard, Debjit Paul, Mahammad Ismayilzada, Beatriz Maria Borges Ribeiro

Language models (LMs) have recently shown remarkable performance on reasoning tasks by explicitly generating intermediate inferences, e.g., chain-of-thought prompting. However, these intermediate inference steps may be in- appropriate deductions from the i ...

2023

Monotonicity Reasoning in the Age of Neural Foundation Models

Zeming Chen

The recent advance of large language models (LLMs) demonstrates that these large-scale foundation models achieve remarkable capabilities across a wide range of language tasks and domains. The success of the statistical learning approach challenges our unde ...

Springer2023

Deep learning-based analysis of multiple sclerosis lesions with high and ultra-high field MRI

Francesco La Rosa

Multiple sclerosis (MS) is the most common demyelinating disease of the central nervous system and affects almost 3 million people worldwide. There is currently no cure for MS, and its symptoms, starting with fatigue and weakness, often progress over time ...

EPFL2022

A Data-Knowledge Hybrid Driven Method for Gas Turbine Gas Path Diagnosis

Dimitrios Kyritsis, Jinzhi Lu

Gas path fault diagnosis of a gas turbine is a complex task involving field data analysis and knowledge-based reasoning. In this paper, a data-knowledge hybrid driven method for gas path fault diagnosis is proposed by integrating a physical model-based gas ...

MDPI2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Automated approach for the evaluation of glutathione-S-transferase P1-1 inhibition by organometallic anticancer compounds

Paul Joseph Dyson

A novel automated method based on sequential injection analysis (SIA), a non-segmented flow injection technique, was developed to evaluate glutathione S-transferase P1-1 (GST P1-1) activity in the presence of organometallic complexes with putative anticanc ...

TAYLOR & FRANCIS LTD2022

Textual Explanations and Critiques in Recommendation Systems

Diego Matteo Antognini

Artificial intelligence and machine learning algorithms have become ubiquitous. Although they offer a wide range of benefits, their adoption in decision-critical fields is limited by their lack of interpretability, particularly with textual data. Moreover, ...

EPFL2022

Automated Verification of Network Function Binaries

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

USENIX Association2022

Cognitive twin construction for system of systems operation based on semantic integration and high-level architecture

Dimitrios Kyritsis, Jinzhi Lu

With the increasing complexity of engineered systems, digital twins (DTs) have been widely used to support integrated modeling, simulation, and decision-making of the system of systems (SoS). However, when integrating DTs of each constituent system, it is ...

IOS PRESS2022

Assessment of metal-based dihydrofolate reductase inhibitors on a novel mesofluidic platform

Paul Joseph Dyson

A new miniaturized micro sequential injection coupled with the lab-on-valve (mu SIA-LOV) technique was full-blown to perform inhibitory studies on dihydrofolate reductase (DHFR). The system was used to evaluate the DHFR inhibition activity of metal-based a ...

ELSEVIER SCIENCE SA2022

Automated Design: A Journey Across Modelling, Optimization, and Education

Cyril Picard

Machine intelligence greatly impacts almost all domains of our societies. It is profoundly changing the field of mechanical engineering with new technical possibilities and processes. The education of future engineers also needs to adapt in terms of techni ...

EPFL2021

Conversational Multi-Hop Reasoning with Neural Commonsense Knowledge and Symbolic Logic Rules

Antoine Bosselut

One of the challenges faced by conversational agents is their inability to identify unstated presumptions of their users' commands, a task trivial for humans due to their common sense. In this paper, we propose a zeroshot commonsense reasoning system for c ...

ASSOC COMPUTATIONAL LINGUISTICS-ACL2021

Learning Analytics for Adaptive and Self-Improving Learning Environments for Inductive Teaching

Louis Pierre Faucon

The emergence of digital technology is changing education in many ways. A particularly interesting aspect of this transformation is the development of learning environments that can automatically adapt to individual students and can collect data in order t ...

EPFL2021

Proving and Disproving Equivalence of Functional Programming Assignments

Viktor Kuncak, Dragana Milovancevic

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

2023

Automated Design Tool for Automotive Control Actuators

Jürg Alexander Schiffmann, Cyril Picard

Automated design tools are seldom used in industry. Their potential, however, is high, especially in companies mostly active in variant design, where custom tools could help cut down development time in the early stages. The design of geared electro-mechan ...

2020

A Bayesian Model of Individual Differences and Flexibility in Inductive Reasoning for Categorization of Examples

Pierre Dillenbourg, Jennifer Kaitlyn Olsen, Louis Pierre Faucon

Inductive reasoning is an important educational practice but can be difficult for teachers to support in the classroom due to the high level of preparation and classroom time needed to choose the teaching materials that challenge students' current views. I ...

ASSOC COMPUTING MACHINERY2020

Seek and learn: Automated identification of microevents in animal behaviour using envelopes of acceleration data and machine learning

Kamiar Aminian, Hooman Dejnabadi, Pritish Chakravarty

Animal‐borne accelerometers have been used across more than 120 species to infer biologically significant information such as energy expenditure and broad behavioural categories. While the accelerometer’s high sensitivity to movement and fast response time ...

2020

Nonintrusive and Adaptive Monitoring for Locating Voltage Attacks in Virtualized FPGAs

Mirjana Stojilovic, Andrea Guerrieri, Seyedeh Sharareh Mirzargar

In this work, we present an automated approach for locating power-wasting attackers in shared FPGAs. In this approach, the FPGA shell is responsible for, first, placing the user designs and, second, inserting voltage sensors in a nonintrusive and adaptive ...

IEEE COMPUTER SOC2020

An Ink–and–Paper Automaton: The Conceptual Mechanization of Cognition and the Practical Automation of Reasoning in Leibniz’s De Affectibus (1679)

Simon François Dumas Primbault

On ten loose handwritten folios dating back from April 1679, Leibniz gradually devised, in the course of three days, a full-blown theory of thought that nonetheless remained unpublished and still has received little attention from scholars. Conceiving of a ...

2020