Search

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.

K-fold cross-validation is a widely used tool for assessing classifier performance. The reproducibility crisis faced by artificial intelligence partly results from the irreproducibility of reported k-fold cross-validation-based performance scores. Recently, we introduced numerical techniques to test the consistency of claimed performance scores and experimental setups. In a crucial use case, the method relies on the combinatorial enumeration of all k-fold configurations, for which we proposed an algorithm in the binary classification case.

We give an example of automated geometry reasoning for an imaginary classroom project by using the free software package GeoGebra Discovery. The project is motivated by a publicly available toy, a rocking camel, installed at a medical center in Upper Austria. We explain how the process of a false conjecture, experimenting, modeling, a precise mathematical setup, and then a proof by automated reasoning could help extend mathematical knowledge at secondary school level and above., Comment: In Proceedings ADG 2023, arXiv:2401.10725

We address, through the automated reasoning tools in GeoGebra Discovery, a problem from a regional phase of the Austrian Mathematics Olympiad 2023. Trying to solve this problem gives rise to four different kind of feedback: the almost instantaneous, automated solution of the proposed problem; the measure of its complexity, according to some recent proposals; the automated discovery of a generalization of the given assertion, showing that the same statement is true over more general polygons than those mentioned in the problem; and the difficulties associated to the analysis of the surprising and involved high number of degenerate cases that appear when using the LocusEquation command in this problem. In our communication we will describe and reflect on these diverse issues, enhancing its exemplar role for showing some of the advantages, problems, and current fields of development of GeoGebra Discovery., Comment: In Proceedings ADG 2023, arXiv:2401.10725

In our contribution we describe some on-going improvements concerning the Automated Reasoning Tools developed in GeoGebra Discovery, providing different examples of the performance of these new features. We describe the new ShowProof command, that outputs both the sequence of the different steps performed by GeoGebra Discovery to confirm a certain statement, as well as a number intending to grade the difficulty or interest of the assertion. The proposal of this assessment measure, involving the comparison of the expression of the thesis (or conclusion) as a combination of the hypotheses, will be developed., Comment: In Proceedings ADG 2023, arXiv:2401.10725

We consider a so-called quantum graph with standard continuity and Kirchhoff vertex conditions where the Kirchhoff vertex condition is perturbed by Gaussian noise. We show that the quantum graph setting is very different from the classical one dimensional boundary noise setting, where the transition semigroup is known to be strong Feller, by giving examples and counterexamples to the strong Feller property. In particular, when the graph is a tree, and there is noise present in all but one of the terminal vertices, then the transition semigroup associated with the problem is strong Feller at any time $T>0$. This turns out to be also a necessary condition for equilateral star graphs. We also comment on the existence and uniqueness of the invariant measure and the regularity of the solution., Comment: The proof of Theorem 4.4 was not correct. We substantially revised the manuscript and extended our original results to hold in an even more general setting on metric trees

The well known JGEX program became open source a few years ago, but seemingly, further development of the program can only be done without the original authors. In our project, we are looking at whether it is possible to continue such a large project as a newcomer without the involvement of the original authors. Is there a way to internationalize, fix bugs, improve the code base, add new features? In other words, to save a relic found in the attic and polish it into a useful everyday tool., Comment: In Proceedings ADG 2023, arXiv:2401.10725

We give an insight into Java Geometry Expert (JGEX) in use in a school context, focusing on the Austrian school system. JGEX can offer great support in some classroom situations, especially for solving mathematical competition tasks. Also, we discuss some limitations of the program., Comment: In Proceedings ADG 2023, arXiv:2401.10725

In this article, we solve some of the geometry problems of the N\'aboj 2023 competition with the help of a computer, using examples that the software tool GeoGebra Discovery can calculate. In each case, the calculation requires symbolic computations. We analyze the difficulty of feeding the problem into the machine and set further goals to make the problems of this type of contests even more tractable in the future., Comment: In Proceedings ADG 2023, arXiv:2401.10725

ADG is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. The conference is held every two years. The previous editions of ADG were held in Hagenberg in 2021 (online, postponed from 2020 due to COVID-19), Nanning in 2018, Strasbourg in 2016, Coimbra in 2014, Edinburgh in 2012, Munich in 2010, Shanghai in 2008, Pontevedra in 2006, Gainesville in 2004, Hagenberg in 2002, Zurich in 2000, Beijing in 1998, and Toulouse in 1996. The 14th edition, ADG 2023, was held in Belgrade, Serbia, in September 20-22, 2023. This edition of ADG had an additional special focus topic, Deduction in Education. Invited Speakers: Julien Narboux, University of Strasbourg, France "Formalisation, arithmetization and automatisation of geometry"; Filip Mari\'c, University of Belgrade, Serbia, "Automatization, formalization and visualization of hyperbolic geometry"; Zlatan Magajna, University of Ljubljana, Slovenia, "Workshop OK Geometry"

We study the effect of isospin-symmetry breaking in the framework of the extended Linear Sigma Model (eLSM) in vacuum. In this model, several particles mix with each other at tree level, due to the three non-zero scalar condensates (non-strange, strange, isospin). We resolve these mixings with the help of various field transformations. We compute all possible meson mixings and decay widths at tree level and perform a $\chi^2$ fit to PDG data. A very good fit is found if we exclude the (very small $\sim 130$~keV) $\omega\to \pi\pi$ decay. We also investigate the violation of Dashen's theorem., Comment: 32 pages, 1 figure

We present the full Hubble diagram of photometrically-classified Type Ia supernovae (SNe Ia) from the Dark Energy Survey supernova program (DES-SN). DES-SN discovered more than 20,000 SN candidates and obtained spectroscopic redshifts of 7,000 host galaxies. Based on the light-curve quality, we select 1635 photometrically-identified SNe Ia with spectroscopic redshift 0.10$< z <$1.13, which is the largest sample of supernovae from any single survey and increases the number of known $z>0.5$ supernovae by a factor of five. In a companion paper, we present cosmological results of the DES-SN sample combined with 194 spectroscopically-classified SNe Ia at low redshift as an anchor for cosmological fits. Here we present extensive modeling of this combined sample and validate the entire analysis pipeline used to derive distances. We show that the statistical and systematic uncertainties on cosmological parameters are $\sigma_{\Omega_M,{\rm stat+sys}}^{\Lambda{\rm CDM}}=$0.017 in a flat $\Lambda$CDM model, and $(\sigma_{\Omega_M},\sigma_w)_{\rm stat+sys}^{w{\rm CDM}}=$(0.082, 0.152) in a flat $w$CDM model. Combining the DES SN data with the highly complementary CMB measurements by Planck Collaboration (2020) reduces uncertainties on cosmological parameters by a factor of 4. In all cases, statistical uncertainties dominate over systematics. We show that uncertainties due to photometric classification make up less than 10% of the total systematic uncertainty budget. This result sets the stage for the next generation of SN cosmology surveys such as the Vera C. Rubin Observatory's Legacy Survey of Space and Time., Comment: 39 pages, 19 figures; Submitted to ApJ; companion paper Dark Energy Collaboration et al. on consecutive arxiv number 2401.02929

We present cosmological constraints from the sample of Type Ia supernovae (SN Ia) discovered during the full five years of the Dark Energy Survey (DES) Supernova Program. In contrast to most previous cosmological samples, in which SN are classified based on their spectra, we classify the DES SNe using a machine learning algorithm applied to their light curves in four photometric bands. Spectroscopic redshifts are acquired from a dedicated follow-up survey of the host galaxies. After accounting for the likelihood of each SN being a SN Ia, we find 1635 DES SNe in the redshift range $0.100.5$ SNe compared to the previous leading compilation of Pantheon+, and results in the tightest cosmological constraints achieved by any SN data set to date. To derive cosmological constraints we combine the DES supernova data with a high-quality external low-redshift sample consisting of 194 SNe Ia spanning $0.025

Machine-learned force fields have transformed the atomistic modelling of materials by enabling simulations of ab initio quality on unprecedented time and length scales. However, they are currently limited by: (i) the significant computational and human effort that must go into development and validation of potentials for each particular system of interest; and (ii) a general lack of transferability from one chemical system to the next. Here, using the state-of-the-art MACE architecture we introduce a single general-purpose ML model, trained on a public database of 150k inorganic crystals, that is capable of running stable molecular dynamics on molecules and materials. We demonstrate the power of the MACE-MP-0 model - and its qualitative and at times quantitative accuracy - on a diverse set problems in the physical sciences, including the properties of solids, liquids, gases, chemical reactions, interfaces and even the dynamics of a small protein. The model can be applied out of the box and as a starting or "foundation model" for any atomistic system of interest and is thus a step towards democratising the revolution of ML force fields by lowering the barriers to entry., Comment: 119 pages, 63 figures, 37MB PDF

Recent findings show that single, non-neuronal cells are also able to learn signalling responses developing cellular memory. In cellular learning nodes of signalling networks strengthen their interactions e.g. by the conformational memory of intrinsically disordered proteins, protein translocation, miRNAs, lncRNAs, chromatin memory and signalling cascades. This can be described by a generalized, unicellular Hebbian learning process, where those signalling connections, which participate in learning, become stronger. Here we review those scenarios, where cellular signalling is not only repeated in a few times (when learning occurs), but becomes too frequent, too large, or too complex and overloads the cell. This leads to desensitisation of signalling networks by decoupling signalling components, receptor internalization, and consequent downregulation. These molecular processes are examples of anti-Hebbian learning and forgetting of signalling networks. Stress can be perceived as signalling overload inducing the desensitisation of signalling pathways. Aging occurs by the summative effects of cumulative stress downregulating signalling. We propose that cellular learning desensitisation, stress and aging may be placed along the same axis of more and more intensive (prolonged or repeated) signalling. We discuss how cells might discriminate between repeated and unexpected signals, and highlight the Hebbian and anti-Hebbian mechanisms behind the fold-change detection in the NF-\k{appa}B signalling pathway. We list drug design methods using Hebbian learning (such as chemically-induced proximity) and clinical treatment modalities inducing (cancer, drug allergies) desensitisation or avoiding drug-induced desensitisation. A better discrimination between cellular learning, desensitisation and stress may open novel directions in drug design, e.g., helping to overcome drug-resistance., Comment: 19 pages, 4 figures

Classical empirical force fields have dominated biomolecular simulation for over 50 years. Although widely used in drug discovery, crystal structure prediction, and biomolecular dynamics, they generally lack the accuracy and transferability required for predictive modelling. In this paper, we introduce MACE-OFF23, a transferable force field for organic molecules created using state-of-the-art machine learning technology and first-principles reference data computed with a high level of quantum mechanical theory. MACE-OFF23 demonstrates the remarkable capabilities of local, short-range models by accurately predicting a wide variety of gas and condensed phase properties of molecular systems. It produces accurate, easy-to-converge dihedral torsion scans of unseen molecules, as well as reliable descriptions of molecular crystals and liquids, including quantum nuclear effects. We further demonstrate the capabilities of MACE-OFF23 by determining free energy surfaces in explicit solvent, as well as the folding dynamics of peptides. Finally, we simulate a fully solvated small protein, observing accurate secondary structure and vibrational spectrum. These developments enable first-principles simulations of molecular systems for the broader chemistry community at high accuracy and low computational cost.

Decision tree and random forest classification and regression are some of the most widely used in machine learning approaches. Binary decision tree implementations commonly use conditioning in the form 'feature $\leq$ (or $<$) threshold', with the threshold being the midpoint between two observed feature values. In this paper, we investigate the bias introduced by the choice of conditioning operator (an intrinsic property of implementations) in the presence of features with lattice characteristics. We propose techniques to eliminate this bias, requiring an additional prediction with decision trees and incurring no cost for random forests. Using 20 classification and 20 regression datasets, we demonstrate that the bias can lead to statistically significant differences in terms of AUC and $r^2$ scores. The proposed techniques successfully mitigate the bias, compared to the worst-case scenario, statistically significant improvements of up to 0.1-0.2 percentage points of AUC and $r^2$ scores were achieved and the improvement of 1.5 percentage points of $r^2$ score was measured in the most sensitive case of random forest regression. The implementation of the study is available on GitHub at the following repository: \url{https://github.com/gykovacs/conditioning_bias}.

The layered van der Waals material ZrTe$_5$ is known as a candidate topological insulator (TI), however its topological phase and the relation with other properties such as an apparent Dirac semimetallic state is still a subject of debate. We employ a semiclassical multicarrier transport (MCT) model to analyze the magnetotransport of ZrTe$_5$ nanodevices at hydrostatic pressures up to 2 GPa. The temperature dependence of the MCT results between 10 and 300 K is assessed in the context of thermal activation, and we obtain the positions of conduction and valence band edges in the vicinity of the chemical potential. We find evidence of the closing and re-opening of the band gap with increasing pressure, which is consistent with a phase transition from weak to strong TI. This matches expectations from ab initio band structure calculations, as well as previous observations that CVT-grown ZrTe$_5$ is a weak TI in ambient conditions., Comment: Main Text: 11 pages, 5 figures; Supporting Information: 13 pages, 9 figures