Publications associées à Induction for SMT Solvers

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Infusing structured knowledge priors in neural models for sample-efficient symbolic reasoning

Mattia Atzeni

The ability to reason, plan and solve highly abstract problems is a hallmark of human intelligence. Recent advancements in artificial intelligence, propelled by deep neural networks, have revolutionized disciplines like computer vision and natural language ...

EPFL2024

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

Simon Guilloud

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

Monotonicity Reasoning in the Age of Neural Foundation Models

Zeming Chen, Qiyue Gao

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

Language Model Decoding as Likelihood–Utility Alignment

Boi Faltings, Maxime Jean Julien Peyrard, Robert West, Martin Josifoski, Valentin Hartmann, Jiheng Wei, Frano Rajic, Debjit Paul

A critical component of a successful language generation pipeline is the decoding algorithm. However, the general principles that should guide the choice of a decoding algorithm re- main unclear. Previous works only compare decoding algorithms in narrow sc ...

Assoc Computational Linguistics-Acl2023

Keep Sensors in Check: Disentangling Country-Level Generalization Issues in Mobile Sensor-Based Models with Diversity Scores

Daniel Gatica-Perez, Lakmal Buddika Meegahapola

Machine learning models trained with passive sensor data from mobile devices can be used to perform various inferences pertaining to activity recognition, context awareness, and health and well-being. Prior work has improved inference performance through t ...

Assoc Computing Machinery2023

REFINER: Reasoning Feedback on Intermediate Representations

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

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

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

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

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

Dimitrios Kyritsis, Jinzhi Lu, Han Li

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

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

Dimitrios Kyritsis, Jinzhi Lu, Xiaochen Zheng, Jinwei Chen

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

Space Oddity? A Statistical Formulation of Conjunction Assessment

Anthony Christopher Davison, Soumaya Elkantassi

Satellite conjunctions involving "near misses" of space objects are becoming increasingly likely. One approach to risk analysis for them involves the computation of the collision probability, but this has been regarded as having some counterintuitive prope ...

AMER INST AERONAUTICS ASTRONAUTICS2022

Reshaping Perception for Autonomous Driving with Semantic Keypoints

Lorenzo Bertoni

The field of artificial intelligence is set to fuel the future of mobility by driving forward the transition from advanced driver-assist systems to fully autonomous vehicles (AV). Yet the current technology, backed by cutting-edge deep learning techniques, ...

EPFL2022

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Springer, Cham2022

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

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

Forough Arabshahi, 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

Distributed Meta-Learning with Networked Agents

Ali H. Sayed, Stefan Vlaski, Mert Kayaalp

Meta-learning aims to improve efficiency of learning new tasks by exploiting the inductive biases obtained from related tasks. Previous works consider centralized or federated architectures that rely on central processors, whereas, in this paper, we propos ...

EUROPEAN ASSOC SIGNAL SPEECH & IMAGE PROCESSING-EURASIP2021

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

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

Pierre Dillenbourg, Louis Pierre Faucon, Jennifer Kaitlyn Olsen

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

Stoic: Towards Disciplined Capabilities

Martin Odersky, Sandro Stucki, Nada Amin, Fengyun Liu, Paolo Giosuè Giarrusso

Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...

2020