预算敏感发现评分：面向AI引导科学选择的形式化验证框架

科学发现日益依赖AI系统来选择昂贵实验验证的候选人，但目前尚不存在原则且预算感知的评估框架来比较选择策略——这一缺口在大语言模型（LLM）生成缺乏可靠下游评估的科学提案时尤为突出。我们引入预算敏感发现评分（BSDS），这是一项经过形式化验证的度量——由Lean 4证明助手机器检查的20个定理组成——它在每个预算水平上联合惩罚假发现（lambda加权FDR）和过度放弃（gamma加权覆盖差距）。其预算平均形式发现质量评分（DQS）提供了单个概述统计量，任何提议者都无法通过仅在特定预算水平上表现良好来人为制造优势。作为案例研究，我们将BSDS/DQS应用于：LLM在药物发现候选选择中是否提供边际价值？我们对39个提议者进行评估——11个机制变体、14个零shot LLM配置和14个few-shot LLM配置——使用SMILES表示在MoleculeNet HIV（41,127个化合物，3.5%活性，1,000个bootstrap复制）下，分别采用随机划分和骨架划分。三个发现浮现：首先，简单的基于随机森林的Greedy-ML提议者在DQS上取得最佳成绩（-0.046），超越所有MLP变体和LLM配置。其次，在HIV或Tox21上，没有任何LLM在零shot或few-shot评估中超越Greedy-ML基线，确立了LLM在药物发现候选选择中不提供额外价值的证据。第三，提议者层次结构在覆盖0.18%至46.2%不同预valence、非药物AV安全领域以及9x7网格的惩罚参数（tau >= 0.636，平均tau = 0.863）下具有普遍适用性。该框架适用于任何在预算约束下进行候选选择且存在不对称错误成本的场景。