AI as a research partner: Advancing theoretical computer science with AlphaEvolve

• source_url: https://research.google/blog/ai-as-a-research-partner-advancing-theoretical-computer-science-with-alphaevolve/
• published: 2025-09-30
• authors: Ansh Nagda, Abhradeep Thakurta, and Prabhakar Raghavan
• source: Google Research Blog

Extracted article text

Recently, large language models (LLMs) have demonstrated surprising capabilities in competitive mathematics and competitive programming, demonstrating world-leading performance across both of these fields. However, their successes in mathematical discovery — proving novel theorems or uncovering new combinatorial structures — have been relatively few. Since mathematics and theoretical computer science demand absolute correctness, any AI-based method that makes mathematical discovery must either have a proof of correctness that can be confirmed computationally without human involvement, or have a domain-expert human in the loop to certify correctness.

In the paper “Reinforced Generation of Combinatorial Structures: Applications to Complexity Theory,” the authors demonstrate how an LLM-powered coding agent can help discover new mathematical structures that push the boundaries of complexity theory. The work uses AlphaEvolve, a Google DeepMind system that uses LLMs to iteratively evolve code. AlphaEvolve starts with populations of code snippets, evaluates the structures produced by those snippets, and uses an LLM to morph the most successful snippets toward better solutions. This produced new results in two areas: improving the state of the art for the inapproximability of MAX-4-CUT, and tightening bounds on the average-case hardness of certifying properties of random graphs.

AI-assisted mathematical research can operate in two modes: a person can invoke an LLM to summarize literature, plan research toward new theorems, or generate proof material; or a person can use AI-derived tools such as AlphaEvolve to generate better proof elements. This work uses the second mode, obtaining proof elements that can be automatically verified by a computer program.

The power of lifting: From finite constructions to universal statements

A fundamental challenge in using AI for theoretical computer science research lies in the universal nature of the problems studied. An AI system might find a solution to one instance of a problem, while computer scientists often seek theorems that hold universally for all problem instances and sizes.

The approach uses a technique known as “lifting.” If a proof is viewed as a long string, a finite structure within the proof can be evolved to support a stronger universal statement while keeping the interface to the rest of the proof intact. To certify overall correctness, researchers only need to certify the correctness of the evolved finite structure.

In complexity theory, researchers often use established proof frameworks that rely on specific, highly optimized finite structures. A better structure can therefore lift to a better universal result. One example is a gadget reduction: a finite recipe for locally transforming a small piece of a known hard problem into a piece of a target problem. Finding the optimal gadget is a painstaking process often done by hand.

By tasking AlphaEvolve with finding better gadgets, the researchers discovered structures more complex than those previously known. When plugged into existing mathematical frameworks, these finite discoveries immediately yielded new universal theorems in complexity theory.

New theorems in complexity theory

The methodology was applied to MAX-k-CUT, where the goal is to partition a graph’s nodes into k sets while maximizing the number of crossing edges. Because the problem is NP-hard, the researchers focused on approximation algorithms and the limit of approximation.

MAX-4-CUT: A new state of the art

For MAX-4-CUT, the previous best-known result showed that it was NP-hard to approximate the solution within a factor of 0.9883. AlphaEvolve searched for a new gadget reduction and discovered an intricate gadget involving 19 variables with a complex weighting scheme, with some connections weighted up to 1,429 times more than others. This established a new inapproximability bound of 0.987.

Although the improvement may appear incremental, advances of this kind in the mature field of hardness of approximation often require significant new techniques or combinatorial insights.

Average-case hardness and Ramanujan graphs

The researchers also studied the hardness of problems on average rather than in the worst case, including the difficulty of certifying bounds on MAX-2-CUT and maximum independent set in sparse random graphs. Prior work used computer assistance to find relevant graphs on up to 10 nodes. AlphaEvolve navigated the search space and discovered Ramanujan graphs with larger cuts on as many as 163 nodes.

These discoveries significantly improved lower bounds for average-case hardness. Combined with new non-AI algorithmic progress, they nearly settled the computational hardness of these questions, matching upper and lower bounds to within the third decimal place.

The crucial role of verified correctness

A critical distinction of this work is that the results come with proofs of correctness. When an LLM is prompted to generate a mathematical proof directly, it often produces a proof sketch or an argument that requires substantial human intervention to verify. Hallucinations or subtle errors can render the output useless, while mathematics requires absolute correctness.

In contrast, this approach uses AI to discover a structure within the proof, not the proof itself. The validity of the final theorem relies on the correctness of the lifting framework and verification of the discovered structure. Verifying the structures discovered by AlphaEvolve is computationally intensive.

AlphaEvolve achieved a 10,000x speedup in the verification process by implementing branch-and-bound strategies and system-level optimizations. The final gadgets were still verified using the original brute-force algorithm, ensuring the absolute correctness of the theorems.

The future of AI-assisted theory

While these initial findings are far from conclusive, they suggest that AI can become a helpful collaborator in mathematical discovery. As proofs may increasingly be attributed to AI, verification is likely to become a significant bottleneck.

Acknowledgments

The authors thank Adam Zsolt Wagner, Swarat Chaudhuri, Pasin Manurangsi, and Sushant Sachdeva for helping during various stages of the project.