Research map / Large language models / Agents, code and math
Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes SPEAC, which designs a Python-subset intermediate language LLMs naturally produce, repairs out-of-language code with MAX-SMT-based compiler techniques and LLM hole-filling, and instantiates it as Eudoxus for the UCLID5 verification language.
Problem
LLMs struggle to generate syntactically valid code in very low-resource programming languages (VLPLs) such as the UCLID5 formal verification language, which are scarce in pre-training data and public examples.
Approach
Use synthetic programming elicitation (grounded-theory analysis of LLM outputs) to pick a parent language (Python) and a child subset that LLMs naturally write, then compile the child subset to the target VLPL, repairing out-of-subset code with largest-consistent-subtree MAX-SMT edits and LLM-filled holes.
Key results
- Eudoxus with GPT-4-turbo parsed 24/33 benchmarks and Eudoxus with GPT-3.5-turbo parsed 28/33, versus at most 4/33 for any baseline.
- Across all 11 baseline variants, programs passed compiler checks for only 6/33 unique problems, versus 30/33 for the two Eudoxus variants combined.
- Of 52 parsed Eudoxus programs, 33 scored 4 or higher on manual semantic correctness; average repair step time was under 2 seconds.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use SPEAC/Eudoxus instead of standard LLM baselines | UCLID5 text-to-code generation · Textbook benchmarks (33) | parse rate: 28/33 vs. 2/33 | Helped |
| Use SPEAC/Eudoxus instead of standard LLM baselines | UCLID5 text-to-code generation · Textbook benchmarks (33) | semantic correctness: 33/52 programs (24 unique problems) scored four or higher | No clear effect |
| Use Eudoxus with GPT3t instead of direct UCLID5 generation | GPT-3.5-turbo-0125 · UCLID5 regression tests (33) | syntactic correctness: 9.1% -> 84.8% | Helped |
| Use Eudoxus with GPT4t instead of direct in-context generation | GPT-4-turbo-2024-04-09 · UCLID5 regression tests (33) | syntactic correctness: 12.1% -> 84.8% | Helped |
Surprising findings
- No LLM produced UCLID5 code that parses in 660 unprompted attempts, while Python code calling a hypothetical API was far more consistent.
Limitations
- Evaluated on only one VLPL (UCLID5).
- Only two LLMs (GPT-3.5-turbo and GPT-4-turbo) were tested.
- Semantic correctness was judged by a single author manually.
Experimental setup
Datasets: UCLID5 regression tests (33 curated, 317 unlabeled) 33 exercises from three textbooks
Benchmarks: 33 UCLID5 textbook exercises
Metrics: parse rate (passes compiler checks) semantic score 1-5 (manual)
Baselines: few-shot prompting few-shot with chain-of-thought fine-tuning self-repair
Builds on: natural programming elicitation Pavlinovic et al. MAX-SMT repair chain-of-thought self-instruct
Closest papers by meaning
- Verified Code Transpilation with LLMs (NeurIPS 2024 · similarity 0.88)
- CodeChemist: Test-Time Scaling for Low-Resource Code Generation via Functional Knowledge Transfer (ICML 2026 · similarity 0.88)
- Training Language Models on Synthetic Edit Sequences Improves Code Synthesis (ICLR 2025 · similarity 0.87)
- How efficient is LLM-generated code? A rigorous & high-standard benchmark (ICLR 2025 · similarity 0.87)
- Beyond Accuracy: Evaluating Self-Consistency of Code Large Language Models with IdentityChain (ICLR 2024 · similarity 0.86)
- Evaluating Program Semantics Reasoning with Type Inference in System $F$ (NeurIPS 2025 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.