The library

Headline result

With RL plus RMaxTS at a sample budget of 32 x 6400 (mixture of two guiding prompts) it reaches 63.5% on miniF2F-test; on the ProofNet test set it reaches 25.3% at a budget of 4 x 6400. The paper calls both new state of the art at publication.

Headline result

The abstract reports 78.1% of formalized past IMO problems proved, MiniF2F saturated, above 50% on PutnamBench, and 5 of 6 IMO 2025 problems fully proved; a separate Seed-Geometry engine handles geometry.

Headline result

Won the DARPA AIxCC final at DEF CON 33 (August 2025) with 392.76 points; the team's paper reports 43 of 70 vulnerabilities found. DARPA's overall figures (all teams): 54 of 63 synthetic vulnerabilities found and 43 patched, 18 real-world bugs found, about $152 average per task.

Headline result

Across four problems (two oscillators, E. coli growth, aluminum stress-strain) with about 2.5K iterations, LLM-SR beat symbolic regression baselines on normalized MSE, most clearly out of domain: for E. coli growth 0.0037 against 1.0141 for the best baseline.

Headline result

On online bin packing, EoH with about 2,000 LLM queries (GPT-3.5-turbo) averaged a 1.18% gap to the lower bound over six test sets, against 2.23% for FunSearch (which the paper says needs around 1 million queries), 4.13% for best fit and 4.51% for first fit. It also reached the best-known tour on three TSPLib instances (pr124, kroA150, u159) and led on Taillard flow-shop sets.

Headline result

On a real quadruped forward-locomotion test (2 m/s target, 5 m track), the best DrEureka policy reached 1.83 m/s and 5.00 m versus 1.32 m/s and 4.17 m for the human-designed setup. The robot also walked atop a real yoga ball for 15.4 seconds on average.

Headline result

On the LeanDojo Benchmark test set, pass@1 is 51.2% (random split) and 26.3% (novel_premises split) with retrieval, versus 47.6% and 23.2% without retrieval and 29.0% and 7.4% for zero-shot GPT-4. Also 26.5% on miniF2F and 13.8% on ProofNet (pass@1, 10 minute wall-time limit per theorem).

Headline result

With Llama 3.1 70B and no model fine-tuning, verified-code generation reaches 32.9% on HumanEval-Verus and 65.7% on MBPP-verified (pass@256), versus 27.1% and 35.9% for GPT-4o and 11.8% and 26.9% for Llama 3.1 70B.

Headline result

Goedel-Prover-SFT reaches 57.6% Pass@32 on miniF2F, 7.6 points above DeepSeek-Prover-V1.5-RL; the paper's abstract reports over 60% Pass@32 after RL including DPO, 7 PutnamBench problems at Pass@512, and proofs for 29.7K Lean Workbook problems versus 15.7K for prior provers.

Headline result

Reaches 72.95% on the miniF2F test set as an accumulative score; the single-run figure is 70.83% +/- 0.89 at a budget of 2048 x 2 x 600 (Lean 4.7.0). The authors say this shows plain best-first search can compete when scaled.

Headline result

In the paper's computational study on c-Abl kinase, the model learned to generate molecules similar to FDA-approved inhibitors without being shown them and reproduced two exactly (imatinib and bosutinib after five iterations). The method was also applied to the HNH domain of Cas9, which has no commercial small-molecule inhibitors.

Headline result

Google's page reports 14 of 31 tested OSS-Fuzz projects compiled new targets and increased coverage (gains 0 to 31%; tinyxml2 line coverage 38% to 69%), and a similar target in OpenSSL rediscovered CVE-2022-3602.

Headline result

ShinkaEvolve found a circle-packing (n=26) solution with sum of radii 2.63598 under its relaxed verifier, beating AlphaEvolve's reported solution within 150 program evaluations. It also improved ALE-Agent solutions on ALE-Bench by about 2.3% on average over 10 tasks, designed an AIME agent scaffold (gpt-4.1-nano, 7 LLM calls), and found a new mixture-of-experts load-balancing loss.

Headline result

Across six combinatorial problems (TSP, CVRP, OP, MKP, BPP, DPP), with a budget of 100 heuristic evaluations and GPT-3.5 Turbo, ReEvo beats EoH on sample efficiency in five problems, and designed heuristics improved neural solvers, for example POMO's TSP1000 gap from about 52% to 29%. Its genetic algorithm for decap placement scored 12.98 vs 12.41 for the expert-designed one.

Headline result

The project reports 2-3x speedups on GPU kernels (MLX Metal) and a circle packing for n=26 that its README calls state of the art, plus sorting and signal-processing examples. These are the project's own claims; the README gives no numeric circle-packing score.

Headline result

The paper reports that for three base models (MiniMax M2.5, Qwen3.5-35B-A3B, GLM-5) across three benchmarks (Terminal-Bench-2.0, SWE-bench Verified, AppWorld) every final harness improves both held-in and held-out pass rates, with relative gains of up to 132%. On Terminal-Bench-2.0 held-out, MiniMax M2.5 went 40.5% to 61.9% and Qwen3.5-35B-A3B 23.8% to 38.1%.

Headline result

For a 350 GPa bulk modulus target, in a range sparse in the training data, three active learning iterations lowered the mean absolute percentage error of generated crystals from about 0.4 to 0.2 (CGCNN-evaluated). DFT bulk moduli of new structures averaged 343.54 GPa (standard deviation 27.20) after the first iteration and 356.52 GPa (standard deviation 18.61) after the second.

Headline result

Over 80 iterations, the best agent rose from 20.0% to 50.0% on SWE-bench (Verified) and from 14.2% to 30.7% on Polyglot (abstract figures; the paper's Section 4.4 gives 14.0% as the Polyglot start).

Headline result

Generated esmGFP, a glowing fluorescent protein sharing only 58% sequence identity with the closest known fluorescent protein (~500 million years of evolutionary divergence).

Headline result

Solved >95% of TravelPlanner and Natural Plan multi-constraint benchmarks with Gemini 1.5 Flash, surpassing Best-of-N and sequential Reflexion by wide margins.

Headline result

On 200 Level 1 and 2 KernelBench tasks the average speedup was 3.13x, falling to 1.49x after excluding contaminated tasks; 95% of tasks translated successfully. On twelve robust-kbench tasks forward kernels reached up to 2.5x over PyTorch eager.

Headline result

In simulated household, chip-design and navigation scenarios, success rates with GPT-4o were 91.65%, 91.60% and 83.69%, against 56.67%, 61.29% and 50.00% for AutoTAMP with GPT-4o. The authors claim a 30 to 40% improvement.

Headline result

Discovered agent architectures that outperform hand-designed baselines by up to 13.6 percentage points on ARC logic tasks and transfer across foundation models.

Headline result

Achieved 76.4% PoseBusters accuracy on protein-ligand complexes, far surpassing classical physics-based docking tools.

Headline result

Reported to significantly outperform state-of-the-art LLM-based approaches on the LPWP and ComplexOR operations research benchmarks.

Headline result

Covered 47.6% more state transitions and 29.6% more code branches than AFLNet across nine network protocol implementations, discovering 9 previously unknown vulnerabilities.

Headline result

Autonomously planned and executed wet-lab syntheses of an insect repellent, three organocatalysts, and a novel chromophore.

Headline result

Rediscovered unseen experimental crystal structures and identified novel stable inorganic phases validated by ab initio DFT.

Headline result

Nearly 90% of sampled structures pass geometric and charge-neutrality checks, and a high fraction relax to metastable or stable states in DFT.

Headline result

Verified 68% of the 782 ground-truth formal verification programs in DafnyBench via multi-turn compiler feedback.

Headline result

Generated pocket-specific 3D ligands with stronger Vina binding scores and drug-likeness than autoregressive 3D baselines on CrossDocked2020.

Headline result

Achieved 36.8% higher line coverage than language-specific fuzzers across 9 systems in 6 languages and found 98 bugs (64 confirmed previously unknown).

Headline result

Reached 65.9% pass@64 on miniF2F-test and 54.5% on ProofNet, and proved 177 PutnamBench problems in Lean 4.

Headline result

Recovered significantly more exact ground-truth physical laws on the Feynman Symbolic Regression Benchmark than standalone PySR or LLM-only baselines.

Headline result

Improved miniF2F-test pass@64 in Lean from 30.8% to 46.3%, outperforming tactic-only search baselines.

Headline result

Outperformed Gaussian Process and Random Forest Bayesian Optimization baselines in the low-trial regime across 25 Bayesmark tasks.

Headline result

On 13 real-world JavaScript packages, produced mutants resembling real bugs that StrykerJS, a state-of-the-art mutation testing tool, cannot produce.

Headline result

Topped the Matbench Discovery leaderboard for predicting stable inorganic crystals at 3-6x higher relaxation speed than prior equivariant potentials.

Headline result

Outperformed GPT-4 across NL4Opt, MAMO, and IndustryOR benchmarks using a 7B open-weight model paired with the COPT solver.

Headline result

Searched a combinatorial space of 30 billion synthesizable molecules to discover 6 structurally novel compounds with potent wet-lab antibacterial activity against A. baumannii.

Headline result

Designed novel Mycobacterium tuberculosis ClpP inhibitors validated in wet-lab assays with strong enzymatic inhibition (IC50 = 0.9 uM).

Headline result

Proved 47.9% of theorems in the Isabelle Archive of Formal Proofs benchmark (65.7% when combined with Thor Sledgehammer).

Headline result

Designed 310 proteins across point-group symmetries, programmable shapes, and protein classes, with crystallographic structures matching design to 1.0-1.4 Angstrom backbone RMSD.

Headline result

Accepted 87% of correct Dafny programs while rejecting all of adversarial incorrect synthesis candidates on the CloverBench suite.

Headline result

Autonomously executed Suzuki-Miyaura and Sonogashira cross-coupling reactions on cloud lab hardware and ran an optimization study that selected conditions against previously collected, fully mapped yield datasets.

Headline result

Outperformed USPEX evolutionary crystal search and CDVAE on MP-20 and Perov-5 crystal structure prediction at a fraction of the compute time.

Headline result

Outperformed human-engineered and gradient-free prompt baselines by up to 25% across 31 NLP and reasoning datasets.

Headline result

Discovered prompts that boosted GSM8K accuracy by up to 8 percentage points over human baselines and solved small-scale TSP and linear regression trajectories.

Headline result

Outperformed Chain-of-Thought, Plan-and-Solve, and OPRO across arithmetic, commonsense, and hate-speech classification benchmarks.

Headline result

Improved pass@1 by up to 12 percentage points across TransCoder C++-to-Python translation, Spider text-to-SQL, and MBPP Python synthesis.

Headline result

Achieved 50.84% (PyTorch) and 30.38% (TensorFlow) higher code coverage than state-of-the-art DL fuzzers and detected 65 bugs (41 confirmed previously unknown).

Headline result

Significantly improved symbolic equation recovery and extrapolation R^2 on SRBench and Feynman physics datasets over beam search or sampling.

Headline result

Unlocked 3.3x more unique items, traveled 2.3x longer distances, and reached key tech-tree milestones up to 15.3x faster than prior agent baselines.

Headline result

Placed in the top 54.3% of human participants across 10 recent Codeforces competitions, the first AI system to reach competitive human rank.

Headline result

Generated valid periodic crystal structures across carbon, perovskite, and Materials Project benchmarks with high structural and compositional validity.

Headline result

Executed spatial-geometric manipulation, drawing, and tabletop rearrangement tasks on physical Franka Panda and UR5e robot arms without task-specific training.

Headline result

Raised pass@1 on HumanEval to 65.8% (+18.8 points over Codex greedy decoding) and improved MBPP and APPS accuracy by over 15 points.

Headline result

Solved 39.3% of miniF2F test theorems in Isabelle/HOL, a more than 10 percentage point jump over prior direct tactic-generation baselines.

Headline result

Solved 82.6% of Metamath set.mm test theorems and 41.0% of miniF2F-curriculum theorems in Lean, discovering shorter proofs than human ground truth.

Headline result

Generated drug-like 3D molecules with more realistic torsion angles and stronger Vina binding scores than 3D voxel baselines on CrossDocked2020.

Headline result

Achieved 52.4% native sequence recovery (vs. 32.9% for Rosetta) and rescued previously failed de novo protein cyclic oligomers, nanoparticles, and binders in wet-lab crystallography.

Headline result

Executed 101 real-world mobile manipulation tasks in an office kitchen with 84% planning rate and 74% physical execution success.

Headline result

Eliminated syntax, type, and scope errors across SQL, Vega-Lite visualization specs, and calendar DSLs while boosting execution accuracy.

Headline result

Boosted T5-3B exact-match and execution accuracy on Spider and CoSQL benchmarks by 4-7 percentage points and eliminated 98% of syntax and schema errors.

Headline result

For unit-load pre-marshalling, Qwen2.5-Coder:32b-generated heuristics solved 30 of 30 held-out instances (seeds 10-39) against 27 of 30 for the "Optimal A*" baseline. For the sliding puzzle they solved 10 of 10 on seeds 0-9 against 5 of 10 for Hybrid A* and for "Optimal A*".

Headline result

On two coupled problems (inventory routing, and multi-robot multi-bay pre-marshalling) with Qwen3-coder:30b, the sequential and iterative strategies converged more stably than the integrated one. On inventory routing the mean relative gap was 0.0429 (sequential), 0.0433 (iterative), 0.0537 (integrated).

Headline result

At equal generation counts (100 generations), the evolved memetic algorithm reached 11.423 bit/s/Hz at 1 W (7.6% over a conventional GA) and 23.611 bit/s/Hz at 5 W (8.2% over a conventional GA), and about 4 to 6% above the two LLM-assisted GA baselines.

Headline result

In a preregistered seed-paired comparison at 400 total LLM calls on online bin packing, the HoxLM configuration won 9 of 10 runs against EoH, with a median sealed excess of 0.836% against 3.912%.

Headline result

The paper reports 67 problems across analysis, combinatorics, geometry and number theory. AlphaEvolve rediscovered the best known solutions in most cases and found improved ones in several, for example an autocorrelation upper bound reduced from 1.5708 to 1.5032 and a finite field Kakeya construction of size 1/4 p^3 + 7/8 p^2 - 1/8 for primes p = 1 mod 4.

Headline result

A Qwen2.5-7B-Instruct model (INT4, on a single 24GB GPU) with GRPO fine-tuning reached an average 0.71% gap on online bin packing, against 0.89% for MCTS-AHD and 2.40% for Best Fit, and beat the best listed competitor on CVRP (3.95% vs 4.70%) and OP (12.58% vs 16.34%) at N=200 in the paper's tables.

Headline result

For unit-load pre-marshalling, Qwen2.5-Coder:32b with CEoH reached a fitness of 12.5% (best overall), against 14.3% for the best EoH run (GPT-4o 2024-08-06). The "Optimal A*" baseline scored about 8.1%. CEoH outperformed EoH for Gemma2:27b, Qwen2.5-Coder:32b and DeepSeekV3:685b.

Headline result

In a bioRxiv preprint, on rat choices in a 2-armed drifting bandit task (data from Miller et al. 2021), CogFunSearch reliably found programs that beat the best existing cognitive model the authors compared against, both when improving supplied programs and when starting from scratch.

Headline result

Discovered acquisition functions that outperform Expected Improvement (EI) and Upper Confidence Bound (UCB) on unseen black-box optimization and HPO benchmarks.

Headline result

Generated average formation energy fell over five iterations (means -1.14, -2.03, -2.93, -3.56, -3.77; units not stated in the text). The authors report 1,598,551 materials with Ehull below 50 meV, and Li2AuH6 as a conventional superconductor with a transition temperature of about 140 K from first-principles electron-phonon calculations. Crystal structure prediction RMSE is 0.0423 angstrom, reported as a 32.96% improvement over existing generative models.

Headline result

Outperforms hand-crafted and automated workflow baselines by 5.7% average across six coding and math benchmarks while enabling smaller models to beat GPT-4o.

Headline result

Achieved state-of-the-art thermodynamic stability and 3x faster integration steps than diffusion baselines on MP-20 and MPTS-52.

Headline result

The authors propose two diversity metrics and use them to compare FunSearch, EoH and ReEvo. They report EoH has higher diversity but unstable scores, ReEvo has good scores but poor diversity, and that HSEvo reaches high diversity and good objective scores while staying cost-effective.

Headline result

Automates proof goals directly inside Lean 4 workflows with 3.8x faster tactic inference than Python RPC bridges.

Headline result

Solved 43% of Codeforces Division 1+2 problems and ranked at the 85th percentile of human competitors.

Headline result

Raised miniF2F-valid pass@100 to 57.0% and miniF2F-test to 50.0% in Isabelle/HOL, accumulating thousands of reusable verified lemmas.

Headline result

Zero-shot execution of 25 everyday manipulation tasks across real-world and simulated robot arms with 88% success, plus online adaptation to moving obstacles.

Headline result

On the authors' benchmark tasks, compared with REINVENT, optimization ability improved about 1.5-fold and sample efficiency about 45-fold, and Augmented Hill-Climb outperformed the other reinforcement learning strategies tested on six tasks.

Headline result

In a factor Xa case study, docking followed by RFXscore gave the best results, especially when diverse structures fitting a binding site were wanted; RFXscore plus the factor Xa model left the most compounds after MM/GBSA and other filters. RFXscore had a test r2 of 0.494 and MAE of 1.086.