Reducing bug-triggering programs to their minimal essential form is a fundamental task in debugging language processors such as compilers and interpreters. Existing reduction techniques are limited by their reliance on predefined, syntax-driven transformations that lack semantic understanding of the target program, and by their inability to learn from past reduction experiences. We present a new approach that recasts program reduction as an autonomous reasoning task powered by agentic Large Language Models (LLMs). Instead of applying fixed transformation rules, our method enables an LLM to analyze program semantics, formulate reduction hypotheses, and iteratively refine its approach based on execution outcomes. Successful reduction experiences are further distilled into reusable strategies, allowing the system to continuously improve over time. We realize this approach in PROJ, a framework built around two collaborative components: a reducer agent that performs semantic-aware, case-specific program reduction, and a reflector agent that extracts and accumulates transferable reduction knowledge. Extensive experiments on 90 benchmarks spanning three programming languages show that PROJ consistently produces smaller reduced programs than all existing state-of-the-art reducers while maintaining high efficiency.
This work proposes a hybrid framework that integrates Large Language Models into GP in two complementary roles: as a semantic mutation operator that proposes non-local program rewrites during evolution, and as a post-evolution repair that iteratively refines single failed programs after search terminates.
Woletemaryam Liyew, Dojun Oh, Seokki Lee et al.· Proceedings of the Genetic a...· 0 citations
While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce *Theo*, an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on seven research papers---five from the ACM Symposium on Theory of Computing (STOC) and two recent OpenAI manuscripts---spanning combinatorics, communication complexity, mechanism design, learning theory, number theory, discrete geometry, and graph theory. We successfully formalize their main theorems and proofs and validate the generated formalizations with human experts; notably, two developments require no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv/.
Arshia Soltani Moakhar, Iman Gholami, Max Springer et al.· arXiv.org· 2 citations
Answer Set Programming (ASP) is a declarative formalism widely used in knowledge representation and reasoning for modeling and solving combinatorial problems, yet current Large Language Models (LLMs) often struggle to generate correct programs from natural language specifications. This difficulty stems both from the limited presence of ASP in training corpora and from the strict syntactic and semantic constraints imposed by stable model semantics. We introduce ALM–ASP (Agentic Loop for Modeling in ASP), a multi-agent architecture for automatic ASP modeling grounded in a functional model of language agents equipped with tools and persistent state. ALM–ASP instantiates this model via two interacting agents: a Modeler, which incrementally constructs candidate ASP programs, and a Validator, which assesses their alignment with the original specification and provides feedback for refinement. The agents interact through a shared ASP execution environment backed by the CLINGO engine, yielding an iterative construct–validate loop. An empirical evaluation on a challenging subset of CP–Bench and on problems from recent LP/CP Programming Contests shows that ALM–ASP significantly improves both syntactic validity and end-to-end correctness over general-purpose LLM baselines, and also achieves improved instance coverage compared to the closest agentic alternative, CP–Agent.
L. A. R. Reiners, Alice Tarzariol, Mario Alviano et al.· Proceedings of the TwentyThi...· 0 citations
Large Language Models (LLMs) have been increasingly adopted in Text-to-SQL systems, yet SQL errors remain a major obstacle in real-world Text-to-SQL inference pipelines. Existing SQL correction approaches either rely on large-scale, high-quality training data with substantial overhead, or adopt single-path agentic workflows that are brittle to early mistakes and prone to error propagation. To develop a practical SQL correctness system for industrial scenarios, we present a training-free framework that formulates SQL correction as a plan-guided, tree-structured debugging process. By maintaining multiple correction strategies and enabling backtracking, the framework mitigates error accumulation during iterative refinement. We further integrate execution-based verification and clause-level diagnostic tools to support strategy pruning and precise error localization. We evaluate the system on the BIRD-Critic benchmark and observe consistent accuracy gains over strong LLM backbones and representative agent-based baselines, achieving a 9.42% improvement over the previous state-of-the-art method. The framework is also deployed in the Torch Log Service (TLS) of Volcano Engine to support an online Text-to-TLS API. In production, it improves execution accuracy from 36.77% to 53.61% on real user queries with a representative strong LLM backbone (GPT-5). These results demonstrate the effectiveness and stability of our approach in real-world deployments.
Xinmei Huang, Jie Song, Peng Li et al.· 0 citations
Compiler bugs are pervasive in modern compiler systems, but the test programs that trigger them are often too large for practical debugging. Program reduction addresses this by minimizing test program size while preserving the original bug-triggering behavior. Existing approaches mainly rely on syntax-guided, rule-based deletion strategies that iteratively remove parts of the program in a trial-and-error manner. While effective in reduction quality, these approaches suffer from slow reduction speed. This paper presents SimP, a program reduction framework that combines traditional reduction with LLM-based syntax- and semantic-guided reduction. SimP leverages customized prompt design to guide the reduction process. SimP synergistically combines rule-based and LLM-based reduction stages to optimize the reduction performance. The results show that SimP improves reduction efficiency while achieving comparable reduction quality, with negligible LLM monetary cost.
Yewei Xiong, Xiangyu Gao, Qiaochu Chen et al.· 0 citations
Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs'training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang et al.· 0 citations