Reproduce “Towards Datalog on Quantum Annealers: Compiling Recursive Logic Programs with Bottom-up Semantics to 2-local Ising Models” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Bruno Rucy Carneiro Alves de Lima, Victor Henrique Cabral Pinheiro, Evgenii Dolzhkov, Joseph Haske
Researchers at the University of Tartu and Lucidarium Systems formally verified a four-stage compiler that translates recursive Datalog programs into 2-local Ising models, where the Ising model's ground state uniquely corresponds to the Datalog program's minimal Herbrand model. Empirical evaluation revealed that programs with "foundedness traps" create challenging energy landscapes, leading to poor recovery rates for solvers, and highlighted physical annealers' precision limitations for distinguishing the minimal model.
Key insights
- Formal verification provides strong guarantees that the compiled Ising model's ground state correctly represents the Datalog program's minimal Herbrand model.
- Recursive Datalog programs with "unfounded self-supporting sets" create energy landscapes with numerous "foundedness traps" (local minima), making it difficult for annealers to find the true global minimum.
- The limited analog precision of current physical quantum annealers poses a significant challenge, as the subtle energy differences used to distinguish the minimal model can be below the hardware's resolution capabilities.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.