Combinatorial and optimization problems are fundamental to many industrial AI applications. Solving large-scale real-world instances of such problems typically requires careful problem formalization, specialized solvers, and expert-designed heuristics. Thus, experts need to specify not only what solutions are, but also how they are derived. By introducing the tool CHECKMATE, we show that algorithm generation via code evolution represents a paradigm shift by eliminating the need to formulate the how. CHECKMATE solely relies on the what. Specifically, a formal specification ensures solutions' correctness and enables systematic performance evaluation of the generated programs, while a natural language description guides the evolutionary process. The effectiveness of our method is demonstrated on selected problems from two industrial domains: configuration and scheduling. In all cases, the evolved algorithms consistently outperform state-of-the-art solvers. This underscores the potential of formal methods in guiding code evolution for automatically solving complex real-world problems.

翻译：组合与优化问题对众多工业AI应用至关重要。求解此类大规模现实世界问题通常需要严谨的问题形式化、专用求解器以及专家设计的启发式算法。因此，专家不仅需要指定解是什么，还需说明解是如何得出的。通过引入CHECKMATE工具，我们证明基于代码演化的算法生成代表了一种范式转变——它消除了对"如何求解"进行形式化的需求。CHECKMATE仅依赖"求解什么"：具体而言，形式化规范确保了求解的正确性，并支持对生成程序进行系统性性能评估；而自然语言描述则引导演化过程。该方法在工业领域选定的配置与调度问题中验证了有效性。在所有案例中，演化生成的算法均持续优于最先进的求解器。这凸显了形式化方法在引导代码演化以自动解决复杂现实问题方面的潜力。