Modelling Arbitrary Computations in the Symbolic Model using an Equational Theory for Bounded Binary Circuits

• URL: http://arxiv.org/abs/2507.21731v1
• Date: Tue, 29 Jul 2025 12:09:50 GMT
• Title: Modelling Arbitrary Computations in the Symbolic Model using an Equational Theory for Bounded Binary Circuits
• Authors: Michiel Marcus, Frank Westers, Anne Nijsten,
• Abstract summary: We propose a class of equational theories for bounded binary circuits with the finite variant property.<n>These theories could serve as a building block to specify cryptographic primitive implementations.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this work, we propose a class of equational theories for bounded binary circuits that have the finite variant property. These theories could serve as a building block to specify cryptographic primitive implementations and automatically discover attacks as binary circuits in the symbolic model. We provide proofs of equivalence between this class of equational theories and Boolean logic up to circuit size 3 and we provide the variant complexities and performance benchmarks using Maude-NPA. This is the first result in this direction and follow-up research is needed to improve the scalability of the approach.

Related papers

• Automatically Identifying Local and Global Circuits with Linear Computation Graphs [45.760716193942685]
  We introduce our circuit discovery pipeline with Sparse Autoencoders (SAEs) and a variant called Transcoders. Our methods do not require linear approximation to compute the causal effect of each node. We analyze three kinds of circuits in GPT-2 Small: bracket, induction, and Indirect Object Identification circuits.
  arXiv  Detail & Related papers  (2024-05-22T17:50:04Z)
• Exponential improvements in the simulation of lattice gauge theories using near-optimal techniques [0.0]
  We provide explicit circuit constructions as well as T-gate counts and logical qubit counts for Hamiltonian simulation.<n>We find up to 25 orders of magnitude reduction in space-time volume over Trotter methods for simulations of non-Abelian lattice gauge theories.
  arXiv  Detail & Related papers  (2024-05-16T19:36:49Z)
• Circuit Transformer: A Transformer That Preserves Logical Equivalence [20.8279111910994]
  We introduce a generative neural model, the "Circuit Transformer", which produces logic circuits strictly equivalent to given Boolean functions.<n>A Markov decision process formulation is also proposed for optimizing certain objectives of circuits.
  arXiv  Detail & Related papers  (2024-03-14T03:24:14Z)
• A Sampling Theory Perspective on Activations for Implicit Neural Representations [73.6637608397055]
  Implicit Neural Representations (INRs) have gained popularity for encoding signals as compact, differentiable entities. We conduct a comprehensive analysis of these activations from a sampling theory perspective. Our investigation reveals that sinc activations, previously unused in conjunction with INRs, are theoretically optimal for signal encoding.
  arXiv  Detail & Related papers  (2024-02-08T05:52:45Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• General quantum algorithms for Hamiltonian simulation with applications to a non-Abelian lattice gauge theory [44.99833362998488]
  We introduce quantum algorithms that can efficiently simulate certain classes of interactions consisting of correlated changes in multiple quantum numbers. The lattice gauge theory studied is the SU(2) gauge theory in 1+1 dimensions coupled to one flavor of staggered fermions. The algorithms are shown to be applicable to higher-dimensional theories as well as to other Abelian and non-Abelian gauge theories.
  arXiv  Detail & Related papers  (2022-12-28T18:56:25Z)
• Multiparameter Persistent Homology-Generic Structures and Quantum Computing [0.0]
  This article is an application of commutative algebra to the study of persistent homology in topological data analysis. The generic structure of such resolutions and the classifying spaces are studied using results spanning several decades of research.
  arXiv  Detail & Related papers  (2022-10-20T17:30:20Z)
• Gauge-equivariant flow models for sampling in lattice field theories with pseudofermions [51.52945471576731]
  This work presents gauge-equivariant architectures for flow-based sampling in fermionic lattice field theories using pseudofermions as estimators for the fermionic determinant. This is the default approach in state-of-the-art lattice field theory calculations, making this development critical to the practical application of flow models to theories such as QCD.
  arXiv  Detail & Related papers  (2022-07-18T21:13:34Z)
• A Complete Equational Theory for Quantum Circuits [58.720142291102135]
  We introduce the first complete equational theory for quantum circuits. Two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations.
  arXiv  Detail & Related papers  (2022-06-21T17:56:31Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Joint Network Topology Inference via Structured Fusion Regularization [70.30364652829164]
  Joint network topology inference represents a canonical problem of learning multiple graph Laplacian matrices from heterogeneous graph signals. We propose a general graph estimator based on a novel structured fusion regularization. We show that the proposed graph estimator enjoys both high computational efficiency and rigorous theoretical guarantee.
  arXiv  Detail & Related papers  (2021-03-05T04:42:32Z)
• A Study of Continuous Vector Representationsfor Theorem Proving [2.0518509649405106]
  We develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We propose datasets that can be used to train these syntactic and semantic properties.
  arXiv  Detail & Related papers  (2021-01-22T15:04:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.