❌

Normal view

Received — 8 April 2026 ⏭

Automated Conjecture Resolution with Formal Verification

✇cs.AI, q-bio.NC updates on arXiv.org
By: Haocheng Ju · Guoxiong Gao · Jiedong Jiang · Bin Wu · Zeming Sun · Leheng Chen · Yutong Wang · Yuefeng Wang · Zichen Wang · Wanyi He · Peihao Wu · Liang Xiao · Ruochuan Liu · Bryan Dai · Bin Dong
7 April 2026 at 12:00
arXiv:2604.03789v1 Announce Type: cross Abstract: Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework for tackling research-level mathematical problems that integrates natural language reasoning with formal verification, enabling end-to-end problem solving with minimal human intervention. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas mimics the workflow of human mathematicians by combining reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with our formal theorem search engine LeanSearch, translates informal arguments into formalized Lean 4 projects through structured task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent is capable of autonomously filling nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, substantially reduce human effort, and offer a concrete instantiation of human-AI collaborative mathematical research.

BAAI Cardiac Agent: An intelligent multimodal agent for automated reasoning and diagnosis of cardiovascular diseases from cardiac magnetic resonance imaging

✇cs.AI, q-bio.NC updates on arXiv.org
By: Taiping Qu · Hongkai Zhang · Lantian Zhang · Can Zhao · Nan Zhang · Hui Wang · Zhen Zhou · Mingye Zou · Kairui Bo · Pengfei Zhao · Xingxing Jin · Zixian Su · Kun Jiang · Huan Liu · Yu Du · Maozhou Wang · Ruifang Yan · Zhongyuan Wang · Tiejun Huang · Lei Xu · Henggui Zhang
7 April 2026 at 12:00
arXiv:2604.04078v1 Announce Type: cross Abstract: Cardiac magnetic resonance (CMR) is a cornerstone for diagnosing cardiovascular disease. However, it remains underutilized due to complex, time-consuming interpretation across multi-sequences, phases, quantitative measures that heavily reliant on specialized expertise. Here, we present BAAI Cardiac Agent, a multimodal intelligent system designed for end-to-end CMR interpretation. The agent integrates specialized cardiac expert models to perform automated segmentation of cardiac structures, functional quantification, tissue characterization and disease diagnosis, and generates structured clinical reports within a unified workflow. Evaluated on CMR datasets from two hospitals (2413 patients) spanning 7-types of major cardiovascular diseases, the agent achieved an area under the receiver-operating-characteristic curve exceeding 0.93 internally and 0.81 externally. In the task of estimating left ventricular function indices, the results generated by this system for core parameters such as ejection fraction, stroke volume, and left ventricular mass are highly consistent with clinical reports, with Pearson correlation coefficients all exceeding 0.90. The agent outperformed state-of-the-art models in segmentation and diagnostic tasks, and generated clinical reports showing high concordance with expert radiologists (six readers across three experience levels). By dynamically orchestrating expert models for coordinated multimodal analysis, this agent framework enables accurate, efficient CMR interpretation and highlights its potentials for complex clinical imaging workflows. Code is available at https://github.com/plantain-herb/Cardiac-Agent.
Received — 2 April 2026 ⏭

Two-step clinical care pathway to predict MASLD-related advanced fibrosis and long-term outcomes in type 2 diabetes

✇(Multiomics OR Omics) AND (Lung OR gastric OR Hepatocellular)
By: Yuping Chen · Bingtian Dong · Xinrui Jin · Chuan Liu · Ming-Hua Zheng · Xiao Liang · Yameng Sun · Hye Won Lee · Huapeng Lin · Emmanuel Tsochatzis · Salvatore Petta · Elisabetta Bugianesi · Masato Yoneda · Hannes Hagström · Jérôme Boursier · José Luis Calleja · George Boon-Bee Goh · Wah-Kheong Chan · Rocio Gallego-Durán · Arun J Sanyal · Victor de Lédinghen · Philip N Newsome · Jian-Gao Fan · Laurent Castéra · Michelle Lai · Céline Fournier-Poizat · Grace Lai-Hung Wong · Grazia Pennisi · Angelo Armandi · Atsushi Nakajima · Wen-Yue Liu · Ying Shang · Marc de Saint-Loup · Elba Llop · Kevin Kim Jun Teh · Carmen Lara-Romero · Amon Asgharpour · Sara Mahgoub · Mandy Sau-Wai Chan · Adrien Lannes · Manuel Romero-Gomez · Airong Hu · Yiling Li · Qing-Lei Zeng · Wei Gou · Hua Bian · Xiao Han · Chenlin Sun · Seung Up Kim · Terry Cheuk-Fung Yip · Gao-Jun Teng · Vincent Wai-Sun Wong · Xiaolong Qi · DiabetesLiver Integrated Management (DLIM) Consortium
30 March 2026 at 18:00

Gut. 2026 Feb 9;75(3):576-587. doi: 10.1136/gutjnl-2025-337506.

ABSTRACT

BACKGROUND: Current guidelines recommend a two-step approach for risk stratification of metabolic dysfunction-associated steatotic liver disease (MASLD), starting with Fibrosis-4 index (FIB-4) followed by liver stiffness measurement (LSM) using vibration-controlled transient elastography (VCTE).

OBJECTIVE: To evaluate this approach for predicting advanced fibrosis and liver-related events (LREs) in patients with type 2 diabetes (T2D).

DESIGN: A prospective liver biopsy cohort of T2D patients with histologically confirmed MASLD from seven centres in China was used to assess diagnostic performance for advanced fibrosis. The international VCTE-Prognosis cohort, including T2D patients with MASLD who underwent VCTE at 16 centres in the USA, Europe and Asia, with longitudinal follow-up, was used to assess LREs, defined as hepatic decompensation or hepatocellular carcinoma.

RESULTS: 4781 participants were included. In the liver biopsy cohort (n=352; 22.2% with advanced fibrosis), applying LSM thresholds of <8 kPa and >12 kPa after FIB-4 classified patients into 63.4% low-risk, 9.4% intermediate-risk and 27.3% high-risk, with a correct classification rate of 71%. In the VCTE-Prognosis cohort (n=4429; median follow-up 51.3 (IQR 27.4-70.7) months), 140 (3.2%) patients developed LREs (110 (2.5%) with hepatic decompensation and 59 (1.3%) with hepatocellular carcinoma). The two-step approach classified 72.6%, 6.8% and 20.6% of patients into low-risk, intermediate-risk and high-risk groups, with corresponding 5-year cumulative LRE incidences of 0.7%, 0.9% and 11.8%. Refining classification of intermediate FIB-4 patients using LSM <10 kPa (low-risk) and >15 kPa (high-risk) reduced the intermediate-risk group to 5.6% while preserving predictive accuracy.

CONCLUSION: The non-invasive two-step approach of FIB-4 followed by LSM effectively stratifies MASLD-related advanced fibrosis and LREs risk in T2D. Applying LSM cut-offs of 10 and 15 kPa further optimises risk stratification for future LREs.

PMID:41911049 | DOI:10.1136/gutjnl-2025-337506

Received — 11 March 2026 ⏭

Lysophosphatidylcholine acyltransferase 1 promotes head and neck squamous cell carcinoma progression by enhancing COX17-dependent oxidative phosphorylation

✇Cell Death Discovery nature.com science feeds
By: Yuanyang Zhao · Yun Li · Yanshi Li · Zhihai Wang · Chuan Liu · Lin Chen · Min Wang · Mengna Wang · Zhaobo Cheng · Guohua Hu · Min Pan
6 March 2026 at 08:00

Cell Death Discovery, Published online: 06 March 2026; doi:10.1038/s41420-026-02994-3

Lysophosphatidylcholine acyltransferase 1 promotes head and neck squamous cell carcinoma progression by enhancing COX17-dependent oxidative phosphorylation
Received — 5 March 2026 ⏭

Pretrained Vision-Language-Action Models are Surprisingly Resistant to Forgetting in Continual Learning

✇cs.AI, q-bio.NC updates on arXiv.org
By: Huihan Liu · Changyeon Kim · Bo Liu · Minghuan Liu · Yuke Zhu
5 March 2026 at 13:00
arXiv:2603.03818v1 Announce Type: cross Abstract: Continual learning is a long-standing challenge in robot policy learning, where a policy must acquire new skills over time without catastrophically forgetting previously learned ones. While prior work has extensively studied continual learning in relatively small behavior cloning (BC) policy models trained from scratch, its behavior in modern large-scale pretrained Vision-Language-Action (VLA) models remains underexplored. In this work, we found that pretrained VLAs are remarkably resistant to forgetting compared with smaller policy models trained from scratch. Simple Experience Replay (ER) works surprisingly well on VLAs, sometimes achieving zero forgetting even with a small replay data size. Our analysis reveals that pretraining plays a critical role in downstream continual learning performance: large pretrained models mitigate forgetting with a small replay buffer size while maintaining strong forward learning capabilities. Furthermore, we found that VLAs can retain relevant knowledge from prior tasks despite performance degradation during learning new tasks. This knowledge retention enables rapid recovery of seemingly forgotten skills through finetuning. Together, these insights imply that large-scale pretraining fundamentally changes the dynamics of continual learning, enabling models to continually acquire new skills over time with simple replay. Code and more information can be found at https://ut-austin-rpl.github.io/continual-vla

Preference Leakage: A Contamination Problem in LLM-as-a-judge

✇cs.AI, q-bio.NC updates on arXiv.org
By: Dawei Li · Renliang Sun · Yue Huang · Ming Zhong · Bohan Jiang · Jiawei Han · Xiangliang Zhang · Wei Wang · Huan Liu
5 March 2026 at 13:00
arXiv:2502.01534v3 Announce Type: replace-cross Abstract: Large Language Models (LLMs) as judges and LLM-based data synthesis have emerged as two fundamental LLM-driven data annotation methods in model development. While their combination significantly enhances the efficiency of model training and evaluation, little attention has been given to the potential contamination brought by this new model development paradigm. In this work, we expose preference leakage, a contamination problem in LLM-as-a-judge caused by the relatedness between the synthetic data generators and LLM-based evaluators. To study this issue, we first define three common relatednesses between the data generator LLM and the judge LLM: being the same model, having an inheritance relationship, and belonging to the same model family. Through extensive experiments, we empirically confirm the bias of judges towards their related student models caused by preference leakage across multiple LLM baselines and benchmarks. Further analysis suggests that preference leakage is a pervasive and real-world problem that is harder to detect compared to previously identified biases in LLM-as-a-judge scenarios. All of these findings imply that preference leakage is a widespread and challenging problem in the area of LLM-as-a-judge. We release all codes and data at: https://github.com/David-Li0406/Preference-Leakage.
Received — 25 February 2026 ⏭

Boolean Satisfiability via Imitation Learning

✇cs.AI, q-bio.NC updates on arXiv.org
By: Zewei Zhang · Huan Liu · Yuanhao Yu · Jun Chen · Xiangyu Xu
24 February 2026 at 13:00
arXiv:2509.25411v2 Announce Type: replace Abstract: We propose ImitSAT, a branching policy for conflict-driven clause learning (CDCL) solvers based on imitation learning for the Boolean satisfiability problem (SAT). Unlike previous methods that predict instance-level signals to improve CDCL branching indirectly, or rely on reinforcement learning and insufficient CDCL information to enhance branching, ImitSAT learns from expert KeyTrace that collapses a full run into the sequence of surviving decisions. Replaying a KeyTrace on the same instance is nearly conflict-free, providing dense decision-level supervision and directly reducing propagations -- the dominant contributor to wall-clock time. This prefix-conditioned supervision enables ImitSAT to reproduce high-quality branches without exploration, yielding faster convergence, stable training, and seamless integration into CDCL. Extensive experiments demonstrate that ImitSAT reduces propagation counts and runtime, outperforming state-of-the-art learned approaches. We released the source code and trained model at https://github.com/zewei-Zhang/ImitSAT
There are no more articles
❌