Proof-Carrying Materials: Falsifiable Safety Certificates for Machine-Learned Interatomic Potentials

This paper introduces Proof-Carrying Materials (PCM), a rigorous framework combining adversarial falsification, statistical refinement, and formal Lean 4 certification to overcome the high failure rates of single machine-learned interatomic potentials, thereby significantly improving the reliability and discovery yield of high-throughput materials screening.

The Gist

Imagine you are a chef trying to create a new, revolutionary recipe for a cake. You have a super-fast, AI-powered assistant (the Machine-Learned Interatomic Potential, or MLIP) that can taste-test thousands of ingredient combinations in a second and tell you, "This will be delicious!" or "This will be a disaster."

The problem? You've never asked the AI to prove why it thinks something will fail. It just gives you a gut feeling. And as this paper shows, that gut feeling is often wrong, missing 93% of the actually delicious cakes and serving you a lot of burnt ones.

The authors of this paper, Abhinaba Basu and Pavan Chakraborty, propose a new system called Proof-Carrying Materials (PCM). Think of it as giving your AI assistant a "safety certificate" that it must earn before you trust its advice.

Here is how the system works, broken down into three simple steps:

1. The "Bad Guy" Test (Adversarial Falsification)

Imagine you want to test if a bridge is safe. You wouldn't just drive a car over it; you'd hire a team of engineers to try to break it. You'd drive heavy trucks, shake it with earthquakes, and see where it cracks.

In this paper, the "bridge" is the AI's prediction of a material's stability. The "engineers" are adversarial algorithms (including some that act like Large Language Models). Their job is to be "bad guys." They try to find specific chemical recipes that the AI says are stable, but which are actually disasters.

• The Result: They found that different AI models have different "blind spots." One AI might think a material with heavy metals is fine, while another thinks it's unstable. They don't agree on why things fail. If you only use one AI, you miss huge chunks of the truth.

2. Drawing the "Safe Zone" (Envelope Refinement)

Once the "bad guys" find where the AI fails, the system draws a map. It creates a boundary line around the "Safe Zone."

• The Analogy: Think of a weather forecast. Instead of saying "It might rain," the system says, "If the temperature is above 30°C and humidity is over 80%, do not trust the AI's prediction."
• The system uses statistics to make this boundary very tight and reliable (with 95% confidence). It tells you exactly which types of materials (e.g., those with heavy elements or large structures) are too risky to trust the AI on.

3. The "Mathematical Seal" (Formal Certification)

This is the coolest part. Usually, when a scientist says, "I'm pretty sure this is safe," they just write a report. Here, the system writes a mathematical proof (using a tool called Lean 4) that can be checked by a computer.

• The Analogy: It's like a bank vault. Instead of just trusting the guard, the vault comes with a digital certificate that proves, beyond any doubt, that the lock works according to the laws of physics. The computer checks the math and says, "Yes, the rules hold up. This safety claim is valid."

Why Does This Matter?

The paper tested this on a massive database of 25,000 materials.

• The Old Way: If you used just one AI to screen for new materials (like solar cells or batteries), you would miss 93% of the good ones because the AI was too scared to predict them, or it confidently predicted them as "bad" when they were actually "good."
• The New Way (PCM): By using this "safety certificate" system, they found 62 extra stable materials that the old method missed. They also saved time and money by knowing exactly which materials needed expensive, real-world computer simulations (DFT) and which ones could be trusted.

The Big Takeaway

The authors discovered that no single AI model is perfect. They all have different blind spots.

• The Solution: Don't just trust one AI. Use this "Proof-Carrying" system to audit them. It acts like a quality control inspector that says, "We trust the AI for these ingredients, but for these specific ingredients, we need to double-check with a human (or a more expensive computer)."

In short, Proof-Carrying Materials turns AI from a "black box" that guesses into a transparent, certified tool that tells you exactly when it's safe to use and when it's time to be careful. It's the difference between trusting a weather app that says "maybe" and one that gives you a verified, mathematical guarantee of a storm.

Technical Summary

Here is a detailed technical summary of the paper "Proof-Carrying Materials: Falsifiable Safety Certificates for Machine-Learned Interatomic Potentials."

1. Problem Statement

Machine-Learned Interatomic Potentials (MLIPs) are increasingly used for high-throughput materials screening to accelerate discovery. However, they are deployed without formal reliability guarantees.

• The Reliability Gap: Aggregate accuracy metrics (e.g., mean absolute error on benchmarks) fail to identify specific chemical compositions where models are unreliable.
• Critical Failure: A single MLIP used as a stability filter misses 93% of Density Functional Theory (DFT)-stable materials (recall = 0.07) on a 25,000-material benchmark.
• Blind Spots: Models like CHGNet, TensorNet, and MACE exhibit architecture-specific blind spots, often rejecting scientifically important materials (e.g., topological insulators like TlBiSe2 or lead-free perovskites) due to systematic errors in specific chemical families (e.g., heavy elements, large unit cells).
• Limitations of Current UQ: Existing Uncertainty Quantification (UQ) methods (e.g., perturbation-based variance) are orthogonal to compositional failures and cannot predict which specific chemistries will fail.

2. Methodology: The Proof-Carrying Materials (PCM) Framework

The authors propose Proof-Carrying Materials (PCM), a three-stage framework inspired by "Proof-Carrying Code," to generate falsifiable safety certificates for MLIPs. The framework is oracle-agnostic and does not require retraining the models.

Stage 1: Adversarial Falsification

• Goal: Systematically probe the compositional space to find "counterexamples" (materials where the MLIP prediction diverges significantly from DFT).
• Mechanism: Six automated adversary strategies are employed:
  1. Random sampling
  2. Heuristic (beta-distribution biased)
  3. Grid search
  4. Latin Hypercube Sampling (LHS)
  5. Sobol sequences
  6. LLM Adversaries: Large Language Models propose feature vectors targeting likely failure regions.
• Process: Adversaries propose compositional feature vectors; the MLIP oracle evaluates them against a DFT reference (WBM benchmark).

Stage 2: Envelope Refinement

• Goal: Convert the discovered counterexamples into a rigorous "safety envelope" (bounds on acceptable error).
• Mechanism: Counterexamples are used to tighten the bounds of the safety claim.
• Statistical Rigor: Bootstrap resampling (1,000 iterations) is used to establish 95% confidence intervals (CIs) for these bounds, ensuring the safety claim is statistically robust.

Stage 3: Formal Certification

• Goal: Provide machine-checkable proof that the MLIP is safe within the refined envelope.
• Mechanism: The refined envelope and physical axioms are compiled into Lean 4 formal proofs.
• Output: A "Safety Certificate" containing:
  • Explicit physical axioms (e.g., DFT uncertainty bounds, MLIP thresholds).
  • Machine-verified theorems proving that if the input falls within the envelope, the safety claim holds.
  • A prospective risk model trained on discovered failure patterns.

3. Key Contributions

1. Quantification of Blind Spots: Demonstrated that different MLIP architectures (CHGNet, TensorNet, MACE) have near-zero pairwise error correlations ($r \le 0.13$) and largely disjoint failure profiles. A model that passes one architecture's test may fail catastrophically on another.
2. Adversarial vs. Structural UQ: Proved that structural perturbation-based UQ (current standard) is orthogonal to compositional failure ($r = 0.039$). A model can be "confidently wrong" on entire chemical families, a fact only adversarial compositional auditing can detect.
3. Formal Verification for ML: Successfully applied Lean 4 to generate machine-checkable safety certificates for regression models in materials science, bridging the gap between data-driven models and formal verification.
4. Prospective Prediction: Showed that features discovered during adversarial auditing (e.g., number of sites, volume per atom, max atomic number) can train a risk model that predicts failures on unseen materials with high accuracy ($AUC\text{-}ROC = 0.938$).
5. Cross-Architecture Transfer: Demonstrated that risk models trained on one MLIP's failures can predict failures in other architectures (cross-MLIP $AUC\text{-}ROC \approx 0.70$), suggesting shared compositional vulnerability drivers.

4. Key Results

• Failure Rates: On a 5,000-material benchmark:
  • CHGNet failed on 31.1% of compositions.
  • TensorNet failed on 75.7%.
  • MACE failed on 73.2%.
  • Disjoint Failures: 2,324 materials failed MACE but not CHGNet; 218 failed CHGNet but not MACE.
• Independent Validation: Independent DFT re-computation (Quantum ESPRESSO) on 20 adversarially selected "worst-case" materials confirmed 100% convergence to ground states. CHGNet underestimated forces by a median factor of 12× (e.g., Brass Cu7Zn1: DFT 557 eV/Å vs. CHGNet 36 eV/Å).
• Discovery Yield Improvement: In a thermoelectric screening case study (647 candidates):
  • Single-MLIP screening missed 50% of stable materials.
  • PCM-audited screening discovered 62 additional stable materials (a 25% improvement in yield) by routing high-risk candidates to DFT.
  • Precision improved from 0.795 to 0.852.
• Cost Efficiency: The full multi-strategy audit costs < $20. The risk model allows for prioritized DFT allocation, improving DFT efficiency by 34% (finding 75.6% stable materials vs. 56.3% with random allocation).
• Generalizability: The framework was successfully applied to non-materials domains (QM9 molecular properties, ESOL drug solubility, California Housing tabular data), confirming the pipeline's universality.

5. Significance and Impact

• Paradigm Shift: Moves MLIP validation from "aggregate benchmark scores" to falsifiable safety claims with formal guarantees.
• Deployment Safety: Provides a concrete protocol for practitioners:
  1. Screen with a union of MLIPs to maximize recall.
  2. Apply the PCM risk model to flag high-risk compositional regions.
  3. Allocate expensive DFT resources only to flagged materials.
• Scientific Discovery: Prevents the systematic rejection of high-value materials (e.g., topological insulators, nuclear fuel candidates) that fall into specific "blind spots" of popular models.
• Accessibility: The framework is open-source, requires no model retraining, and operates with a minimal query budget (200 queries), making it feasible for immediate adoption in high-throughput pipelines.

In conclusion, Proof-Carrying Materials establishes that MLIP reliability is not a monolithic property but a compositional one. By combining adversarial testing, statistical refinement, and formal verification, PCM provides the first rigorous, machine-checkable safety certificates for materials discovery, transforming risk management from a retrospective audit into a predictive intervention.