Budget-Sensitive Discovery Scoring: A Formally Verified Framework for Evaluating AI-Guided Scientific Selection
| Authors | Abhinaba Basu & Pavan Chakraborty |
| Year | 2026 |
| Field | Machine Learning |
| arXiv | 2603.12349 |
| Download | |
| Categories | cs.LG, cs.AI, stat.ML |
Abstract
Scientific discovery increasingly relies on AI systems to select candidates for expensive experimental validation, yet no principled, budget-aware evaluation framework exists for comparing selection strategies -- a gap intensified by large language models (LLMs), which generate plausible scientific proposals without reliable downstream evaluation. We introduce the Budget-Sensitive Discovery Score (BSDS), a formally verified metric -- 20 theorems machine-checked by the Lean 4 proof assistant -- that jointly penalizes false discoveries (lambda-weighted FDR) and excessive abstention (gamma-weighted coverage gap) at each budget level. Its budget-averaged form, the Discovery Quality Score (DQS), provides a single summary statistic that no proposer can inflate by performing well at a cherry-picked budget. As a case study, we apply BSDS/DQS to: do LLMs add marginal value to an existing ML pipeline for drug discovery candidate selection? We evaluate 39 proposers -- 11 mechanistic variants, 14 zero-shot LLM configurations, and 14 few-shot LLM configurations -- using SMILES representations on MoleculeNet HIV (41,127 compounds, 3.5% active, 1,000 bootstrap replicates) under both random and scaffold splits. Three findings emerge. First, the simple RF-based Greedy-ML proposer achieves the best DQS (-0.046), outperforming all MLP variants and LLM configurations. Second, no LLM surpasses the Greedy-ML baseline under zero-shot or few-shot evaluation on HIV or Tox21, establishing that LLMs provide no marginal value over an existing trained classifier. Third, the proposer hierarchy generalizes across five MoleculeNet benchmarks spanning 0.18%-46.2% prevalence, a non-drug AV safety domain, and a 9x7 grid of penalty parameters (tau >= 0.636, mean tau = 0.863). The framework applies to any setting where candidates are selected under budget constraints and asymmetric error costs.
Engineering Breakdown
Plain English
This paper addresses a critical gap in AI-driven scientific discovery: there's no principled way to compare different candidate selection strategies when experimental validation is expensive and limited by budget constraints. The authors introduce the Budget-Sensitive Discovery Score (BSDS), a formally verified metric that simultaneously penalizes false discoveries (using false discovery rate weighted by lambda) and missing good candidates (coverage gap weighted by gamma) at each budget level. They also propose the Discovery Quality Score (DQS), a single summary statistic derived from BSDS that prevents selection strategies from gaming the metric by cherry-picking high-performance regions. The metric has been verified with 20 theorems machine-checked using the Lean 4 proof assistant, providing formal guarantees about its correctness.
Core Technical Contribution
The core novelty is a mathematically rigorous, budget-aware evaluation framework that jointly optimizes two opposing objectives that typically trade off against each other in scientific discovery pipelines. Unlike prior evaluation approaches that focus on either precision or recall independently, BSDS explicitly models the budget constraint and penalizes both false discoveries and abstention (failure to propose good candidates) in a weighted, principled manner. The formal verification via Lean 4 theorems is itself a significant contribution—it guarantees the metric's properties and prevents subtle mathematical errors that could invalidate comparisons. The DQS aggregation scheme is designed to be gaming-resistant: no selection strategy can artificially inflate its score by performing exceptionally well on a subset of budgets while doing poorly elsewhere.
How It Works
The BSDS framework operates by evaluating candidate selection strategies across a range of budget levels, where budget represents the number of experimental slots available. At each budget level b, the system assigns a score that combines two penalty terms: (1) a lambda-weighted false discovery rate (FDR) that penalizes proposing candidates that fail validation, and (2) a gamma-weighted coverage gap that penalizes the fraction of valid candidates not included in the proposal set. The input is a set of proposed candidates ranked by some selection strategy and a binary validation outcome for each (success or failure in downstream experiments). The output at each budget level is a scalar score between 0 and 1, with higher scores indicating better selection quality. The DQS summarizes performance across all budget levels into a single value that cannot be gamed by strategies that perform well at only certain budgets—this robustness is guaranteed by the formal theorems verified in Lean 4.
Production Impact
For teams building AI-driven drug discovery, materials science, or other experimental systems, this metric directly solves the validation problem: you can now objectively compare whether an LLM-based proposal system, a classical scoring method, or a hybrid approach better allocates your limited experimental budget. Adoption would change your evaluation pipeline from ad-hoc metrics (like simple hit rate or precision at k) to a principled framework that reflects real business constraints—experimental validation is expensive and you want to maximize both the quality of what you propose and the coverage of good candidates you shouldn't miss. The formal verification guarantees mean you can defend your selection strategy to stakeholders with mathematical certainty, not just empirical observation. The main trade-off is computational: computing BSDS requires running validation experiments across multiple budget levels, which can be expensive if you're doing frequent model comparisons, though this is a one-time cost per comparison rather than per-inference.
Limitations and When Not to Use This
The paper's scope appears to end at the abstract (the full text is truncated), so specific limitations are partly inferred, but key gaps likely include: the method assumes binary validation outcomes (success/failure), which doesn't capture partial credit or confidence in experimental results common in practice. It also assumes you can afford to validate a representative sample across all budget levels to estimate the FDR and coverage gap—a strong assumption in truly budget-constrained settings where validation itself is rare. The choice of lambda and gamma weights is not addressed in the abstract; in practice, these hyperparameters require domain expertise and sensitivity analysis, and the optimal values may vary by field or problem. The formal verification via Lean 4 guarantees correctness of the mathematical definitions but does NOT guarantee that the metric is well-calibrated for real scientific discovery—the theorems prove the metric works as defined, not that it selects the best strategies for downstream scientific progress.
Research Context
This work sits at the intersection of machine learning evaluation, formal verification, and scientific discovery systems—specifically addressing the recent explosion of LLM-based proposal generation (like AlphaFold for structure prediction or LLMs for hypothesis generation) which produces plausible but often unvalidated candidates at scale. It builds on classical statistical frameworks like false discovery rate control (Benjamini-Hochberg) but extends them to be budget-aware and resistant to gaming, addressing limitations of prior work that evaluated selection strategies in isolation rather than under realistic resource constraints. The use of Lean 4 for theorem proving is increasingly common in high-stakes ML work (safety guarantees, differential privacy proofs) and signals a trend toward formal verification of evaluation metrics themselves. The paper opens a research direction around budget-constrained evaluation: future work will likely extend this to soft validation outcomes, adaptive budget allocation, and multi-objective discovery scenarios.
:::tip Subscribe Get weekly breakdowns of papers like this in AI Letters - the newsletter for engineers building production AI systems. :::