Generalist robot manipulation on unseen tasks and environments

As of Aug-Sep 2026 frontier results remain company-reported and far from reliable zero-shot generality: Generalist AI's GEN-1.5 (Aug 2026) reported 59% average one-shot success on ten simple short-horizon tasks, with no evidence on long sequences, unfamiliar industrial processes or standardized external benchmarks; independent real-robot benchmarks (RoboArena, RoboChallenge) exist because simulation suites like LIBERO do not predict real-world generalization.

Source: quasa.io

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

/-!
# Generalist robot manipulation on unseen tasks and environments

Concrete here: the **scoring**. An evaluation is a finite set of tasks; each task
is run for a fixed number of physical trials whose outcomes are booleans. Per-task
success rate, the mean success rate across tasks, and the per-task floor are all
defined arithmetically here, as is the trial-count requirement.

Opaque oracle (`Evaluation`): the per-trial outcomes themselves, since a trial is
a physical rollout judged by a rubric (LIBERO- or RoboArena-style), plus the
facts that the tasks, objects and scene configurations were withheld from
training, that the policy weights were frozen before disclosure, and that no
per-task fine-tuning or human teleoperation occurred during evaluation.

Who must attest: the evaluation host, publishing the task list and success
rubric, running the trials on its own hardware with the submitted frozen policy,
and recording initial-state randomisation. Per-trial outcome logs are the
evidence; `success` is that log.

Units: success rates are dimensionless fractions in [0,1]; `trials` and task
counts are plain counts. Rates use the guarded denominator `0 < trials`.

Checked with Lean 4.33.0 / Mathlib using:
  lake env lean <absolute-path-to-this-file>
-/

namespace OpenSpur.Problems.GeneralistRobotManipulation

/-- One held-out task, run for `trials` physical rollouts. -/
structure TaskResult where
  trials : ℕ
  /-- Judged outcome of each rollout; supplied by the evaluation host. -/
  success : Fin trials → Bool

/-- Number of successful rollouts on a task (concrete count). -/
def successCount (t : TaskResult) : ℕ :=
  (Finset.univ.filter fun j => t.success j = true).card

/-- Per-task success rate; meaningful when `0 < trials`. -/
noncomputable def successRate (t : TaskResult) : ℝ :=
  (successCount t : ℝ) / (t.trials : ℝ)

/-- A full evaluation over `n` held-out tasks, plus its attestations. -/
structure Evaluation (n : ℕ) where
  task : Fin n → TaskResult
  /-- Tasks, objects and scenes were withheld from training data. -/
  tasksUnseen : Prop
  /-- Policy weights were frozen before the task list was disclosed. -/
  policyFrozen : Prop
  /-- No per-task fine-tuning, no teleoperation, no human resets mid-episode. -/
  noHumanAssistance : Prop

/-- Mean success rate across the held-out tasks. -/
noncomputable def meanSuccessRate {n : ℕ} (E : Evaluation n) : ℝ :=
  (∑ i, successRate (E.task i)) / (n : ℝ)

/-- Bars a board would pay against. -/
structure Thresholds where
  /-- Minimum mean success rate across held-out tasks, e.g. 0.90. -/
  minMeanRate : ℝ
  /-- Floor no individual task may fall below, e.g. 0.50. -/
  minPerTaskRate : ℝ
  /-- Minimum rollouts per task, so a rate is statistically meaningful. -/
  minTrials : ℕ
  /-- Minimum number of held-out tasks in the evaluation. -/
  minTasks : ℕ

/-- Acceptance predicate. -/
def Solved {n : ℕ} (T : Thresholds) (E : Evaluation n) : Prop :=
  E.tasksUnseen ∧
  E.policyFrozen ∧
  E.noHumanAssistance ∧
  T.minTasks ≤ n ∧
  (∀ i, T.minTrials ≤ (E.task i).trials) ∧
  (∀ i, T.minPerTaskRate ≤ successRate (E.task i)) ∧
  T.minMeanRate ≤ meanSuccessRate E

/-- Rung `k` raises the mean bar from 0.50 in steps of 0.05 (capped by the
caller's choice of `k`; `k = 8` is the 0.90 bar) and keeps the other bars fixed. -/
def Rung (k : ℕ) : Thresholds where
  minMeanRate := 0.5 + 0.05 * (k : ℝ)
  minPerTaskRate := 0.25
  minTrials := 20
  minTasks := 50

/-- The mean-rate bar tightens monotonically along the rungs. -/
theorem rung_mean_mono {j k : ℕ} (h : j ≤ k) :
    (Rung j).minMeanRate ≤ (Rung k).minMeanRate := by
  have hjk : (j : ℝ) ≤ (k : ℝ) := Nat.cast_le.mpr h
  simp only [Rung]
  linarith

/-- Solving a higher rung implies solving every lower rung. -/
theorem solved_rung_mono {n j k : ℕ} (h : j ≤ k) (E : Evaluation n) :
    Solved (Rung k) E → Solved (Rung j) E := by
  intro hs
  obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := hs
  exact ⟨h1, h2, h3, h4, h5, h6, le_trans (rung_mean_mono h) h7⟩

/-- Successes never exceed trials: the rate's numerator is bounded by its
denominator, so `successRate ≤ 1` whenever `0 < trials`. -/
theorem successCount_le_trials (t : TaskResult) : successCount t ≤ t.trials := by
  have := Finset.card_filter_le (Finset.univ : Finset (Fin t.trials))
    (fun j => t.success j = true)
  simpa [successCount] using this

end OpenSpur.Problems.GeneralistRobotManipulation

• LIBERO (LeRobot format, Physical Intelligence)
• RoboArena: distributed real-world pairwise evaluation of generalist policies (DROID platform)
• RoboChallenge Table30 real-robot benchmark dataset
• RoboChallenge paper / leaderboard
• Unitree G1 manipulation datasets + UnifoLM models
• Open X-Embodiment dataset
• Gemini Robotics 1.5 technical report (generalization benchmark)