We introduce dynamically weighted tree transducers (dyn-wtts), a weighted generalization of top-down tree transducers with regular look-ahead in which rule weights are determined by external tree weighters mapping input trees to values in a commutative semiring. The general framework allows for any kind of device defining a weighted tree language to serve as a tree weighter. In this paper, we focus on weighters implemented by different classes of tree automata and show how the resulting classes of weighted tree transformations relate to one another and to known classes. In particular, we show how conventional top-down weighted tree transducers (with and without regular look-ahead) can be expressed as dyn-wtts, also in the linear and non-deleting cases.

We define weighted alternating tree automata — a generalization of weighted (non-alternating) tree automata, (unweighted) alternating tree automata, and weighted alternating (string) automata — over commutative semirings. We study their expressive power, and show that it is equivalent to that of weighted tree automata exactly when the employed semiring is locally finite. In our main result, we characterize the class of weighted tree languages defined by weighted alternating tree automata as the closure of the recognizable weighted tree languages under inverse tree homomorphisms.

We investigate whether synthetic pretraining data generated from a formal grammar modeling syntactic dependencies can improve English language models. Building upon the structured pretraining data approach of Papadimitriou and Jurafsky (2023), we develop a grammar that more closely mirrors empirical dependency structures. Our results are negative – this type of pretraining significantly degrades model performance, with both our and their pretraining approach performing worse than no pretraining at all. We analyze potential explanations for these findings and discuss implications for future work on structured-data pretraining.

Sledgehammer, a component of the interactive proof assistant Isabelle/HOL, aims to increase proof automation by automatically discharging proof goals with the help of external provers. Among these provers are a group of satisfiability modulo theories (SMT) solvers with support for the SMT-LIB input language. Despite existing formalizations of IEEE floating-point arithmetic in both Isabelle/HOL and SMT-LIB, Sledgehammer employs an abstract translation of floating-point types and constants, depriving the SMT solvers of the opportunity to make use of their dedicated decision procedures for floating-point arithmetic.

We show that, by extending Sledgehammer’s translation from the language of Isabelle/HOL into SMT-LIB with an interpretation of floating-point types and constants, floating-point reasoning in SMT solvers can be made available to Isabelle/HOL. Our main contribution is a description and implementation of such an extension. An evaluation of the extended translation shows a significant increase of Sledgehammer’s success rate on proof goals involving floating-point arithmetic.