Imperial College London（帝国理工学院）

IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

IsabeLLM: 自动化定理证明应用于共识的形式化验证

Elliot Jones, William Knottenbelt

机构 * Imperial College London（伦敦帝国学院） 纠错

AI总结 本文改进IsabeLLM自动化定理证明工具，通过检索增强生成、错误追踪和反例生成提升大语言模型上下文，并兼容最新Isabelle和Sledgehammer，用于验证比特币工作量证明共识。

SegDINO: Introducing Multi-Scale Structure into DINO for Efficient Medical Image Segmentation

SegDINO: 将多尺度结构引入DINO以实现高效医学图像分割

Sicheng Yang, Hongqiu Wang, Zhaohu Xing, Sixiang Chen, Qiuxia Yang, Yize Mao, Guang Yang, Lei Zhu

机构 * The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州）） ； Sun Yat-sen University Cancer Center（中山大学肿瘤防治中心） ； Imperial College London（帝国理工学院） 纠错

AI总结 提出SegDINO框架，通过令牌金字塔适应和尺度感知解码将多尺度结构引入DINO，在保持高效的同时实现医学图像分割的最优性能。

Comments Code: https://github.com/script-Yang/segdino_v2

PearlVLA: Progressive Embodied Action-Plan Refinement in Latent Space

PearlVLA：潜在空间中的渐进式具身动作计划精炼

Bochen Yang, Lianlei Shan

机构 * Imperial College London（帝国理工学院） ； Tsinghua University（清华大学） 纠错

AI总结 提出PearlVLA框架，通过在VLM潜在空间中进行迭代计划精炼，平衡动作生成效率与显式推理，在LIBERO基准上达到最先进性能。

Comments 21 pages, 2 figures. Preprint

QueryMarket: Cost-Aware Online Active Learning in Data Markets

QueryMarket: 数据市场中成本感知的在线主动学习

Xiwen Huang, Pierre Pinson

机构 * Dyson School of Design Engineering, Imperial College London（帝国理工学院戴森设计工程学院） ； Halfspace (part of Accenture)（埃森哲旗下Halfspace） ； Technical University of Denmark (DTU Management)（丹麦技术大学（DTU管理系）） ； Aarhus University (CoRE)（奥胡斯大学（CoRE）） 纠错

AI总结 提出QueryMarket框架和OVBAL算法，通过D-最优性准则估计边际效用，在滚动预算约束下实现成本感知的在线主动学习，适应非平稳流和异构标签成本。

Comments 10 pages, 8 figures. Submitted to IEEE Transactions on Neural Networks and Learning Systems