-
ECTIL: Label-efficient Computational Tumour Infiltrating Lymphocyte (TIL) assessment in breast cancer: Multicentre validation in 2,340 patients with breast cancer
Authors:
Yoni Schirris,
Rosie Voorthuis,
Mark Opdam,
Marte Liefaard,
Gabe S Sonke,
Gwen Dackus,
Vincent de Jong,
Yuwei Wang,
Annelot Van Rossum,
Tessa G Steenbruggen,
Lars C Steggink,
Liesbeth G. E. de Vries,
Marc van de Vijver,
Roberto Salgado,
Efstratios Gavves,
Paul J van Diest,
Sabine C Linn,
Jonas Teuwen,
Renee Menezes,
Marleen Kok,
Hugo Horlings
Abstract:
The level of tumour-infiltrating lymphocytes (TILs) is a prognostic factor for patients with (triple-negative) breast cancer (BC). Computational TIL assessment (CTA) has the potential to assist pathologists in this labour-intensive task, but current CTA models rely heavily on many detailed annotations. We propose and validate a fundamentally simpler deep learning based CTA that can be trained in o…
▽ More
The level of tumour-infiltrating lymphocytes (TILs) is a prognostic factor for patients with (triple-negative) breast cancer (BC). Computational TIL assessment (CTA) has the potential to assist pathologists in this labour-intensive task, but current CTA models rely heavily on many detailed annotations. We propose and validate a fundamentally simpler deep learning based CTA that can be trained in only ten minutes on hundredfold fewer pathologist annotations. We collected whole slide images (WSIs) with TILs scores and clinical data of 2,340 patients with BC from six cohorts including three randomised clinical trials. Morphological features were extracted from whole slide images (WSIs) using a pathology foundation model. Our label-efficient Computational stromal TIL assessment model (ECTIL) directly regresses the TILs score from these features. ECTIL trained on only a few hundred samples (ECTIL-TCGA) showed concordance with the pathologist over five heterogeneous external cohorts (r=0.54-0.74, AUROC=0.80-0.94). Training on all slides of five cohorts (ECTIL-combined) improved results on a held-out test set (r=0.69, AUROC=0.85). Multivariable Cox regression analyses indicated that every 10% increase of ECTIL scores was associated with improved overall survival independent of clinicopathological variables (HR 0.86, p<0.01), similar to the pathologist score (HR 0.87, p<0.001). We demonstrate that ECTIL is highly concordant with an expert pathologist and obtains a similar hazard ratio. ECTIL has a fundamentally simpler design than existing methods and can be trained on orders of magnitude fewer annotations. Such a CTA may be used to pre-screen patients for, e.g., immunotherapy clinical trial inclusion, or as a tool to assist clinicians in the diagnostic work-up of patients with BC. Our model is available under an open source licence (https://github.com/nki-ai/ectil).
△ Less
Submitted 24 January, 2025;
originally announced January 2025.
-
Searching Entangled Program Spaces
Authors:
James Koppel,
Zheng Guo,
Edsko de Vries,
Armando Solar-Lezama,
Nadia Polikarpova
Abstract:
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures -- version-space algebras, finite tree automata, or e-graphs -- to compactly represent these programs. To find a compact representation, existing data structures exploit independence of su…
▽ More
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures -- version-space algebras, finite tree automata, or e-graphs -- to compactly represent these programs. To find a compact representation, existing data structures exploit independence of subterms; they blow up when the choices of subterms are entangled. We introduce equality-constrained tree automata (ECTAs), a generalization of the three aforementioned data structures that can efficiently represent large spaces of programs with entangled subterms. We present efficient algorithms for extracting programs from ECTAs, implemented in a performant Haskell library, \texttt{ecta}. Using \texttt{ecta} we construct \textsc{Hectare}, a type-driven program synthesizer for Haskell. \textsc{Hectare} significantly outperforms a state-of-the-art synthesizer Hoogle+ -- providing an average speedup of 8x -- despite its implementation being an order of magnitude smaller.
△ Less
Submitted 15 June, 2022;
originally announced June 2022.
-
Locally Nameless Permutation Types
Authors:
Edsko de Vries,
Vasileios Koutavas
Abstract:
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is particularly useful when formalizing programming languages where bound names may become free during execution ("extrusion"), common in process calculi. It inherits the generic definition of permutations and support, and…
▽ More
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is particularly useful when formalizing programming languages where bound names may become free during execution ("extrusion"), common in process calculi. It inherits the generic definition of permutations and support, and associated lemmas, from the Nominal approach, and the ability to stay close to pencil-and-paper proofs from the locally nameless approach. We explain how to use cofinite quantification in this setting, show why reasoning about renaming is more important here than in languages without extrusion, and provide results about infinite support, necessary when reasoning about countable choice.
△ Less
Submitted 23 October, 2017;
originally announced October 2017.
-
Uniqueness Typing for Resource Management in Message-Passing Concurrency
Authors:
Edsko de Vries,
Adrian Francalanza,
Matthew Hennessy
Abstract:
We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increas…
▽ More
We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.
△ Less
Submitted 29 March, 2010;
originally announced March 2010.