Publications related to A Formally Verified NAT

Related publications (33)

Tango*: constrained synthesis planning using chemically informed value functions

Daniel Paul Armstrong, Philippe Schwaller, Jeff Guo

TANGO* enables starting material constrained synthesis planning using computed molecular similarity to guide retrosynthetic search toward specific starting materials, achieving superior performance to neural network approaches. ...

Royal Society of Chemistry (RSC)2025

How data structures affect generalization in Kernel Methods and Deep Learning

Umberto Maria Tomasini

Artificial Intelligence has revolutionized numerous fields, driving advancements in healthcare, finance, and autonomous systems. At the core of this revolution lies Deep Learning---algorithms that learn representations from data through computational layer ...

EPFL2025

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

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

Task-driven neural network models predict neural dynamics of proprioception: Experimental data, activations and predictions of neural network models

Alexander Mathis, Alberto Silvio Chiappa, Alessandro Marin Vargas, Axel Bisi

Here we provide the neural data, activation and predictions for the best models and result dataframes of our article "Task-driven neural network models predict neural dynamics of proprioception". It contains the behavioral and neural experimental data (cu ...

EPFL Infoscience2024

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

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Analytical Computation of the Sensitivity Coefficients in Hybrid AC/DC Networks

Mario Paolone, Willem Lambrichts

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

2024

On the number of regions of piecewise linear neural networks

Michaël Unser, Alexis Marie Frederic Goujon

Many feedforward neural networks (NNs) generate continuous and piecewise-linear (CPWL) mappings. Specifically, they partition the input domain into regions on which the mapping is affine. The number of these so-called linear regions offers a natural metric ...

2024

Safe Deep Neural Networks

Kyle Michael Matoba

The capabilities of deep learning systems have advanced much faster than our ability to understand them. Whilst the gains from deep neural networks (DNNs) are significant, they are accompanied by a growing risk and gravity of a bad outcome. This is troubli ...

EPFL2024

Intermediate Address Space: virtual memory optimization of heterogeneous architectures for cache-resident workloads

Qunyou Liu, David Atienza Alonso, Marina Zapater Sancho, Darong Huang, Luis Maria Costero Valero

The increasing demand for computing power and the emergence of heterogeneous computing architectures have driven the exploration of innovative techniques to address current limitations in both the compute and memory subsystems. One such solution is the use ...

2024

Performing and Detecting Backdoor Attacks on Face Recognition Algorithms

Alexander Carl Unnervik

The field of biometrics, and especially face recognition, has seen a wide-spread adoption the last few years, from access control on personal devices such as phones and laptops, to automated border controls such as in airports. The stakes are increasingly ...

EPFL2024

Generalization of Scaled Deep ResNets in the Mean-Field Regime

Volkan Cevher, Grigorios Chrysos, Fanghui Liu

Despite the widespread empirical success of ResNet, the generalization properties of deep ResNet are rarely explored beyond the lazy training regime. In this work, we investigate scaled ResNet in the limit of infinitely deep and wide neural networks, of wh ...

2024

Deep Learning Theory Through the Lens of Diagonal Linear Networks

Scott William Pesme

In this PhD manuscript, we explore optimisation phenomena which occur in complex neural networks through the lens of

2

-layer diagonal linear networks. This rudimentary architecture, which consists of a two layer feedforward linear network with a diagonal ...

EPFL2024

Exploring High-Performance and Energy-Efficient Architectures for Edge AI-Enabled Applications

Joshua Alexander Harrison Klein

The desire and ability to place AI-enabled applications on the edge has grown significantly in recent years. However, the compute-, area-, and power-constrained nature of edge devices are stressed by the needs of the AI-enabled applications, due to a gener ...

EPFL2024

Random matrix methods for high-dimensional machine learning models

Antoine Philippe Michel Bodin

In the rapidly evolving landscape of machine learning research, neural networks stand out with their ever-expanding number of parameters and reliance on increasingly large datasets. The financial cost and computational resources required for the training p ...

EPFL2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024

Statistical Inference for Inverse Problems: From Sparsity-Based Methods to Neural Networks

Pakshal Narendra Bohra

In inverse problems, the task is to reconstruct an unknown signal from its possibly noise-corrupted measurements. Penalized-likelihood-based estimation and Bayesian estimation are two powerful statistical paradigms for the resolution of such problems. They ...

EPFL2024

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

A Theory of Finite-Width Neural Networks: Generalization, Scaling Laws, and the Loss Landscape

Berfin Simsek

Deep learning has achieved remarkable success in various challenging tasks such as generating images from natural language or engaging in lengthy conversations with humans. The success in practice stems from the ability to successfully train massive neural ...

EPFL2023