AI
Researchers Build Verified System to Prevent AI from Making False Scientific Discoveries
A new functional architecture uses formal verification and statistical controls to stop AI-driven research systems from manufacturing spurious results through uncontrolled hypothesis testing.
AI-driven discovery systems can inadvertently produce misleading findings when they run unlimited hypothesis tests without proper statistical safeguards. A new research effort tackles this problem head-on by building a computer-verified system that enforces statistical rigor throughout the research pipeline.
The Core Problem#
When AI systems test many hypotheses without adjustment, they naturally find false patterns in data—a well-known pitfall in statistics called the multiple-testing problem. Traditional AI-Scientist systems lack built-in protections against this, allowing spurious discoveries to pass through as valid results.
A Two-Layer Solution#
The researchers designed an architecture with dual enforcement mechanisms:
- A domain-specific language (built in Haskell) that makes it mathematically impossible to test a hypothesis without first deducting from an error budget. This "Research monad" forces disciplined hypothesis spending.
- An OS-level sandbox that physically prevents AI-generated code from accessing validation data, even if the exact file path is known. This separation ensures held-out test data remains truly held-out.
Verified from Theory to Code#
The team grounded their design in a formal proof system (Lean 4), deriving the error budget for LORD++ (an online false-discovery-rate control procedure) and proving it maintains both marginal and full FDR control. They then verified the budget calculation's correctness down to IEEE 754 floating-point arithmetic using SPARK/Ada—reportedly the first verified chain from mathematical theorem to floating-point implementation for an online FDR procedure.
Real-World Performance#
In simulations, the architecture kept the false discovery rate near 1%, meeting a 5% target, while a naive approach reached 41%. Case studies showed that the validated approach avoids false discoveries that flawed methods would produce, yet still detects real effects when the underlying data support them. Adversarial testing confirmed that generated code cannot circumvent the sandbox to read held-out data.
