预算敏感的发现评分：一种用于评估AI引导的科学选择的正式验证框架
Budget-Sensitive Discovery Scoring: A Formally Verified Framework for Evaluating AI-Guided Scientific Selection
AI总结：
本文提出BSDS评分，通过正式验证方法评估AI引导的科学选择策略，证明LLMs在药物发现中无额外价值。
摘要：
科学发现越来越多地依赖AI系统来选择需要昂贵实验验证的候选者，但目前缺乏一个原理上考虑预算的评估框架来比较选择策略——这在大型语言模型（LLMs）中尤为突出，因为它们生成有说服力的科学提案但缺乏可靠的下游评估。我们引入了预算敏感的发现评分（BSDS），这是一个经过正式验证的度量标准——20个定理由Lean 4证明助手验证——在每个预算水平上共同惩罚假发现（lambda加权FDR）和过度回避（gamma加权覆盖差距）。其预算平均形式，发现质量评分（DQS），提供了一个无法通过在特定预算上表现良好来人为提高的单一汇总统计量。作为案例研究，我们应用BSDS/DQS来：LLMs是否为现有的ML药物发现候选选择流程增加边际价值？我们评估了39个提案者——11种机械变体，14种零样本LLM配置，14种少量样本LLM配置——使用SMILES表示在MoleculeNet HIV（41,127种化合物，3.5%活性，1,000次bootstrap重复）上，在随机和骨架分割下。三个发现出现。第一，基于简单RF的Greedy-ML提案者在DQS上表现最佳（-0.046），优于所有MLP变体和LLM配置。第二，没有LLM在零样本或少量样本评估中超过Greedy-ML基线在HIV或Tox21上，证明LLMs在现有训练分类器之上没有边际价值。第三，提案者等级在五个MoleculeNet基准上泛化，涵盖0.18%-46.2%的普及率，一个非药物AV安全领域，以及一个9x7的惩罚参数网格（tau >= 0.636，平均tau = 0.863）。该框架适用于任何在预算限制下选择候选者的设置，并且具有不对称误差成本。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
