A Toolbox for Barriers on Interactive Oracle Proofs

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

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

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

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

In this thesis, we give new protocols that offer a quantum advantage for problems in ML, Physics, and Finance. Quantum mechanics gives predictions that are inconsistent with local realism. The experiment proving this fact (Bell, 1964) gives a quantum proto ...

Modern integrated circuits are tiny yet incredibly complex technological artifacts, composed of millions and billions of individual structures working in unison. Managing their complexity and facilitating their design drove part of the co-evolution of mode ...

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

Group testing is a technique that can reduce the number of tests needed to identify infected members in a population, by pooling together multiple diagnostic samples. Despite the variety and importance of prior results, traditional work on group testing ha ...

Physics-informed machine learning (PIML) is a set of methods and tools that systematically integrate machine learning (ML) algorithms with physical constraints and abstract mathematical models developed in scientific and engineering domains. As opposed to ...

According to physicalism, everything is physical or metaphysically connected to the physical. If physicalism were true, it seems that we should - in principle - be able to reduce the descriptions and explanations of special sciences to physical ones, for e ...

A hash proof system (HPS) is a form of implicit proof of membership to a language. Out of the very few existing post-quantum HPS, most are based on languages of ciphertexts of code-based or lattice-based cryptosystems and inherently suffer from a gap cause ...

A shift from fossil-based energy and products to more sustainable alternatives is essential to reduce greenhouse gas emissions and associated climate change impacts. Biomass represents a promising alternative for providing fuels and carbon-based products w ...

Preventing the misfolding or aggregation of transactive response DNA binding protein with 43 kDa (TDP-43) is the most actively pursued disease-modifying strategy to treat amyotrophic lateral sclerosis and other neurodegenerative diseases. In this work, we ...

Existing machine learning potentials for predicting phonon properties of crystals are typically limited on a material-to-material basis, primarily due to the exponential scaling of model complexity with the number of atomic species. We address this bottlen ...

This data set provides a computer-assisted proof for the kernel inequalities needed to prove universal optimality in the paper "Universal optimality of the E_8 and Leech lattices and interpolation formulas" (by Cohn, Kumar, Miller, Radchenko, and Viazovska ...

IoT devices are increasingly present, both in the industry and in consumer markets, but their security remains weak, which leads to an unprecedented number of attacks against them. In order to reduce the attack surface, one approach is to analyze the binar ...

Zero knowledge plays a central role in cryptography and complexity. The seminal work of Ben-Or et al. (STOC 1988) shows that zero knowledge can be achieved unconditionally for any language in NEXP, as long as one is willing to make a suitable physical assu ...

We survey lower-bound results in complexity theory that have been obtained via newfound interconnections between propositional proof complexity, boolean circuit complexity, and query/communication complexity. We advocate for the theory of total search prob ...

The celebrated PCP Theorem states that any language in NP can be decided via a verifier that reads O(1) bits from a polynomially long proof. Interactive oracle proofs (IOP), a generalization of PCPs, allow the verifier to interact with the prover for multi ...

Assessing the traversability of rugged terrain is a difficult challenge for legged robots, especially when they implement multiple, distinct gaits. We tackle this problem on the k-rock2 amphibious, sprawling gait robot by training a gait-dependent traversa ...

In this paper, we analyze the recently proposed stochastic primal-dual hybrid gradient (SPDHG) algorithm and provide new theoretical results. In particular, we prove almost sure convergence of the iterates to a solution with convexity and linear convergenc ...

A Toolbox for Barriers on Interactive Oracle Proofs

Chat with Graph Search

Orthologic with Axioms

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

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

Quantum Protocols for ML, Physics, and Finance

Graph generative deep learning models with an application to circuit topologies

LISA – A Modern Proof System

Community-Aware Group Testing

Physics-Informed Machine Learning for Modeling and Control of Dynamical Systems

Why computational complexity may set impenetrable barriers for epistemic reductionism

A Gapless Post-quantum Hash Proof System in the Hamming Metric

Decision support for the design of integrated biorefineries

Effective Inhibition of TDP-43 Aggregation by Native State Stabilization

Million-scale data integrated deep neural network for phonon properties of heuslers spanning the periodic table

Computer-assisted proof of kernel inequalities

Investigating Graph Embedding Methods for Cross-Platform Binary Code Similarity Detection

Spatial Isolation Implies Zero Knowledge Even in a Quantum World

Proofs, Circuits, and Communication

A PCP Theorem for Interactive Proofs and Applications

Gait-dependent Traversability Estimation on the k-rock2 Robot

On The Convergence Of Stochastic Primal-Dual Hybrid Gradient