AI驱动发现中统计严谨性的结构性强制：一种函数式架构
TLDR
一种函数式架构通过monadic DSL和形式化验证控制错误发现率，强制AI驱动发现的统计严谨性。
评分理由
Strengths: novel integration of formal methods (Lean4, SPARK/Ada) to ensure statistical rigor, with simulation and adversarial evaluation. Weaknesses: lacks real-world empirical validation; case studies may be synthetic, limiting generalizability.
Read-first 评分解释
综合优先阅读分 55.3，由主题、引用、图谱、方法、可复现性和近期性等信号加权得到。 原始总分保留为 68。
研究版图角色
前沿论文
排序敏感性
稳定性：volatile；排名波动范围：68。
关键词评分
深度分析
创新点
- Research monad：一种Haskell嵌入式DSL，强制每次假设检验更新误差预算，使得无法在不考虑多重性的情况下进行检验。
- 带有操作系统级沙箱的声明式脚手架，物理隔离验证数据与LLM生成的代码运行的环境。
- 在Lean 4中对LORD++在线FDR控制的机器检查形式化，包括误差预算的推导以及边际和完全FDR控制的证明。
- 使用SPARK/Ada验证预算的财富不变性在IEEE 754浮点算术上，弥合从定理到实现的差距。
- 首个从定理到浮点实现的在线FDR程序的验证链。
方法
该架构结合了一个Haskell EDSL（Research monad），强制假设检验消耗误差预算，以及一个沙箱执行环境，扣留验证数据不让LLM生成的代码访问。设计基于Lean 4对LORD++在线FDR控制的形式化，包含FDR控制的证明，并在SPARK/Ada中验证了财富不变性在IEEE 754算术上。评估使用模拟、端到端案例研究和对抗性测试。
关键结果
模拟显示该架构将错误发现率保持在接近1%（目标为5%），而朴素方法达到41%。端到端案例研究表明，有效测试避免了虚假发现，但仍能检测到真实效应。对抗性评估证实，生成的代码即使被给予确切路径也无法访问保留数据。