Search

We present $griz$ photometric light curves for the full 5 years of the Dark Energy Survey Supernova program (DES-SN), obtained with both forced Point Spread Function (PSF) photometry on Difference Images (DIFFIMG) performed during survey operations, and Scene Modelling Photometry (SMP) on search images processed after the survey. This release contains $31,636$ DIFFIMG and $19,706$ high-quality SMP light curves, the latter of which contains $1635$ photometrically-classified supernovae that pass cosmology quality cuts. This sample spans the largest redshift ($z$) range ever covered by a single SN survey ($0.1

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale., Comment: Submitted to FMCAD 2024, https://fmcad.org/FMCAD24/

We present an updated ephemeris and physical parameters for the exoplanet WASP-77 A b. In this effort, we combine 64 ground- and space-based transit observations, 6 space-based eclipse observations, and 32 radial velocity observations to produce the most precise orbital solution to date for this target, aiding in the planning of James Webb Space Telescope (JWST) and Ariel observations and atmospheric studies. We report a new orbital period of 1.360029395 +- 5.7e-8 days, a new mid-transit time of 2459957.337860 +- 4.3e-5 BJDTDB (Barycentric Julian Date in the Barycentric Dynamical Time scale; arXiv:1005.4415) and a new mid-eclipse time of 2459956.658192 +- 6.7e-5 BJDTDB. Furthermore, the methods presented in this study reduce the uncertainties in the planet mass to 1.6654 +- 4.5e-3 Mjup and orbital period to 1.360029395 +- 5.7e-8 days by factors of 15.1 and 10.9, respectively. Through a joint fit analysis comparison of transit data taken by space-based and citizen science-led initiatives, our study demonstrates the power of including data collected by citizen scientists compared to a fit of the space-based data alone. Additionally, by including a vast array of citizen science data from ExoClock, Exoplanet Transit Database (ETD), and Exoplanet Watch, we can increase our observational baseline and thus acquire better constraints on the forward propagation of our ephemeris than what is achievable with TESS data alone., Comment: Updated a co-author name. Added a co-author. Added an acknowledgement

Time-dependent potentials are common in galactic systems that undergo significant evolution, interactions, or encounters with other galaxies, or when there are dynamic processes like star formation and merging events. Recent studies show that an ensemble approach along with the so-called snapshot framework in dynamical system theory provide a powerful tool to analyze time dependent dynamics. In this work, we aim to explore and quantify the phase space structure and dynamical complexity in time-dependent galactic potentials consisting of multiple components. We apply the classical method of Poincar\'e-surface of section to analyze the phase space structure in a chaotic Hamiltonian system subjected to parameter drift. This, however, makes sense only when the evolution of a large ensemble of initial conditions is followed. Numerical simulations explore the phase space structure of such ensembles while the system undergoes a continuous parameter change. The pair-wise average distance of ensemble members allows us to define a generalized Lyapunov-exponent, that might also be time dependent, to describe the system stability. We provide a comprehensive dynamical analysis of the system under circumstances where linear mass transfer occurs between the disk and bulge components of the model., Comment: 13 pages, 13 figures (including the Appendix). The article was accepted for publication at Astronomy & Astrophysics. The official acceptance date is 04/11/2024. Reason of replacement: Comments and suggestions from the referee, along with fixed spelling inconsistencies

We present the Flagship galaxy mock, a simulated catalogue of billions of galaxies designed to support the scientific exploitation of the Euclid mission. Euclid is a medium-class mission of the European Space Agency optimised to determine the properties of dark matter and dark energy on the largest scales of the Universe. It probes structure formation over more than 10 billion years primarily from the combination of weak gravitational lensing and galaxy clustering data. The breath of Euclid's data will also foster a wide variety of scientific analyses. The Flagship simulation was developed to provide a realistic approximation to the galaxies that will be observed by Euclid and used in its scientific analyses. We ran a state-of-the-art N-body simulation with four trillion particles, producing a lightcone on the fly. From the dark matter particles, we produced a catalogue of 16 billion haloes in one octant of the sky in the lightcone up to redshift z=3. We then populated these haloes with mock galaxies using a halo occupation distribution and abundance matching approach, calibrating the free parameters of the galaxy mock against observed correlations and other basic galaxy properties. Modelled galaxy properties include luminosity and flux in several bands, redshifts, positions and velocities, spectral energy distributions, shapes and sizes, stellar masses, star formation rates, metallicities, emission line fluxes, and lensing properties. We selected a final sample of 3.4 billion galaxies with a magnitude cut of H_E<26, where we are complete. We have performed a comprehensive set of validation tests to check the similarity to observational data and theoretical models. In particular, our catalogue is able to closely reproduce the main characteristics of the weak lensing and galaxy clustering samples to be used in the mission's main cosmological analysis. (abridged), Comment: Paper submitted as part of the A&A special issue `Euclid on Sky', which contains Euclid key reference papers and first results from the Euclid Early Release Observations

The current standard model of cosmology successfully describes a variety of measurements, but the nature of its main ingredients, dark matter and dark energy, remains unknown. Euclid is a medium-class mission in the Cosmic Vision 2015-2025 programme of the European Space Agency (ESA) that will provide high-resolution optical imaging, as well as near-infrared imaging and spectroscopy, over about 14,000 deg^2 of extragalactic sky. In addition to accurate weak lensing and clustering measurements that probe structure formation over half of the age of the Universe, its primary probes for cosmology, these exquisite data will enable a wide range of science. This paper provides a high-level overview of the mission, summarising the survey characteristics, the various data-processing steps, and data products. We also highlight the main science objectives and expected performance., Comment: Accepted for publication in the A&A special issue`Euclid on Sky'

Among the numerous heat conduction models, the Guyer--Krumhansl equation has a special role. Besides its various application possibilities in nanotechnology, cryotechnology, and even in case of modeling heterogeneous materials, it poses additional mathematical challenges compared to the Fourier or Cattaneo {(a.k.a. Maxwell--Cattaneo--Vernotte)} equations. Furthermore, the Guyer--Krumhansl equation is the first heat conduction model, which includes the curl of the heat flux density in the evolution equation. In the present paper, we place our focus on the consequences of the existence of such whirling heat current density by solving the two-dimensional Guyer--Krumhansl equation with a space and time-dependent heat pulse boundary condition. The discretization poses further challenges in regard to the boundary condition for which we propose a particular extrapolation method. Furthermore, with the help of the Helmholtz decomposition, we show the analogy with the linearized acoustics of Newtonian fluids, which reveals how the heat flux density plays the role of the velocity field. Our solutions also reveal an unexpected temperature evolution caused by the whirling heat flux density, namely, the temperature can locally be decreased for a short time in a case when the curl of the heat flux density dominates the heat conduction process.

Deep learning has enabled breakthroughs in automated diagnosis from medical imaging, with many successful applications in ophthalmology. However, standard medical image classification approaches only assess disease presence at the time of acquisition, neglecting the common clinical setting of longitudinal imaging. For slow, progressive eye diseases like age-related macular degeneration (AMD) and primary open-angle glaucoma (POAG), patients undergo repeated imaging over time to track disease progression and forecasting the future risk of developing disease is critical to properly plan treatment. Our proposed Longitudinal Transformer for Survival Analysis (LTSA) enables dynamic disease prognosis from longitudinal medical imaging, modeling the time to disease from sequences of fundus photography images captured over long, irregular time periods. Using longitudinal imaging data from the Age-Related Eye Disease Study (AREDS) and Ocular Hypertension Treatment Study (OHTS), LTSA significantly outperformed a single-image baseline in 19/20 head-to-head comparisons on late AMD prognosis and 18/20 comparisons on POAG prognosis. A temporal attention analysis also suggested that, while the most recent image is typically the most influential, prior imaging still provides additional prognostic value., Comment: Accepted to npj Digital Medicine

Volumetric brain reconstructions provide an unprecedented opportunity to gain insights into the complex connectivity patterns of neurons in an increasing number of organisms. Here, we model and quantify the complexity of the resulting neural connectomes in the fruit fly, mouse, and human and unveil a simple set of shared organizing principles across these organisms. To put the connectomes in a physical context, we also construct contactomes, the network of neurons in physical contact in each organism. With these, we establish that physical constraints -- either given by pairwise distances or the contactome -- play a crucial role in shaping the network structure. For example, neuron positions are highly optimal in terms of distance from their neighbors. However, spatial constraints alone cannot capture the network topology, including the broad degree distribution. Conversely, the degree sequence alone is insufficient to recover the spatial structure. We resolve this apparent conflict by formulating scalable maximum entropy models, incorporating both types of constraints. The resulting generative models have predictive power beyond the input data, as they capture several additional biological and network characteristics, like synaptic weights and graphlet statistics., Comment: 24 pages, 20 figures

Realistic modeling of ecological population dynamics requires spatially explicit descriptions that can take into account spatial heterogeneity as well as long-distance dispersal. Here, we present Monte Carlo simulations and numerical renormalization group results for the paradigmatic model, the contact process, in the combined presence of these factors in both one and two-dimensional systems. Our results confirm our analytic arguments stating that the density vanishes smoothly at the extinction threshold, in a way characteristic of infinite-order transitions. This extremely smooth vanishing of the global density entails an enhanced exposure of the population to extinction events. At the same time, a reverse order parameter, the local persistence displays a discontinuity characteristic of mixed-order transitions, as it approaches a non-universal critical value algebraically with an exponent $\beta_p'<1$., Comment: 8 pages, 6 figures

The discovery of Little Red Dots (LRDs) -- a population of compact, high-redshift, dust-reddened galaxies -- is one of the most surprising results from JWST. However, the nature of LRDs is still debated: does the near-infrared emission originate from accreting supermassive black holes (SMBHs), or intense star formation? In this work, we utilize ultra-deep Chandra observations and study LRDs residing behind the lensing galaxy cluster, Abell~2744. We probe the X-ray emission from individual galaxies but find that they remain undetected and provide SMBH mass upper limits of $\lesssim(1.5-16)\times10^{6}~\rm{M_{\odot}}$ assuming Eddington limited accretion. To increase the signal-to-noise ratios, we conduct a stacking analysis of the full sample with a total lensed exposure time of $\approx87$~Ms. We also bin the galaxies based on their stellar mass, lensing magnification, and detected broad-line H$\alpha$ emission. For the LRDs exhibiting broad-line H$\alpha$ emission, there is a hint of a stacked signal ($\sim2.6\sigma$), corresponding to a SMBH mass of $\sim3.2\times10^{6}~\rm{M_{\odot}}$. Assuming unobscured, Eddington-limited accretion, this BH mass is at least 1.5 orders of magnitude lower than that inferred from virial mass estimates using JWST spectra. Given galaxy-dominated stellar mass estimates, our results imply that LRDs do not host over-massive SMBHs and/or accrete at a few percent of their Eddington limit. However, alternative stellar mass estimates may still support that LRDs host over-massive BHs. The significant discrepancy between the JWST and Chandra data hints that the scaling relations used to infer the SMBH mass from the H$\alpha$ line and virial relations may not be applicable for high-redshift LRDs., Comment: Accepted by ApJL; DOI: 10.3847/2041-8213/ad5669

$ $Low density cosmic voids gravitationally lens the cosmic microwave background (CMB), leaving a negative imprint on the CMB convergence $\kappa$. This effect provides insight into the distribution of matter within voids, and can also be used to study the growth of structure. We measure this lensing imprint by cross-correlating the Planck CMB lensing convergence map with voids identified in the Dark Energy Survey Year 3 data set, covering approximately 4,200 deg$^2$ of the sky. We use two distinct void-finding algorithms: a 2D void-finder which operates on the projected galaxy density field in thin redshift shells, and a new code, Voxel, which operates on the full 3D map of galaxy positions. We employ an optimal matched filtering method for cross-correlation, using the MICE N-body simulation both to establish the template for the matched filter and to calibrate detection significances. Using the DES Y3 photometric luminous red galaxy sample, we measure $A_\kappa$, the amplitude of the observed lensing signal relative to the simulation template, obtaining $A_\kappa = 1.03 \pm 0.22$ ($4.6\sigma$ significance) for Voxel and $A_\kappa = 1.02 \pm 0.17$ ($5.9\sigma$ significance) for 2D voids, both consistent with $\Lambda$CDM expectations. We additionally invert the 2D void-finding process to identify superclusters in the projected density field, for which we measure $A_\kappa = 0.87 \pm 0.15$ ($5.9\sigma$ significance). The leading source of noise in our measurements is Planck noise, implying that future data from the Atacama Cosmology Telescope (ACT), South Pole Telescope (SPT) and CMB-S4 will increase sensitivity and allow for more precise measurements., Comment: 16 pages, 9 figures. Accepted for publication in MNRAS

Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique., Comment: In Proceedings LSFA/HCVS 2023, arXiv:2404.13672. This research was partially funded by the UNKP-22-2,3-I New National Excellence Program and Project no. 2019-1.3.1-KK-2019-00004, which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the 2019-1.3.1-KK funding scheme

Understanding the atmospheric parameters of stars on the top of the RGB is essential to reveal the chemical composition of the Milky Way, as they can be used to probe the farthest parts of our Galaxy. Our goal is to determine the chemical composition of 21 RGB stars with $T_{\mathrm{eff}}<4200$K selected from the APOGEE-2 DR17 database using new observations carried out with the spectrograph mounted on the 1-m telescope of the Hungarian Piszk\'estet\H{o} Observatory and the SONG spectrograph (R=77000) on the Hertzsprung SONG telescope in the 4500$-$5800\r{A} wavelength range. This is the first time the spectrograph (R=18000) on the 1-m telescope at Piszk\'estet\H{o} Observatory was used to measure the abundances of stars. We created a new LTE spectral library using MARCS model atmospheres and SYNSPEC by including the line list of 23 molecules to determine atmospheric parameters ($T_{\mathrm{eff}}$, $\log g$, [Fe/H], [$\alpha$/Fe]) and abundances of Si, Ca, Ti, V, Cr, Mn, and Ni with FERRE. The resulting parameters were compared to that of APOGEE. We found a good agreement in general, the average difference is $-$11.2K in $T_{\mathrm{eff}}$, 0.11dex in $\log g$, 0.10dex in [Fe/H], and $-$0.01dex in [$\alpha$/Fe]. Our analysis successfully demonstrates the ability of the spectrograph at Piszk\'estet\H{o} Observatory to reliably measure the abundance of bright stars., Comment: Accepted for publication in PASP, 18 pages, 6 figures

Here, the entanglement entropy is calculated at the quantum multicritical point of the random transverse-field Ising model (RTIM). We use an efficient implementation of the strong disorder renormalization group method in two and three dimensions for two types of disorder. For cubic subsystems we find a universal logarithmic corner contribution to the area law b*ln(l) that is independent of the form of disorder. Our results agree qualitatively with those at the quantum critical points of the RTIM, but with new b prefactors due to having both geometric and quantum fluctuations at play. By studying the vicinity of the multicritical point, we demonstrate that the corner contribution serves as an `entanglement susceptibility', a useful tool to locate the phase transition and to measure the correlation length critical exponents., Comment: 6 pages, 4 figures, 1 table

With the wealth of medical image data, efficient curation is essential. Assigning the sequence type to magnetic resonance images is necessary for scientific studies and artificial intelligence-based analysis. However, incomplete or missing metadata prevents effective automation. We therefore propose a deep-learning method for classification of prostate cancer scanning sequences based on a combination of image data and DICOM metadata. We demonstrate superior results compared to metadata or image data alone, and make our code publicly available at https://github.com/deepakri201/DICOMScanClassification.

Accurately segmenting thin tubular structures, such as vessels, nerves, roads or concrete cracks, is a crucial task in computer vision. Standard deep learning-based segmentation loss functions, such as Dice or Cross-Entropy, focus on volumetric overlap, often at the expense of preserving structural connectivity or topology. This can lead to segmentation errors that adversely affect downstream tasks, including flow calculation, navigation, and structural inspection. Although current topology-focused losses mark an improvement, they introduce significant computational and memory overheads. This is particularly relevant for 3D data, rendering these losses infeasible for larger volumes as well as increasingly important multi-class segmentation problems. To mitigate this, we propose a novel Skeleton Recall Loss, which effectively addresses these challenges by circumventing intensive GPU-based calculations with inexpensive CPU operations. It demonstrates overall superior performance to current state-of-the-art approaches on five public datasets for topology-preserving segmentation, while substantially reducing computational overheads by more than 90%. In doing so, we introduce the first multi-class capable loss function for thin structure segmentation, excelling in both efficiency and efficacy for topology-preservation., Comment: Accepted at ECCV 2024

Building large-scale quantum communication networks has its unique challenges. Here, we demonstrate that a network-wide synergistic usage of quantum memories distributed in a quantum communication network offers a fundamental advantage. We first map the problem of quantum communication with local usage of memories into a classical continuum percolation model. Then, we show that this mapping can be improved through a cooperation of entanglement distillation and relay protocols via remote access to distributed memories. This improved mapping, which we term $\alpha$-percolation, can be formulated in terms of graph-merging rules, analogous to the decimation rules of the renormalization group treatment of disordered quantum magnets. These rules can be performed in any order, yielding the same optimal result, which is characterized by the emergence of a ``positive feedback'' mechanism and the formation of spatially disconnected ``hopping'' communication components -- both marking significant improvements in quantum network connectivity., Comment: 6 pages, 3 figures

While supermassive black holes (BHs) are widely observed in the nearby and distant universe, their origin remains debated with two viable formation scenarios with light and heavy seeds. In the light seeding model, the first BHs form from the collapse of massive stars with masses of $10-100 \ \rm{M_{\odot}}$, while the heavy seeding model posits the formation of $10^{4-5} \ \rm{M_{\odot}}$ seeds from direct collapse. The detection of BHs at redshifts $z\gtrsim10$, edging closer to their formation epoch, provides critical observational discrimination between these scenarios. Here, we focus on the JWST-detected galaxy, GHZ 9, at $z\approx10$ that is lensed by the foreground cluster, Abell 2744. Based on 2.1 Ms deep Chandra observations, we detect a candidate X-ray AGN, which is spatially coincident with the high-redshift galaxy, GHZ 9. The BH candidate is inferred to have a bolometric luminosity of $(1.0^{+0.5}_{-0.4})\times10^{46} \ \rm{erg \ s^{-1}}$, which corresponds to a BH mass of $(8.0^{+3.7}_{-3.2})\times10^7 \ \rm{M_{\odot}}$ assuming Eddington-limited accretion. This extreme mass at such an early cosmic epoch suggests the heavy seed origin for this BH candidate. Based on the Chandra and JWST discoveries of extremely high-redshift quasars, we have constructed the first simple AGN luminosity function extending to $z\approx10$. Comparison of this luminosity function with theoretical models indicates an over-abundant $z\approx10$ BH population, consistent with a higher-than-expected seed formation efficiency., Comment: 9 pages, 4 figures, accepted for publication in The Astrophysical Journal Letters

One of the hot topics in machine learning is the field of GNN. The complexity of graph data has imposed significant challenges on existing machine learning algorithms. Recently, many studies on extending deep learning approaches for graph data have emerged. This paper represents a survey, providing a comprehensive overview of Graph Neural Networks (GNNs). We discuss the applications of graph neural networks across various domains. Finally, we present an advanced field in GNNs: graph generation.

We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate's input format and its various components, modes, and output. CheckMate is evaluated on 15 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

Mesh texture synthesis is a key component in the automatic generation of 3D content. Existing learning-based methods have drawbacks -- either by disregarding the shape manifold during texture generation or by requiring a large number of different views to mitigate occlusion-related inconsistencies. In this paper, we present a novel surface-aware approach for mesh texture synthesis that overcomes these drawbacks by leveraging the pre-trained weights of 2D Convolutional Neural Networks (CNNs) with the same architecture, but with convolutions designed for 3D meshes. Our proposed network keeps track of the oriented patches surrounding each texel, enabling seamless texture synthesis and retaining local similarity to classical 2D convolutions with square kernels. Our approach allows us to synthesize textures that account for the geometric content of mesh surfaces, eliminating discontinuities and achieving comparable quality to 2D image synthesis algorithms. We compare our approach with state-of-the-art methods where, through qualitative and quantitative evaluations, we demonstrate that our approach is more effective for a variety of meshes and styles, while also producing visually appealing and consistent textures on meshes.

The exchange bias phenomenon, inherent in exchange-coupled ferromagnetic and antiferromagnetic systems, has intrigued researchers for decades. Van der Waals materials, with their layered structure, provide an optimal platform for probing such physical phenomena. However, achieving a facile and effective means to manipulate exchange bias in pristine van der Waals heterostructures remains challenging. In this study, we investigate the origin of exchange bias in MnPS3/Fe3GeTe2 van der Waals heterostructures. Our work demonstrates a method to modulate unidirectional exchange anisotropy, achieving an unprecedented nearly 1000% variation through simple thermal cycling. Despite the compensated interfacial spin configuration of MnPS3, magneto-transport measurements reveal a huge 170 mT exchange bias at 5 K, the largest observed in pristine van der Waals antiferromagnet-ferromagnet interfaces. This substantial magnitude of the exchange bias is linked to an anomalous weak ferromagnetic ordering in MnPS3 below 40 K. On the other hand, the tunability of exchange bias during thermal cycling is ascribed to the modified arrangement of interfacial atoms and changes in the vdW gap during field cooling. Our findings highlight a robust and easily adjustable exchange bias in van der Waals antiferromagnetic/ferromagnetic heterostructures, presenting a straightforward approach to enhance other interface related spintronic phenomena for practical applications.

We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort.

This contribution presents the recent research developments within the Cosmic Ray Extremely Distributed Observatory (CREDO) in the search for resolution of various scientific puzzles, ranging from fundamental physical questions to applications like the determination of earthquake precursors. The state-of-the art theoretical, numerical and computational aspects of these phenomena are addressed, as well as recent experimental developments for detection., Comment: 9 pages, 7 figures. Based on the contribution to the XVIII Mexican Workshop on Particles and Fields in Puebla, Mexico, November 2022. M\'exico

Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors., Comment: 23 pages; this is an extended version of the published paper

Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of first-order theorem proving. We describe our induction inference rules proving properties with inductively defined datatypes and integers. We also present additional reasoning heuristics for strengthening inductive reasoning, as well as for using induction hypotheses and recursive function definitions for guiding induction. We present exhaustive experimental results demonstrating the practical impact of our approach as implemented within Vampire. This is an extended version of a Principles of Systems Design 2022 paper with the same title and the same authors., Comment: 26 pages; this is an extended version of the published paper

This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2's frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.

Graph embeddings learn the structure of networks and represent it in low-dimensional vector spaces. Community structure is one of the features that are recognized and reproduced by embeddings. We show that an iterative procedure, in which a graph is repeatedly embedded and its links are reweighted based on the geometric proximity between the nodes, reinforces intra-community links and weakens inter-community links, making the clusters of the initial network more visible and more easily detectable. The geometric separation between the communities can become so strong that even a very simple parsing of the links may recover the communities as isolated components with surprisingly high precision. Furthermore, when used as a pre-processing step, our embedding and reweighting procedure can improve the performance of traditional community detection algorithms., Comment: 41 pages, 20 figures

We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour of matrices, as we show that tree-like calculi have a number of drawbacks in the context of satisfiability solving. The matrix setting permits numerous global refinements of the basic connection calculus. We also show that a suitably-refined calculus is a decision procedure for the Bernays-Sch\"onfinkel class.

Generative modelling aims to accelerate the discovery of novel chemicals by directly proposing structures with desirable properties. Recently, score-based, or diffusion, generative models have significantly outperformed previous approaches. Key to their success is the close relationship between the score and physical force, allowing the use of powerful equivariant neural networks. However, the behaviour of the learnt score is not yet well understood. Here, we analyse the score by training an energy-based diffusion model for molecular generation. We find that during the generation the score resembles a restorative potential initially and a quantum-mechanical force at the end. In between the two endpoints, it exhibits special properties that enable the building of large molecules. Using insights from the trained model, we present Similarity-based Molecular Generation (SiMGen), a new method for zero shot molecular generation. SiMGen combines a time-dependent similarity kernel with descriptors from a pretrained machine learning force field to generate molecules without any further training. Our approach allows full control over the molecular shape through point cloud priors and supports conditional generation. We also release an interactive web tool that allows users to generate structures with SiMGen online (https://zndraw.icp.uni-stuttgart.de).

In this paper we develop a Neumann-Neumann type domain decomposition method for elliptic problems on metric graphs. We describe the iteration in the continuous and discrete setting and rewrite the latter as a preconditioner for the Schur complement system. Then we formulate the discrete iteration as an abstract additive Schwarz iteration and prove that it convergences to the finite element solution with a rate that is independent of the finite element mesh size. We show that the condition number of the Schur complement is also independent of the finite element mesh size. We provide an implementation and test it on various examples of interest and compare it to other preconditioners.

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover Vampire, and show that it is noticeably faster than the state of the art.