SolEvolve: LLM-driven evolutionary search for SAT-verified constructions in discrete mathematics
- 주제(키워드) large language models , SAT solving , algorithm portfolios , error- correcting codes , Latin squares , self-orthogonal embeddings , genetic algorithms
- 발행기관 서강대학교 일반대학원
- 지도교수 Jon-Lark Kim
- 발행년도 2026
- 학위수여년월 2026. 2
- 학위명 석사
- 학과 및 전공 일반대학원 수학과
- 실제URI http://www.dcollection.net/handler/sogang/000000082888
- UCI I804:11029-000000082888
- 본문언어 영어
- 저작권 논문은 저작권에 의해 보호받습니다.
초록(요약문)
This study presents an end-to-end framework for automated algorithm dis- covery driven by large language models (LLMs). The system integrates SAT solving, integer-linear programming (ILP), evolutionary search, and agentic workflows to explore mathematical structures. Starting from natural-language design sketches produced through dialogue with LLMs, the framework distills these ideas into modular Python components for encoding binary linear codes, mutually orthogonal Latin squares, and Lucas cube partitions. The LLM- generated encoders yield substantial structural reductions, including standard- form simplifications, linear-size sequential counters, and compact XOR encod- ings, which in turn reduce variable and clause counts and make larger instances tractable for standard SAT and ILP solvers. Leveraging these encodings, the framework rapidly rediscovered benchmark codes with parameters [32, 14, 8] and produced new inequivalent [43, 10, 16] codes with improved weight-16 counts. The same templates also produced Commander encodings for 10 × 10 MOLS, an ILP model proving a 15-center perfect partition of the 7-dimensional Lucas cube Λ7(14), and a rank-one elimi- nation method yielding minimal self-orthogonal embeddings that generate self- dual codes of lengths 22, 52, and 114. These experiments indicate that LLMs can reliably act as planners and coders within compositional search pipelines, while SAT/ILP solvers provide formal guarantees. With solver-level proof artifacts, systematic verification, and transparent logging, the framework shows how LLM–human collaboration can support mathematically rigorous, reproducible discoveries across multiple discrete domains.
more목차
1 Introduction 5
2 The SolEvolve framework 10
2.1 Architecture overview 10
2.2 System data flow 12
2.3 LLM-driven encoding strategies 12
2.4 Verification and bounds analysis 14
3 Discovery of binary linear codes 15
3.1 Preliminaries 15
3.2 Algorithm design for binary codes 17
3.3 Experimental results and analysis 18
3.4 Hybrid search and repair methods 21
4 Self-orthogonal embeddings 25
4.1 Preliminaries 25
4.2 Rank-one elimination algorithm 27
4.3 SAT-based self-orthogonal embeddings 30
5 Perfect partitions in generalized Lucas cubes 34
5.1 Preliminaries 34
5.2 Main results 36
5.3 Construction and non-existence results 39
5.4 Syndrome shift construction and non-linear codes 41
5.5 The Λ31(128) conjecture and obstruction 42
6 Mutually orthogonal Latin squares 43
6.1 Preliminaries 43
6.2 SAT-based construction of orthogonal pairs 45
6.3 Advanced search strategies for higher orders 47
7 Discussion 49
8 Conclusion 51
