@inproceedings{21327, abstract = {Proteins exist as a dynamic ensemble of multiple conformations, and these motions are often crucial for their functions. However, current structure prediction methods predominantly yield a single conformation, overlooking the conformational heterogeneity revealed by diverse experimental modalities. Here, we present a framework for building experiment-grounded protein structure generative models that infer conformational ensembles consistent with measured experimental data. The key idea is to treat stateof-the-art protein structure predictors (e.g., AlphaFold3) as sequence-conditioned structural priors, and cast ensemble modeling as posterior inference of protein structures given experimental measurements. Through extensive real-data experiments, we demonstrate the generality of our method to incorporate a variety of experimental measurements. In particular, our framework uncovers previously unmodeled conformational heterogeneity from crystallographic densities, and generates high-accuracy NMR ensembles orders of magnitude faster than the status quo. Notably, we demonstrate that our ensembles outperform AlphaFold3 (Abramson et al., 2024) and sometimes better fit experimental data than publicly deposited structures to the Protein Data Bank (PDB, Burley et al. (2017)). We believe that this approach will unlock building predictive models that fully embrace experimentally observed conformational diversity.}, author = {Maddipatla, Sai A and Sellam, Nadav E and Bojan, Meital I and Vedula, Sanketh and Schanda, Paul and Marx, Ailie and Bronstein, Alexander}, booktitle = {Proceedings of the 42nd International Conference on Machine Learning}, issn = {2640-3498}, location = {Vancouver, Canada}, pages = {42366 -- 42393}, publisher = {ML Research Press}, title = {{Inverse problems with experiment-guided AlphaFold}}, volume = {267}, year = {2025}, } @inproceedings{21328, abstract = {Multi-index models provide a popular framework to investigate the learnability of functions with low-dimensional structure and, also due to their connections with neural networks, they have been object of recent intensive study. In this paper, we focus on recovering the subspace spanned by the signals via spectral estimators – a family of methods routinely used in practice, often as a warm-start for iterative algorithms. Our main technical contribution is a precise asymptotic characterization of the performance of spectral methods, when sample size and input dimension grow proportionally and the dimension p of the space to recover is fixed. Specifically, we locate the top-p eigenvalues of the spectral matrix and establish the overlaps between the corresponding eigenvectors (which give the spectral estimators) and a basis of the signal subspace. Our analysis unveils a phase transition phenomenon in which, as the sample complexity grows, eigenvalues escape from the bulk of the spectrum and, when that happens, eigenvectors recover directions of the desired subspace. The precise characterization we put forward enables the optimization of the data preprocessing, thus allowing to identify the spectral estimator that requires the minimal sample size for weak recovery.}, author = {Kovačević, Filip and Yihan, Zhang and Mondelli, Marco}, booktitle = {Proceedings of 38th Conference on Learning Theory}, issn = {2640-3498}, location = {Lyon, France}, pages = {3354--3404}, publisher = {ML Research Press}, title = {{Spectral estimators for multi-index models: Precise asymptotics and optimal weak recovery}}, volume = {291}, year = {2025}, } @article{21343, abstract = {The large sieve is used to estimate the density of quadratic polynomials Q ∈ Z[x], such that there exists an odd degree polynomial defined over Z which has resultant ±1 with Q. Given a monic polynomial R ∈ Z[x] of odd degree, this is used to show that for almost all quadratic polynomials Q ∈ Z[x], there exists a prime p such that Q and R share a common root in Fp. Using recent work of Landesman, an application to the average size of the odd part of the class group of quadratic number fields is also given}, author = {Browning, Timothy D and Chan, Yik Tung}, issn = {2270-518X}, journal = {Journal de l'ecole polytechnique mathematiques}, pages = {1677--1691}, publisher = {Ecole polytechnique}, title = {{Solubility of a resultant equation and applications}}, doi = {10.5802/jep.320}, volume = {12}, year = {2025}, } @unpublished{21399, abstract = {We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.}, author = {Bolan, Matthew and Breitner, Joachim and Brox, Jose and Carlini, Nicholas and Carneiro, Mario and Doorn, Floris van and Dvorak, Martin and Goens, Andrés and Hill, Aaron and Husum, Harald and Mejia, Hernán Ibarra and Kocsis, Zoltan A. and Floch, Bruno Le and Bar-on, Amir and Luccioli, Lorenzo and McNeil, Douglas and Meiburg, Alex and Monticone, Pietro and Nielsen, Pace P. and Osazuwa, Emmanuel Osalotioman and Paolini, Giovanni and Petracci, Marco and Reinke, Bernhard and Renshaw, David and Rossel, Marcus and Roux, Cody and Scanvic, Jérémy and Srinivas, Shreyas and Tadipatri, Anand Rao and Tao, Terence and Tsyrklevich, Vlad and Vaquerizo-Villar, Fernando and Weber, Daniel and Zheng, Fan}, booktitle = {arXiv}, title = {{The equational theories project: Advancing collaborative mathematical research at scale}}, doi = {10.48550/arXiv.2512.07087}, year = {2025}, } @inproceedings{21412, abstract = {Payment channel networks (PCNs) are a promising technology that alleviates blockchain scalability by shifting the transaction load from the blockchain to the PCN. Nevertheless, the network topology has to be carefully designed to maximise the transaction throughput in PCNs. Additionally, users in PCNs also have to make optimal decisions on which transactions to forward and which to reject to prolong the lifetime of their channels. In this work, we consider an input sequence of transactions over p parties. Each transaction consists of a transaction size, source, and target, and can be either accepted or rejected (entailing a cost). The goal is to design a PCN topology among the p cooperating parties, along with the channel capacities, and then output a decision for each transaction in the sequence to minimise the cost of creating and augmenting channels, as well as the cost of rejecting transactions. Our main contribution is an 𝒪(p) approximation algorithm for the problem with p parties. We further show that with some assumptions on the distribution of transactions, we can reduce the approximation ratio to 𝒪(√p). We complement our theoretical analysis with an empirical study of our assumptions and approach in the context of the Lightning Network.}, author = {Chatterjee, Krishnendu and Křišťan, Jan Matyáš and Schmid, Stefan and Svoboda, Jakub and Yeo, Michelle X}, booktitle = {39th International Symposium on Distributed Computing}, isbn = {9783959774024}, issn = {1868-8969}, location = {Berlin, Germany}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Boosting payment channel network liquidity with topology optimization and transaction selection}}, doi = {10.4230/LIPIcs.DISC.2025.23}, volume = {356}, year = {2025}, } @article{21413, abstract = {We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelik, Martin and Forejt, Vojtěch and Kretinsky, Jan and Kwiatkowska, Marta and Meggendorfer, Tobias and Parker, David and Ujma, Mateusz}, issn = {2751-4838}, journal = {TheoretiCS}, publisher = {TheoretiCS Foundation}, title = {{Learning algorithms for verification of Markov decision processes}}, doi = {10.46298/theoretics.25.10}, volume = {4}, year = {2025}, } @article{17094, abstract = {Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory designed to ensure system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. Additionally, we introduce information-flow contracts where assumptions and guarantees are sets of flow relations. We use these contracts to illustrate how to enrich information-flow interfaces with a semantic view. We illustrate the applicability of our framework with two examples inspired by the automotive domain.}, author = {Bartocci, Ezio and Ferrere, Thomas and Henzinger, Thomas A and Nickovic, Dejan and Oliveira da Costa, Ana}, issn = {1572-8102}, journal = {Formal Methods in System Design}, pages = {3--48}, publisher = {Springer Nature}, title = {{Information-flow interfaces}}, doi = {10.1007/s10703-024-00447-0}, volume = {66}, year = {2025}, } @article{17149, abstract = {The approximation of a circle with the edges of a fine square grid distorts the perimeter by a factor about 4/Pi. We prove that this factor is the same on average (in the ergodic sense) for approximations of any rectifiable curve by the edges of any non-exotic Delaunay mosaic (known as Voronoi path), and extend the results to all dimensions, generalizing Voronoi paths to Voronoi scapes.}, author = {Edelsbrunner, Herbert and Nikitenko, Anton}, issn = {1432-0444}, journal = {Discrete & Computational Geometry}, pages = {490--499}, publisher = {Springer Nature}, title = {{Average and expected distortion of Voronoi paths and scapes}}, doi = {10.1007/s00454-024-00660-y}, volume = {73}, year = {2025}, } @article{17293, abstract = {Voltage-gated CaV2.1 (P/Q-type) Ca2+ channels play a crucial role in regulating neurotransmitter release, thus contributing to synaptic plasticity and to processes such as learning and memory. Despite their recognized importance in neural function, there is limited information on their potential involvement in neurodegenerative conditions such as Alzheimer's disease (AD). Here, we aimed to explore the impact of AD pathology on the density and nanoscale compartmentalization of CaV2.1 channels in the hippocampus in association with GABAB receptors. Histoblotting experiments showed that the density of CaV2.1 channel was significantly reduced in the hippocampus of APP/PS1 mice in a laminar-dependent manner. CaV2.1 channel was enriched in the active zone of the axon terminals and was present at a very low density over the surface of dendritic tree of the CA1 pyramidal cells, as shown by quantitative SDS-digested freeze-fracture replica labelling (SDS-FRL). In APP/PS1 mice, the density of CaV2.1 channel in the active zone was significantly reduced in the strata radiatum and lacunosum-moleculare, while it remained unaltered in the stratum oriens. The decline in Cav2.1 channel density was found to be associated with a corresponding impairment in the GABAergic synaptic function, as evidenced by electrophysiological experiments carried out in the hippocampus of APP/PS1 mice. Remarkably, double SDS-FRL showed a co-clustering of CaV2.1 channel and GABAB1 receptor in nanodomains (~40–50 nm) in wild type mice, while in APP/PS1 mice this nanoarchitecture was absent. Together, these findings suggest that the AD pathology-induced reduction in CaV2.1 channel density and CaV2.1-GABAB1 de-clustering may play a role in the synaptic transmission alterations shown in the AD hippocampus. Therefore, uncovering these layer-dependent changes in P/Q calcium currents associated with AD pathology can benefit the development of future strategies for AD management.}, author = {Martín‐Belmonte, Alejandro and Aguado, Carolina and Alfaro‐Ruiz, Rocío and Kulik, Akos and de la Ossa, Luis and Moreno‐Martínez, Ana Esther and Alberquilla, Samuel and García‐Carracedo, Lucía and Fernández, Miriam and Fajardo‐Serrano, Ana and Aso, Ester and Shigemoto, Ryuichi and Martín, Eduardo D. and Fukazawa, Yugo and Ciruela, Francisco and Luján, Rafael}, issn = {1750-3639}, journal = {Brain Pathology}, number = {2}, publisher = {Wiley}, title = {{Nanoarchitecture of CaV>2.1 channels and GABAB receptors in the mouse hippocampus: Impact of APP/PS1 pathology}}, doi = {10.1111/bpa.13279}, volume = {35}, year = {2025}, } @article{17459, abstract = {Atopic dermatitis (AD) is the most common chronic inflammatory skin disease worldwide. AD is a highly complex disease with different subtypes. Many elements of AD pathophysiology have been described, but if/how they interact with each other or which mechanisms are important in which patients is still unclear. Langerhans cells (LCs) are antigen-presenting cells (APCs) in the epidermis. Depending on the context, they can act either pro- or anti-inflammatory. Many different studies have investigated LCs in the context of AD and found them to be connected to all major mechanisms of AD pathophysiology. As APCs, LCs recruit other immune cells and shape the immune response, especially adaptive immunity via polarization of T cells. As sentinel cells, LCs are primary sensors of the skin microbiome and are important for the decision of immunity versus tolerance. LCs are also involved with the integrity of the skin barrier by influencing tight junctions. Finally, LCs are important cells in the neuro-immune crosstalk in the skin. In this review, we provide an overview about the many different roles of LCs in AD. Understanding LCs might bring us closer to a more complete understanding of this highly complex disease. Potentially, modulating LCs might offer new options for targeted therapies for AD patients.}, author = {Pan, Yi and Hochgerner, Mathias and Cichon, Malgorzata Anna and Benezeder, Theresa and Bieber, Thomas and Wolf, Peter}, issn = {1468-3083}, journal = {Journal of the European Academy of Dermatology and Venereology}, number = {2}, pages = {278--289}, publisher = {Wiley}, title = {{Langerhans cells: Central players in the pathophysiology of atopic dermatitis}}, doi = {10.1111/jdv.20291}, volume = {39}, year = {2025}, } @article{8616, abstract = {The brain vasculature supplies neurons with glucose and oxygen, but little is known about how vascular plasticity contributes to brain function. Using longitudinal in vivo imaging, we report that a substantial proportion of blood vessels in the adult mouse brain sporadically occlude and regress. Their regression proceeds through sequential stages of blood-flow occlusion, endothelial cell collapse, relocation or loss of pericytes, and retraction of glial endfeet. Regressing vessels are found to be widespread in mouse, monkey and human brains. We further reveal that blood vessel regression cause a reduction of neuronal activity due to a dysfunction in mitochondrial metabolism and glutamate production. Our results elucidate the mechanism of vessel regression and its role in neuronal function in the adult brain.}, author = {Gao, Xiaofei and Li, Jun-Liszt and Chen, Xingjun and Ci, Bo and Chen, Fei and Lu, Nannan and Shen, Bo and Zheng, Lijun and Jia, Jie-Min and Yi, Yating and Zhang, Shiwen and Shi, Ying-Chao and Shi, Kaibin and Propson, Nicholas E and Huang, Yubin and Poinsatte, Katherine and Zhang, Zhaohuan and Yue, Yuanlei and Bosco, Dale B and Lu, Ying-mei and Yang, Shi-bing and Adams, Ralf H. and Lindner, Volkhard and Huang, Fen and Wu, Long-Jun and Zheng, Hui and Han, Feng and Hippenmeyer, Simon and Stowe, Ann M. and Peng, Bo and Margeta, Marta and Wang, Xiaoqun and Liu, Qiang and Körbelin, Jakob and Trepel, Martin and Lu, Hui and Zhou, Bo O. and Zhao, Hu and Su, Wenzhi and Bachoo, Robert M. and Ge, Woo-ping}, issn = {2041-1723}, journal = {Nature Communications}, publisher = {Springer Nature}, title = {{Reduction of neuronal activity mediated by blood-vessel regression in the brain}}, doi = {10.1038/s41467-025-60308-0}, volume = {16}, year = {2025}, } @inproceedings{21020, abstract = {Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification. In this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation. The sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.}, author = {Henzinger, Thomas A and Karimi, Mahyar and Thejaswini, K. S.}, booktitle = {Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security}, isbn = {9798400715259}, location = {Taipei, Taiwan}, pages = {2774--2787}, publisher = {Association for Computing Machinery}, title = {{Privacy-preserving runtime verification}}, doi = {10.1145/3719027.3765137}, year = {2025}, } @unpublished{21435, abstract = {Multiferroic materials, in which electric polarization and magnetic order coexist and couple, offer rich opportunities for both fundamental discovery and technology. However, multiferroicity remains rare due to conflicting electronic requirements for ferroelectricity and magnetism. One route to circumvent this challenge is to exploit the noncollinear ordering of spin cycloids, whose symmetry permits the emergence of polar order. In this work, we introduce another pathway to multiferroic order in which strain generates polarization in materials that host nonpolar spin spirals. To demonstrate this phenomenon, we chose the spin spiral in the well-studied helimagnet Cr1/3NbS2. To detect the induced polarization, we introduce the technique of magnetoelectric birefringence (MEB), an optical probe that enables spatially-resolved and unambiguous detection of polar order. By combining MEB imaging with strain engineering, we confirm the onset of a polar vector at the magnetic transition, establishing strained Cr1/3NbS2 as a type-II multiferroic.}, author = {Sun, Y. and Ahn, Y. and Sapkota, D. and Arachchige, H. S. and Xue, R. and Mozaffari, S. and Mandrus, D. G. and Zhao, L. and Orenstein, J. and Sunko, Veronika}, booktitle = {arXiv}, title = {{Strain-induced multiferroicity in Cr1/3NbS2}}, doi = {10.48550/arXiv.2510.11619}, year = {2025}, } @unpublished{21437, abstract = {Altermagnets are a class of collinear magnets that exhibit non-relativistic spin splitting (NRSS) of electronic bands in the absence of net magnetization. Their potential to generate large spin polarization without spin-orbit coupling has created strong interest in probes that access the underlying order parameter directly. In this Perspective, we show that linear magneto-birefringence (LMB) provides a natural and broadly applicable route to detecting altermagnetic order. Building on the correspondence between the momentum-space structure of NRSS and the ferroic ordering of magnetic multipoles in real space, we demonstrate how $d$-wave and $g$-wave NRSS textures yield distinct LMB responses. We present a symmetry-based framework that identifies the optical geometries and field configurations required to isolate specific multipole components, enabling domain imaging and providing benchmarks for theoretical models of LMB.}, author = {Sunko, Veronika and Orenstein, J.}, booktitle = {arXiv}, title = {{Linear magneto-birefringence as a probe of altermagnetism}}, doi = {10.48550/arXiv.2511.16421}, year = {2025}, } @misc{20842, abstract = {Probing the possibility of entanglement generation through gravity offers a path to tackle the question of whether gravitational fields possess a quantum mechanical nature. A potential realization necessitates systems with low-frequency dynamics at an optimal mass scale, for which the microgram-to-milligram range is a strong contender. Here, after refining a figure-of-merit for the problem, we present a 1-milligram torsional pendulum operating at 18 Hz. We demonstrate laser cooling its motion from room temperature to 240~microkelvins, surpassing by over 20-fold the coldest motions attained for oscillators ranging from micrograms to kilograms. We quantify and contrast the utility of the current approach with other platforms. The achieved performance and large improvement potential highlight milligram-scale torsional pendulums as a powerful platform for precision measurements relevant to future studies at the quantum-gravity interface.}, author = {Agafonova, Sofya}, publisher = {Institute of Science and Technology Austria}, title = {{Research Data for: 'One-milligram torsional pendulum toward experiments at the quantum-gravity interface'}}, doi = {10.15479/AT-ISTA-20842}, year = {2025}, } @article{17884, abstract = {Human T cell leukemia virus type 1 (HTLV-1) immature particles differ in morphology from other retroviruses, suggesting a distinct way of assembly. Here we report the results of cryo-electron tomography studies of HTLV-1 virus-like particles assembled in vitro, as well as derived from cells. This work shows that HTLV-1 uses a distinct mechanism of Gag–Gag interactions to form the immature viral lattice. Analysis of high-resolution structural information from immature capsid (CA) tubular arrays reveals that the primary stabilizing component in HTLV-1 is the N-terminal domain of CA. Mutagenesis analysis supports this observation. This distinguishes HTLV-1 from other retroviruses, in which the stabilization is provided primarily by the C-terminal domain of CA. These results provide structural details of the quaternary arrangement of Gag for an immature deltaretrovirus and this helps explain why HTLV-1 particles are morphologically distinct.}, author = {Obr, Martin and Percipalle, Mathias and Chernikova, Darya and Yang, Huixin and Thader, Andreas and Pinke, Gergely and Porley, Dario J and Mansky, Louis M. and Dick, Robert A. and Schur, Florian KM}, issn = {1545-9985}, journal = {Nature Structural & Molecular Biology}, pages = {268--276}, publisher = {Springer Nature}, title = {{Distinct stabilization of the human T cell leukemia virus type 1 immature Gag lattice}}, doi = {10.1038/s41594-024-01390-8}, volume = {32}, year = {2025}, } @unpublished{21427, abstract = {While tumor malignancy has been extensively studied under the prism of genetic and epigenetic heterogeneity, tumor cell states also critically depend on reciprocal interactions with the microenvironment. This raises the hitherto untested possibility that heterogeneity of the untransformed tumor stroma can actively fuel malignant progression. As biological heterogeneity is inherently difficult to control, we adopted a reductionist approach and let tumor cells invade micro-engineered environments harboring obstacles with precision-controlled geometry. We find that not only the presence of obstacles, but more surprisingly their spatial disorder, causes a drastic shift from a collective to a single-cell mode of invasion – comparable in strength to cadherin loss. Combining live-imaging and perturbation experiments with minimal biophysical modeling, we demonstrate that cell detachments result both from local geometrical constraints and a global integration of spatial disorder over time. We show that different types of microenvironments map onto different universality classes of invasion dynamics - homogeneous substrates follow Kardar–Parisi–Zhang (KPZ) scaling, while disordered ones exhibit exponents consistent with KPZ with quenched disorder (KPZq). Our findings highlight generic physical principles for how the mode of cancer cell invasion depends on environmental heterogeneity, with potential implications to understand tumor evolution in vivo.}, author = {Dunajova, Zuzana and Tasciyan, Saren and Majek, Juraj and Merrin, Jack and Sahai, Erik and Sixt, Michael K and Hannezo, Edouard B}, publisher = {bioRxiv}, title = {{Substrate heterogeneity promotes cancer cell dissemination through interface roughening}}, doi = {10.1101/2025.05.20.655037}, year = {2025}, } @inproceedings{21474, abstract = {Rendering novel, relit views of a human head, given a monocular portrait image as input, is an inherently underconstrained problem. The traditional graphics solution is to explicitly decompose the input image into geometry, material and lighting via differentiable rendering; but this is constrained by the multiple assumptions and approximations of the underlying models and parameterizations of these scene components. We propose 3DPR, an image-based relighting model that leverages generative priors learnt from multi-view One-Light-at-A-Time (OLAT) images captured in a light stage. We introduce a new diverse and large-scale multi-view 4K OLAT dataset of 139 subjects to learn a high-quality prior over the distribution of high-frequency face reflectance. We leverage the latent space of a pre-trained generative head model that provides a rich prior over face geometry learnt from in-the-wild image datasets. The input portrait is first embedded in the latent manifold of such a model through an encoder-based inversion process. Then a novel triplane-based reflectance network trained on our lightstage data is used to synthesize high-fidelity OLAT images to enable image-based relighting. Our reflectance network operates in the latent space of the generative head model, crucially enabling a relatively small number of lightstage images to train the reflectance model. Combining the generated OLATs according to a given HDRI environment maps yields physically accurate environmental relighting results. Through quantitative and qualitative evaluations, we demonstrate that 3DPR outperforms previous methods, particularly in preserving identity and in capturing lighting effects such as specularities, self-shadows, and subsurface scattering.}, author = {Rao, Pramod and Meka, Abhimitra and Zhou, Xilong and Fox, Gereon and Mallikarjun, B. R. and Zhan, Fangneng and Weyrich, Tim and Bickel, Bernd and Pfister, Hanspeter and Matusik, Wojciech and Beeler, Thabo and Elgharib, Mohamed and Habermann, Marc and Theobalt, Christian}, booktitle = {Proceedings SIGGRAPH Asia 2025 Conference Papers 2025}, isbn = {9798400721373}, location = {Hong Kong, Hong Kong}, publisher = {Association for Computing Machinery}, title = {{3DPR: Single image 3D portrait relighting with generative priors}}, doi = {10.1145/3757377.3763962}, year = {2025}, } @unpublished{21398, abstract = {Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges, most importantly that only a limited number of notions and results have been implemented so far. In this work, we formalize the proof of the forward (composition) direction of Seymour's theorem for regular matroids. To this end, we develop a library in Lean 4 that implements definitions and results about totally unimodular matrices, vector matroids, their standard representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary matroids given by their standard representations. Using this framework, we formally state Seymour's decomposition theorem and implement a formally verified proof of the composition direction in the setting where the matroids have finite rank and may have infinite ground sets.}, author = {Dvorak, Martin and Figueroa-Reid, Tristan and Hamadani, Rida and Hwang, Byung-Hak and Karunus, Evgenia and Kolmogorov, Vladimir and Meiburg, Alexander and Nelson, Alexander and Nelson, Peter and Sandey, Mark and Sergeev, Ivan}, booktitle = {arXiv}, pages = {21}, title = {{Composition direction of Seymour's theorem for regular matroids — Formally verified}}, doi = {10.48550/arXiv.2509.20539}, year = {2025}, } @article{20326, abstract = {Ag2Se is a promising n-type thermoelectric material, but its performance is limited by excessive carrier concentration, compositional inhomogeneity, and phase instability, challenges rooted in a narrow homogeneity range and uncontrolled Ag+ diffusion in the superionic phase. Here, we address these issues by exploiting liquid–solid interface reactions using CdSe complexes that remove surface excess Ag to yield stoichiometric Ag2Se and generate CdSe nanodomains that inhibit Ag+ diffusion and constrain grain growth. The resulting Ag2Se-CdSe nanocomposites exhibit a reproducible, stable figure of merit (zT) of 1.04 between 300 and 390 K. Beyond demonstrating high performance, we elucidate the interfacial chemical reactions that give rise to the observed microstructure and transport properties, providing a foundation for rationally engineering interfacial chemistry to tailor transport properties across diverse thermoelectric material systems.}, author = {Liu, Yu and Kleinhanns, Tobias and Horta, Sharona and Dutkiewicz, Ewelina and Lu, Shaoqing and Spadaro, Maria Chiara and Genç, Aziz and Chen, Lei and Lim, Khak Ho and Hong, Min and Arbiol, Jordi and Ibáñez, Maria}, issn = {1520-5126}, journal = {Journal of the American Chemical Society}, number = {35}, pages = {32199--32208}, publisher = {American Chemical Society}, title = {{Liquid-solid interface reactions drive enhanced thermoelectric performance in Ag2Se}}, doi = {10.1021/jacs.5c11435}, volume = {147}, year = {2025}, }