# forallutoexistsval: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks

arXiv: https://arxiv.org/abs/2403.18327 · HTML: https://mlsanity.com/paper/2403.18327/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 52 references that are in the map.
- First posted on arXiv 27 Mar 2024.

## Builds on (most cited first, 24 of 24)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [mT5: A massively multilingual pre-trained text-to-text transformer](https://mlsanity.com/paper/2010.11934/) (2020)
- [Code as Policies: Language Model Programs for Embodied Control](https://mlsanity.com/paper/2209.07753/) (2022)
- [A Systematic Survey of Prompt Engineering in Large Language Models: Techniques and Applications](https://mlsanity.com/paper/2402.07927/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [ReClor: A Reading Comprehension Dataset Requiring Logical Reasoning](https://mlsanity.com/paper/2002.04326/) (2020)
- [Leveraging Pre-trained Large Language Models to Construct and Utilize World Models for Model-based Task Planning](https://mlsanity.com/paper/2305.14909/) (2023)
- [CLUTRR: A Diagnostic Benchmark for Inductive Reasoning from Text](https://mlsanity.com/paper/1908.06177/) (2019)
- [Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis](https://mlsanity.com/paper/2304.04675/) (2023)
- [Translating Natural Language to Planning Goals with Large-Language Models](https://mlsanity.com/paper/2302.05128/) (2023)
- [#InsTag: Instruction Tagging for Analyzing Supervised Fine-tuning of Large Language Models](https://mlsanity.com/paper/2308.07074/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [TIM: Teaching Large Language Models to Translate with Comparison](https://mlsanity.com/paper/2307.04408/) (2023)
- [Semantic Parsing with Dual Learning](https://mlsanity.com/paper/1907.05343/) (2019)
- [LangPro: Natural Language Theorem Prover](https://mlsanity.com/paper/1708.09417/) (2017)
- [SAT-Based Synthesis Methods for Safety Specs](https://mlsanity.com/paper/1311.3530/) (2013)

## Built on by (most cited first, 3 of 3)

- [Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition](https://mlsanity.com/paper/2510.06774/) (2025)
- [Adaptive Selection of Symbolic Languages for Improving LLM Logical Reasoning](https://mlsanity.com/paper/2510.10703/) (2025)
- [Natural Language to First-Order Logic LLM-based Autoformalization](https://mlsanity.com/paper/2610.12030/) (2026)

## Abstract (arXiv)

This paper presents forallutoexistsval, a new approach for scaling LLM assessment in translating formal syntax -- such as first-order logic, regular expressions, etc -- to natural language (interpretation) or vice versa (compilation), thereby facilitating their use in applications such as generating/explaining logic and control flow for programs etc. Existing approaches for LLM assessment in these areas require labor-intensive ground-truth creation, the availability of which undermines the separation of training and test sets. Furthermore, such datasets typically include relatively few hand-coded test cases over which LLM accuracy is determined, thus making them inadequate for determining the safety or correctness of their generated outputs. We introduce a new approach that utilizes context-free grammars (CFGs) to generate out-of-distribution datasets on the fly and perform closed-loop testing of LLM capabilities using formal verifiers to guarantee the correctness of LLM outputs without any human intervention. We release our dataset and benchmark as open-source code at urlhttps://github.com/AAIR-lab/auto-llm-assessment. We also conduct an assessment of several SOTA closed and open-source LLMs to showcase the feasibility and scalability of this paradigm. Our experiments reveal that SOTA LLMs are unable to solve the formal translation task adequately.