Publication

A Toolbox for Barriers on Interactive Oracle Proofs

Publications associées (30)

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

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

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

Quantum Protocols for ML, Physics, and Finance

Grzegorz Adam Gluch

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

EPFL2024

Graph generative deep learning models with an application to circuit topologies

Igor Krawczuk

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

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

Why computational complexity may set impenetrable barriers for epistemic reductionism

Michael Herzog, Adrien Christophe Doerig, Christian Sachse

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

Springer2023

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

Serge Vaudenay, Bénédikt Minh Dang Tran

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

2023

Decision support for the design of integrated biorefineries

Julia Granacher

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

EPFL2023

Effective Inhibition of TDP-43 Aggregation by Native State Stabilization

Hilal Lashuel, Lixin Yang, Yllza Jasiqi

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

Wiley-VCH Verlag GmbH2024

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

Chen Shen, Hong Zhang, Changpeng Lin, Yong Zhao

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

NATURE PORTFOLIO2023

Computer-assisted proof of kernel inequalities

Maryna Viazovska, Abhinav Kumar

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

EPFL Infoscience2023

Spatial Isolation Implies Zero Knowledge Even in a Quantum World

Alessandro Chiesa

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

ASSOC COMPUTING MACHINERY2022

Proofs, Circuits, and Communication

Mika Tapani Göös

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

2022

A PCP Theorem for Interactive Proofs and Applications

Alessandro Chiesa

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

SPRINGER INTERNATIONAL PUBLISHING AG2022

Computation Complexity Reduction Technique for Accurate Seizure Detection Implants

Alexandre Schmid, Keyvan Farhang Razi

An automatic seizure detection method from high-resolution intracranial-EEG (iEEG) signals is presented to minimize the computational complexity and realize real-time accurate seizure detection for biomedical implants. Complex signal processing on a large ...

IEEE2022

On Semi-Algebraic Proofs and Algorithms

Mika Tapani Göös

We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where ...

Schloss Dagstuhl - Leibniz-Zentrum für Informatik2022

Zero-Knowledge IOPs with Linear-Time Prover and Polylogarithmic-Time Verifier

Alessandro Chiesa, Siqi Liu

Interactive oracle proofs (IOPs) are a multi-round generalization of probabilistically checkable proofs that play a fundamental role in the construction of efficient cryptographic proofs. ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Minimum Cost Intervention Design for Causal Effect Identification

Seyed Jalal Etesami, Negar Kiyavash, Sina Akbari

Pearl's do calculus is a complete axiomatic approach to learn the identifiable causal effects from observational data. When such an effect is not identifiable, it is necessary to perform a collection of often costly interventions in the system to learn the ...

PMLR2022

On Succinct Non-interactive Arguments in Relativized Worlds

Alessandro Chiesa

Succinct non-interactive arguments of knowledge (SNARKs) are cryptographic proofs with strong efficiency properties. Applications of SNARKs often involve proving computations that include the SNARK verifier, a technique called recursive composition. Unfort ...

SPRINGER INTERNATIONAL PUBLISHING AG2022