Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.29287

Post-Pruning vs. Early Stopping: Which Works Better for Link Prediction with AnyBurl?

Thomas Eiter·Davide Soldà·Hai Xia
View original source ↗Read source document ↗Export metadata ↓

Abstract

Rule-based link prediction combines symbolic and statistical artificial intelligence methods by inductively learning a set of rules from a knowledge graph (KG), with the aim of completing the graph when a query cannot be answered from the KG alone. Several systems have been proposed, and while they perform well on classical benchmarks, even compared with embedding-based systems, many of them produce a large number of rules. This compromises scalability in the query-answering phase, especially under strong hardware constraints. In this work, we investigate the behavior of AnyBurl, a state-of-the-art rule learner for link prediction, to determine whether running it for a given time and then pruning the learned rules yields better query-answering performance at test time than a simpler approach that stops rule generation earlier.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Thomas Eiter, Davide Soldà, Hai Xia. 2026-10-21. Post-Pruning vs. Early Stopping: Which Works Better for Link Prediction with AnyBurl?. https://arxiv.org/abs/2610.29287

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Formula size game and model checking for modal substitution calculus

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that floating-point recurrent graph neural networks have the same expressive power as graded modal substitution calculus GMSC, which is the extension of MSC with counting modalities. GMSC can be further extended with the counting global modality, resulting in the logic GGMSC, which corresponds to floating-point GNNs with global readout mechanisms. In this paper, we introduce a formula size game that characterizes the expressive power of MSC, GMSC, GGMSC, and related logics. Furthermore, we study the expressiveness and model checking of logics in this family. We prove that MSC and its extensions (GMSC, GGMSC) are as expressive as linear tape-bounded Turing machines, while asynchronous variants are linked to the modal mu-calculus and modal computation logic MCL. We establish that for MSC, GMSC and GGMSC, both the combined and data complexity of model checking are PSPACE-complete, and for their asynchronous variants, both complexities are PTIME-complete. We also establish that for the propositional fragment SC of MSC, the combined complexity of model checking is PSPACE-complete, while for asynchronous SC it is PTIME-complete, and in both cases, the data complexity is constant. As a corollary, we observe that SC satisfiability is PSPACE-complete and NP-complete for its asynchronous variant. Finally, we construct a universal reduction from all recursively enumerable problems to MSC model checking.

cs.LO↗
arXiv2026

Theorem prover Arend

This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.

cs.LO↗
arXiv2026

Deciding Scale Placement in MXFP4 Dot Products with Integer Arithmetic

The Open Compute Project's microscaling (MX) family includes MXFP4, which stores 32 four-bit elements with a shared power-of-two scale. When lowering a dot-product reduction, a compiler can apply these scales before the reduction, or defer scaling until afterwards. Although equivalent over real numbers, these formulations can produce different IEEE binary32 results through overflow or underflow, with equivalence also depending on the reduction tree. We study the legality of compiler rewrites in either direction by deriving conditions under which the two formulations are bitwise equivalent. To decide rewrite legality, we construct an integer state machine that exploits the finite element alphabet and shared power-of-two scales, modeling overflow, NaN, and subnormal rounding. We prove its faithfulness under bounded scale codes and integer coefficients, yielding an exact encoding of the equivalence query in quantifier-free linear integer arithmetic (QF_LIA). For MXFP4, we derive a closed-form sufficient upper bound on the sum of scale exponents for any fixed binary reduction tree within the supported coefficient range. This bound depends on the size of the largest proper subtree. For four tree shapes at block lengths $k\in\{2,3,4,8,16,32\}$ and two shapes at $k=64$, SMT finds counterexamples when this upper bound is increased by one exponent step. Against the standard direct encoding in quantifier-free floating-point arithmetic (QF_FP), on matched queries cvc5 proves the integer version in seconds but reaches a configured one-CPU-hour limit on the floating-point proof even at $k=2$. The implementation was cross-checked using an independent floating-point encoding, exhaustive and stratified binary32 execution, and GPU replay of counterexamples. An MLIR lowering prototype demonstrates selection between the two formulations using the certified conditions as static or runtime guards.

cs.LO↗