# Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization

arXiv: https://arxiv.org/abs/2609.34069 · HTML: https://mlsanity.com/paper/2609.34069/

## Key facts

- No citing papers in the map yet (data through 7 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 33 references that are in the map.
- First posted on arXiv 28 Sep 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 15 of 15)

- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [ShinkaEvolve: Towards Open-Ended And Sample-Efficient Program Evolution](https://mlsanity.com/paper/2509.19349/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [An AI system to help scientists write expert-level empirical software](https://mlsanity.com/paper/2509.06503/) (2025)
- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [Program Synthesis from Polymorphic Refinement Types](https://mlsanity.com/paper/1510.08419/) (2015)
- [RLSF: Fine-tuning LLMs via Symbolic Feedback](https://mlsanity.com/paper/2405.16661/) (2024)
- [Program Synthesis using Abstraction Refinement](https://mlsanity.com/paper/1710.07740/) (2017)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [HepLean: Digitalising high energy physics](https://mlsanity.com/paper/2405.08863/) (2024)
- [Equivalence Checking of ML GPU Kernels](https://mlsanity.com/paper/2511.12638/) (2025)
- [MadEvolve: Evolutionary Optimization of Cosmological Algorithms with Large Language Models](https://mlsanity.com/paper/2602.15951/) (2026)
- [Generalizing to new geometries with Geometry-Aware Autoregressive Models (GAAMs) for fast calorimeter simulation](https://mlsanity.com/paper/2305.11531/) (2023)
- [Learning Abstractions for Program Synthesis](https://mlsanity.com/paper/1804.04152/) (2018)
- [CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery](https://mlsanity.com/paper/2608.20686/) (2026)

## Abstract (arXiv)

The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerate legacy code, repair feedback in prompts alone does not prevent subsequent candidates from repeating the same errors. We introduce Certificate-Driven Evolutionary Search (CDES), which extends evolutionary search with enforceable restrictions derived from failed candidates, recorded as certificates of assumptions, checker evidence, and justified restrictions. Its control logic enforces these restrictions through rejection, backtracking, and targeted repair while preserving compatible edits. We apply CDES to CPU-to-GPU translation of two particle-simulation functions from the Geant4 toolkit, evaluated with a harness that goes beyond unit tests to combine formal checks, numerical comparisons, physics checks, and GPU safety tests. Generated implementations achieve 13.78x and 23.54x function-level speedups over CPU code, including data conversion and transfers; for one function, GPU throughput exceeds an expert implementation by 14.9%, reaching 16.1% when complementary components are combined. In an ablation over execution settings, certificate feedback increases the fraction of candidates passing required correctness checks from 55% to 90%.