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

Abhinaba Basu; Pavan Chakraborty

cond-mat.mtrl-sciMar 12, 2026

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

Authors: Abhinaba Basu, Pavan Chakraborty

Organizations: Indian Institute of Information Technology Allahabad (IIITA), Prayagraj, India · National Institute of Electronics and Information Technology (NIELIT), India

Abstract

Machine-learned interatomic potentials (MLIPs) are deployed for high-throughput materials screening without formal reliability guarantees. We show that 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. Proof-Carrying Materials (PCM) closes this gap through three stages: adversarial falsification across compositional space, bootstrap envelope refinement with 95% confidence intervals, and Lean 4 formal certification. Auditing CHGNet, TensorNet and MACE reveals architecture-specific blind spots with near-zero pairwise error correlations (r <= 0.13; n = 5,000), confirmed by independent Quantum ESPRESSO validation (20/20 converged; median DFT/CHGNet force ratio 12x). A risk model trained on PCM-discovered features predicts failures on unseen materials (AUC-ROC = 0.938 +/- 0.004) and transfers across architectures (cross-MLIP AUC-ROC ~ 0.70; feature importance r = 0.877). In a thermoelectric screening case study, PCM-audited protocols discover 62 additional stable materials missed by single-MLIP screening - a 25% improvement in discovery yield.

Figures & tables

Figure 1: The PCM pipeline. Stage 1 : automated adversaries (six strategies including LLMs) propose compositional feature vectors; the MLIP oracle evaluates each against the DFT reference. Stage 2 : counterexamples refine the safety envelope with bootstrap CIs. Stage 3 : the envelope compiles into Lean 4 proofs with explicit axioms.

Figure 2: Cross-MLIP comparison of three architecturally distinct MLIPs on 5,000 WBM-derived structures. a , CHGNet vs MACE max force ( $r=0.13$ ). b , Pairwise force correlation heatmap: all three pairs near zero (CHGNet–TensorNet $r=0.10$ , CHGNet–MACE $r=0.13$ , TensorNet–MACE $r=-0.01$ ). c , Failure rates: CHGNet 31.1%, TensorNet 75.7%, MACE 73.2%. d , Architecture-specific blind spots with largely disjoint failure chemistries.

Figure 3: Adversary strategy comparison (10 configurations, budget = 200). a , CX rate with Wilson 95% CI: all strategies achieve

{>}85\%

against the 93.2% base rate. b , Unique materials discovered: algorithmic strategies find 61–138 unique compositions; LLM adversaries find 5–29 but concentrate on functionally important materials. c , Exploration heatmap: LLMs converge on high-

Z

, multi-element regions (top) while baselines spread uniformly (bottom).

Rank	Formula	Anomaly	Pred. error (eV atom -1 )	Max force (eV Å -1 )	Application
1	DyLi 2 PuF 8	3.49	7.06	75.6	Nuclear fuel (molten salt)
2	Pb 4 Pt 4 O 12	2.97	4.13	107.6	Pt-group catalysis
3	Au 2 Ba 2 Np 2 Se 6	2.70	6.95	44.9	Nuclear waste
4	Au 2 Cs 2 Sc 2 Te 6	2.68	5.36	73.4	Thermoelectric
5	Bi 2 Cu 2 O 4 Te 2 V	2.58	5.69	63.0	Multiferroic
6	Th 2 I 6	2.53	6.07	53.8	Nuclear fuel processing

Table 1: Top 12 DFT-stable/CHGNet-unstable materials, ranked by anomaly score. All have identified functional applications spanning nuclear, electronic, photovoltaic and catalytic domains.

Figure 4: Systematic failure patterns. a , Anomaly distribution: prediction error vs max force for 5,000 WBM materials (grey) with adversarially discovered failures (red). b , Per-element stability disagreement by periodic table block: f-block elements fail most ( $p=0.042$ ). c , JARVIS cross-functional validation: 682 CHGNet blind spots confirmed by independent DFT.

Protocol	Discov.	Missed	False leads	Precision	DFT evals
CHGNet-only	244	244 (50.0%)	63	0.795	0
MACE-only	63	425 (87.1%)	14	0.818	0
Union (no DFT)	253	235 (48.2%)	65	0.796	0
Union + random DFT	296	192 (39.3%)	52	0.850	130
PCM-audited (ours)	306	182 (37.3%)	53	0.852	130

Table 2: Thermoelectric screening case study. Discovery yield across five screening protocols for 647 WBM candidates (488 DFT-stable). PCM-audited screening discovers 62 additional stable thermoelectrics over the CHGNet baseline while reducing false leads, at the cost of 130 DFT evaluations (20% of candidates).

Step	Action
1. Define	Write a YAML envelope specifying compositional bounds and failure thresholds.
	Example: $Z_{\text{max}}\leq 83$ , prediction error $\leq$ 2 eV atom -1 , force $\leq$ 50 eV Å -1 .
2. Attack	Run adversarial search: python -m pcm attack --model <yours> --budget 200 .
	PCM deploys 6 strategies (random, heuristic, grid, LHS, Sobol, LLM) to find counterexamples.
3. Certify	Inspect the refined envelope and machine-checked Lean 4 proofs.
	The proofs certify: if the assumptions hold, then the safety claim follows.

Table 3: Box 1: How to audit your MLIP. Three-step protocol for pre-deployment reliability certification.

Rank	Strategy	CX Rate	95% CI	Entropy (bits)	Unique
1	Gemini 2.5 Pro (LLM)	100.0%	[98.1, 100]	0.000	5
2	GPT-5 (LLM)	100.0%	[98.1, 100]	0.875	6
3	Gemini 3 Flash (LLM)	98.5%	[95.7, 99.5]	0.980	17
4	GPT-5.2 (LLM)	98.5%	[95.7, 99.5]	0.998	29
5	Claude Opus 4.6 (LLM)	88.5%	[83.3, 92.2]	0.986	20
6	Claude Opus 4.5 (LLM)	88.5%	[83.3, 92.2]	1.211	22

Table Extended Data Table 1 : Full adversary strategy comparison (10 configurations, budget = 200). CX rate with Wilson 95% CI, failure mode entropy, and unique materials discovered. LLM adversaries achieve higher CX rates but lower unique discovery counts; algorithmic strategies provide broader coverage. Grid and LHS strategies are omitted as they perform comparably to Random and Sobol at this budget.

#	Formula	Atoms	Pred. err. (eV atom -1 )	DFT $F_{\text{max}}$ (eV Å -1 )	CHGNet $F_{\text{max}}$ (eV Å -1 )	Ratio DFT/CHGNet	SCF	Time (s)
1	Cu 7 Zn 1	8	10.49	557	36	15.4 $\times$	15	180
2	Cd 6 Zr 2	8	10.09	460	28	16.5 $\times$	14	153
3	Ag 6 Cl 2 S 2	10	9.98	1445	39	36.8 $\times$	13	296
4	RuZn 3	4	9.95	89	54	1.6 $\times$	11	22
5	LiO 4 Sc 3	8	9.74	197	22	8.8 $\times$	18	71
6	Cu 6 Mg 2	8	9.68	321	24	13.2 $\times$	14	60

Table Extended Data Table 2 : Independent DFT validation of 20 adversarially discovered materials (QE pw.x v6.7, PAW-PBE, SSSP v1.3.0, 60/480 Ry, 8 cores). All 20 converge (2 require expanded cells on retry). DFT

E

/atom is total energy (including core electrons); CHGNet

F_{\text{max}}

is evaluated on the same golden-ratio structure for direct force comparison. Cu 7 Zn 1 (brass) and Cu 7 Mn 1 (manganese bronze) are industrial alloys where CHGNet underestimates forces by 15–33

\times

Figure Extended Data Fig. 1 : Dual-adversary Venn diagram. Two adversary strategies discover complementary materials with 14.3% overlap (3 consensus materials). Complementary search strategies exploit different regions of compositional space.

Figure Extended Data Fig. 2 : Cross-MLIP adversarial transfer. a , CHGNet $\leftrightarrow$ TensorNet transfer rate heatmap: 97.8% of CHGNet failures also fail on TensorNet. b , Error correlation scatter ( $r=0.69$ ). c , Seeded vs random discovery rates. d , Model-specific blind spots.

Figure Extended Data Fig. 3 : JARVIS-DFT cross-oracle validation. a , CHGNet prediction error vs JARVIS formation energy for 814 matched materials. b , Cross-oracle category counts: 682 CHGNet-only failures. c , Failure overlap Venn diagram. d , Compositional features of disagreement regions: max

Z

(

p=0.002

) and mean atomic mass (

p=7\times 10^{-5}

) significantly higher in CHGNet blind spots.

Figure Extended Data Fig. 4 : Iterative envelope refinement (4 rounds). a , Envelope bounds convergence. b , CX/pass rate evolution. c , Cumulative material discovery. d , Error distribution per round. The safe envelope compresses by 75–91% per feature dimension.

Figure Extended Data Fig. 5 : Element frequency analysis. a , Per-element mean prediction error vs WBM frequency (84 elements, Spearman

\rho=0.443

). b , Stability disagreement by periodic table block: f-block highest (Kruskal–Wallis

p=0.042

). c , Adversarial vs non-adversarial elements (

p=0.020

). Rarest quintile contains 41% adversarial elements.

Figure Extended Data Fig. 6 : Adversarial strategy analysis. Top : Ablation comparing 13 adversary configurations on CX rate vs unique materials discovered (base CX rate = 93.2%; max-everything achieves 100% but discovers only 1 unique material). Bottom : Emergent search behaviour— a , Feature-space autocorrelation. b , Phase transition detection. c , Post-violation exploration (

p=0.0001

Figure Extended Data Fig. 7 : Shuffled-feature ablation. CX rate by condition: control 90%, shuffled 82%, anonymous 88% (Wilson 95% CIs). Incorrect domain knowledge (shuffled) is worse than no knowledge (anonymous), confirming the adversary–oracle separation as the core mechanism.

Figure Extended Data Fig. 8 : Independent DFT validation of adversarially discovered MLIP blind spots (18 materials with identical golden-ratio structures; 2 retry materials excluded from force comparison). a , Maximum forces from Quantum ESPRESSO (DFT) vs CHGNet on the same structures (log scale). DFT forces are systematically larger, confirming CHGNet underestimates instability. b , Force ratio (DFT/CHGNet); median 11.6

\times

. Cu 7 Zn 1 (brass, 15

\times

) and Cu 7 Mn 1 (manganese bronze, 33

\times

) are highlighted. c , SCF iterations to convergence (median 14). d , Wall-clock time per material (total 47 min on 8 CPU cores).

Figure Extended Data Fig. 9 : Representative Lean 4 proof output for the WBM–CHGNet safety certificate (auto-generated from the refined envelope). Top : The core safety module defines compositional bounds ( EnvBounds ), structural requirements ( DesignReq ), and outcome thresholds ( HoldsThresholds ). The oracle_guarantee axiom—the only unverified assumption—states that the MLIP satisfies thresholds within the envelope; a domain expert can inspect whether this assumption is warranted. safe_under_envelope composes these into the safety claim; envelope_non_vacuous provides a constructive witness proving the envelope is non-empty. Bottom : The error propagation module composes DFT accuracy (

\varepsilon_{\text{DFT}}=0.1

eV atom -1 ) with the MLIP threshold via the triangle inequality, making the full approximation chain (reality

\to

DFT

\to

MLIP) explicit and auditable. All proofs are verified by lake build (Lean 4.27.0).

Machine Learning Interatomic Potentials

Machine learning interatomic potentials predict atomic energies and forces for fast simulations of molecules and materials.

See all 91 papers

Risk-Controlled DFT Selection for Machine-Learned Interatomic Potentials
Oct 14, 2026Kun Ryu, Yeo Jin Jung, Shyue Ping Ong +2Selective Prediction Computational Materials Science
Pritzker School of Molecular Engineering, The University of Chicago · Department of Statistics, The University of Chicago · Department of Material Science and Engineering, National University of Singapore
MLIP Detective: Active Failure Mode Discovery Beyond Benchmark Scores for Machine-Learning Interatomic Potentials
Sep 8, 2026Ryuhei Okuno, Nontawat Charoenphakdee, Kaoru Hisama +1AI Agents for Scientific Discovery Machine Learning Interatomic Potentials
Preferred Networks
Knowing when to trust machine-learned interatomic potentials
May 1, 2026Shams Mehdi, Ilkwon Cho, Olexandr IsayevMachine Learning Interatomic Potentials Selective Prediction
Department of Chemistry, Mellon College of Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, 15213, USA. · Department of Materials Science and Engineering, Carnegie Mellon University, Pittsburgh, Pennsylvania, 15213, USA. · Ray and Stephanie Lane Computational Biology Department, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, 15213, USA.

Oct 14, 2026J/K move · Enter open · S save

Risk-Controlled DFT Selection for Machine-Learned Interatomic Potentials

Kun Ryu, Yeo Jin Jung, Shyue Ping Ong, Claire Donnat+1

Pritzker School of Molecular Engineering, The University of Chicago · Department of Statistics, The University of Chicago · Department of Material Science and Engineering, National University of Singapore

Selective Prediction Computational Materials Science Machine Learning Interatomic Potentials

Open paper AskPDF arXiv

Automated materials discovery requires evaluating large pools of candidate configurations, with density functional theory (DFT) as a major throughput bottleneck. Pretrained machine-learned interatomic potentials (MLIPs) approximate DFT cheaply, but their errors vary by orders of magnitude across configurations, making it difficult to decide when to trust the MLIP predictions and when to fall back to DFT. We frame this decision as a risk-controlled selection problem and solve it within a conformal risk control (CRC) framework. Each configuration is mapped from atomic numbers and Cartesian coordinates to a fixed geometric descriptor, which a lightweight predictor uses to estimate an MLIP-DFT disagreement score in energy, average force, and maximum force. CRC then calibrates this score into a selection threshold for DFT labeling such that the MLIP error on the unselected configurations, which keep their MLIP labels, stays below a user-chosen fraction

α

of the expected error. Under an identical guarantee across eight dataset-MLIP pairs, our predictor routes 7% and 14% fewer configurations to DFT at

α=0.3

than committee baselines. Because committee disagreement overlooks errors the MLIPs share, our gains are largest when the DFT labels and MLIP training data differ in DFT functional and basis set, and narrow when the two agree. Without model access, the structure-only predictor also ranks errors as well as the target MLIP's latent representation and outperforms widely used descriptors such as Smooth Overlap of Atomic Positions (SOAP) and Atom-Centered Symmetry Functions (ACSF).

Abstract

Machine Learning Interatomic Potentials

Explore similar work

Risk-Controlled DFT Selection for Machine-Learned Interatomic Potentials

MLIP Detective: Active Failure Mode Discovery Beyond Benchmark Scores for Machine-Learning Interatomic Potentials

Knowing when to trust machine-learned interatomic potentials