Predicting cellular response to unseen perturbations (virtual cell)

In the 2025 Virtual Cell Challenge almost all models performed worse than baseline on MAE, and Arc concluded perturbation models are not yet consistently beating naive baselines; independently, Ahlmann-Eltze et al. (Nature Methods 2025) found scGPT, scFoundation and GEARS do not beat simple linear baselines. Arc says it would be 'pleasantly surprised' if anyone reaches the target level in the 2026 round.

Source: arcinstitute.org

import Mathlib

/-!
# Predicting cellular response to unseen perturbations (virtual cell)

Modelled on the Arc Institute Virtual Cell Challenge: given a cell context and a
genetic perturbation not seen in training, predict the post-perturbation expression
profile. Scored on held-out perturbations by three metrics, each compared with a
pinned baseline (e.g. predict the mean perturbed profile):
* MAE of the pseudobulk expression profile (lower is better),
* perturbation discrimination: is the prediction closer to its own true profile than
  to other perturbations' true profiles (higher is better),
* differential-expression overlap: fraction of truly DE genes recovered (higher is better).

Concrete in Lean: all three metrics over finite gene/perturbation sets and the
"better than baseline on all three by margins" Prop.

Opaque oracle (`HeldOut`): measured pseudobulk profiles for the hidden perturbations
(from single-cell sequencing), the true DE gene sets (from the organisers' pinned
statistical test and FDR), and the baseline's scores. Attester: the challenge organiser
/ data generator.

Units: expression in the organisers' pinned normalization (e.g. log1p CP10k);
scores dimensionless.
-/

namespace OpenSpur.Problems.PerturbationResponse

noncomputable section

/-- Held-out data: `P` perturbations, `G` genes (oracle). -/
structure HeldOut (P G : ℕ) where
  truth : Fin P → Fin G → ℝ
  trueDE : Fin P → Finset (Fin G)
  baseMAE : ℝ
  baseDisc : ℝ
  baseDE : ℝ

/-- Submission: predicted profile and predicted DE set per held-out perturbation. -/
structure Submission (P G : ℕ) where
  profile : Fin P → Fin G → ℝ
  de : Fin P → Finset (Fin G)

def l1 {G : ℕ} (u v : Fin G → ℝ) : ℝ := ∑ g, |u g - v g|

def mae {P G : ℕ} (h : HeldOut P G) (s : Submission P G) : ℝ :=
  (∑ p, l1 (s.profile p) (h.truth p)) / ((P : ℝ) * G)

/-- 1 − mean fraction of other perturbations whose truth is strictly closer to the prediction. -/
def discrimination {P G : ℕ} (h : HeldOut P G) (s : Submission P G) : ℝ :=
  1 - (∑ p, ((Finset.univ.filter fun q =>
          q ≠ p ∧ l1 (s.profile p) (h.truth q) < l1 (s.profile p) (h.truth p)).card : ℝ)
        / ((P : ℝ) - 1)) / P

/-- Mean recall of true DE genes; predicted set truncated in effect by requiring |pred| ≤ |true|. -/
def deOverlap {P G : ℕ} (h : HeldOut P G) (s : Submission P G) : ℝ :=
  (∑ p, ((s.de p ∩ h.trueDE p).card : ℝ) / (h.trueDE p).card) / P

structure Thresholds where
  minPerts : ℕ
  maeMargin : ℝ
  discMargin : ℝ
  deMargin : ℝ

def Solved {P G : ℕ} (T : Thresholds) (h : HeldOut P G) (s : Submission P G) : Prop :=
  T.minPerts ≤ P ∧ 2 ≤ P ∧
  (∀ p, (s.de p).card ≤ (h.trueDE p).card) ∧
  mae h s + T.maeMargin ≤ h.baseMAE ∧
  h.baseDisc + T.discMargin ≤ discrimination h s ∧
  h.baseDE + T.deMargin ≤ deOverlap h s

def rung (T : Thresholds) (k : ℕ) : Thresholds :=
  { T with discMargin := T.discMargin + (k : ℝ) / 20, deMargin := T.deMargin + (k : ℝ) / 20 }

end

theorem rung_mono {P G : ℕ} (T : Thresholds) (h : HeldOut P G) (s : Submission P G)
    {j k : ℕ} (hjk : j ≤ k) (hs : Solved (rung T k) h s) : Solved (rung T j) h s := by
  have hc : (j : ℝ) ≤ k := by exact_mod_cast hjk
  obtain ⟨a, b, c, d, e, f⟩ := hs
  refine ⟨a, b, c, d, ?_, ?_⟩ <;> simp only [rung] at e f ⊢ <;> linarith

end OpenSpur.Problems.PerturbationResponse

• Virtual Cell Challenge (Arc Institute) - leaderboard and cell-eval metrics
• Virtual Cell Challenge 2026 benchmark paper (Cell)
• Open Problems - Single-Cell Perturbations (Kaggle / NeurIPS 2023)
• Tahoe-100M single-cell drug perturbation atlas (Hugging Face)
• X-Atlas/Orion genome-wide Perturb-seq dataset (Xaira)
• Linear-baseline benchmark (Ahlmann-Eltze, Huber, Anders; Nature Methods 2025)
• TxPert code (Valence Labs)