Fully Computer-Assisted Proofs in Extremal Combinatorics
Authors: Olaf Parczyk, Sebastian Pokutta, Christoph Spiegel, Tibor Szabó
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present a fully computer-assisted proof system for solving a particular family of problems in Extremal Combinatorics. Existing techniques using Flag Algebras have proven powerful in the past, but have so far lacked a computational counterpart to derive matching constructive bounds. We demonstrate that common search heuristics are capable of finding constructions far beyond the reach of human intuition. ... The upper bounds for all three problems were found using search heuristics by restating the search for these constructive bounds as discrete optimization problems. ... We implemented all search methods in Python 3.8 and logged the results using Weights & Biases (Biewald 2020). |
| Researcher Affiliation | Academia | 1 Freie Universit at Berlin, Institute of Mathematics, Berlin 2 Technische Universit at Berlin, Institute of Mathematics, Berlin 3 Zuse Institute Berlin, Department for AI in Society, Science, and Technology, Germany |
| Pseudocode | No | The paper describes the search algorithms (Simulated Annealing, Tabu Search) in narrative text but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states 'by making our results and tools available to the research community' but does not provide a specific link to source code for the described methodology, nor does it state the code is in supplementary materials. |
| Open Datasets | No | The paper focuses on finding mathematical constructions (graphs) using computational search heuristics, rather than training on or evaluating against traditional publicly available datasets. It does not mention any external dataset sources or links. |
| Dataset Splits | No | The paper does not describe dataset splits for training, validation, or testing, as it focuses on computational search for mathematical constructions rather than traditional machine learning experiments on empirical datasets. |
| Hardware Specification | No | The paper does not specify any particular hardware (GPU, CPU models, memory, or cloud resources) used for running the experiments. |
| Software Dependencies | Yes | We implemented all search methods in Python 3.8 and logged the results using Weights & Biases (Biewald 2020). We also relied on the GAP (GAP) component in Sage Math for the computations required for the Cayley graphs. |
| Experiment Setup | Yes | Simulated Annealing (SA) was originally proposed by Kirkpatrick, Gelatt Jr, and Vecchi (1983) and is a probabilistic technique that can be interpreted as a modified local search, that attempts to avoid getting trapped in a local minimum early on while still ultimately being driven to better and better states. To more precisely describe SA, let c : 0, 1N R denote some cost function we are trying to minimize and N : {0, 1}N P({0, 1}N) some notion of neighborhoods of the states. We restricted ourselves to considering states as neighboring if their Hamming distance is 1. The algorithm starts with a randomly initialized state s0 and then executes a fixed number of iterations I where in each iteration 1 i I it picks a candidate state sc uniformly at random from N(si 1) and accepts it as si with probability min(1, exp((c(si 1) - c(sc))/ti)) where (ti)1 i I is a sequence of decreasing temperatures in R>0. A common choice for (ti)1 i I consists of linearly decaying it from some tuned initial value to 0 over the runtime of the algorithm. |