AI 中文总结
该研究将递归Datalog程序编译为量子退火器可处理的2局域伊辛模型，经Lean 4验证正确性，还映射到商用退火器拓扑并表征基态获取情况。
AI 中文摘要
量子退火器通过寻找可编程物理系统（即2局域伊辛模型，其能量函数为哈密顿量）的最低能量（基态）来解决问题。我们将递归Datalog程序编译为这类模型，使得基态投影到程序的最小Herbrand模型上。该编译器包含四个阶段：二值化、实例化、归约为Min-Ones SAT公式以及伊辛编码。每条规则会对违反该规则的唯一赋值施加能量惩罚，同时对每个为真的原子施加小额统一成本，以此选择最小模型。我们在理论和实践两方面均有贡献：每个阶段都提供了正确性引理，且在Lean 4中验证了对应定理，确立了编译后模型的基态投影到程序最小Herbrand模型的关系。我们将编译后的模型映射到商用退火器的拓扑结构上，并在经典退火和模拟量子退火场景下，表征何时以及能否获得该经认证的基态。
英文摘要
Quantum annealers solve problems by finding the lowest-energy (ground) state of a programmable physical system, a 2-local Ising model, whose energy function is the Hamiltonian. We compile recursive Datalog programs into such models so that the ground state projects onto the program's minimal Herbrand model. The compiler has four stages: binarization, grounding, reduction to a Min-Ones SAT formula, and Ising encoding. Each rule becomes an energy penalty on the one assignment that violates it, and a small uniform cost on every true atom selects the minimal model. We contribute both in theory and in practice with per-stage correctness lemmas and a correspondence theorem, verified in Lean 4, establishing that the ground state of the compiled model projects onto the program's minimal Herbrand model. We map the compiled models onto the topologies of commercial annealers and characterize, under classical and simulated-quantum annealing, whether and when that certified ground state is attained.
Comments12 pages, 4 pages of appendix, Datalog 2.0 preprint
