$\forall$uto$\exists$$\lor\!\land$L: Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks
Large Language Models;Logical Reasoning;Autoformalization;Informalization;Formal Translation;Truth Maintenance
Yes
No ethics review needed.
1. How diverse can the generated dataset be ?
2. How do you ensure that duplicate data points won’t be there ? I.e data points with very close similarity or minute changes or only change in vocabulary while the logic statement is same 
3. Would love to know how LLMs with tools work as verfiers
1. LLMs can be now tested on dynamic data generated by this framework for Formal Syntax
2. Their method has better indication of accuracy than other metrics for the LLM performance on various FOL. 
3. Very good experimentations , dataset size and presentation
The paper presents a new approach to evaluate and benchmark LLMs on formal syntax. The authors suggest using CFGs to generate synthetic data for testing the LLMs, they utilize formal verifiers to verify the logic.

Contributions:
1. A new method to evaluate LLMs on formal syntax without using static datasets by generating synthetic data using CFGs and adding vocabulary using another LLM
2. Their method has better indication of accuracy than other metrics for the LLM performance on various FOL.
1. Explanation on how the generated dataset is having diverse data points or quality is missing.
Yes
No ethics review needed.
1. The article mentions using context-free grammars (CFGs) to generate datasets dynamically. How does this method ensure diversity and balance at different difficulty levels? Specifically in fields like logic and regular expressions, how does it ensure comprehensive coverage of various possible syntactic structures while maintaining a balanced sample size for each structure type?

2. The article evaluates whether LLMs can act as verifiers to assess the equivalence of formal grammar expressions and finds that even the most advanced LLMs struggle with this role. In the evaluation process, in which types of logical structures or specific conditions do LLMs perform the worst? Are there specific logical structures or syntactic features that make it difficult for LLMs to accurately judge equivalence?
1. The article introduces the ∀UTO∃∨∧L benchmark as an innovative evaluation framework that can automatically assess the ability of large language models (LLMs) to maintain truthfulness in formal tasks. Its practicality lies in dynamically generating datasets, reducing the need for manual annotation, and providing an evaluation method without human intervention.
2. The ∀UTO∃∨∧L framework is designed to be flexible, allowing it to be extended to any formal grammar category that uses syntax and accepts equivalence checks.
3. The article demonstrates the correlation between the results of ∀UTO∃∨∧L and other existing benchmarks, indicating that ∀UTO∃∨∧L can serve as an effective alternative or complementary tool.
The ∀UTO∃∨∧L method evaluates the ability of LLMs to maintain truthfulness in formal tasks by dynamically generating datasets, utilizing the models' automatic formal and informal processing capabilities, and using formal verifiers. This approach allows for automated, human-free evaluation and can be extended to any formal grammar category that uses syntax and accepts equivalence checks. The authors demonstrate the effectiveness of ∀UTO∃∨∧L as an evaluation framework through empirical studies, revealing the limitations of current state-of-the-art models in maintaining truthfulness in formal tasks. By comparing it with existing benchmarks, the article highlights the practicality and importance of ∀UTO∃∨∧L in evaluating LLMs.
1. ∀UTO∃∨∧L relies on existing formal verifiers and parsing libraries to ensure evaluation accuracy. This means its reliability depends on the performance and accuracy of these tools, and any errors in them could affect the evaluation results of ∀UTO∃∨∧L.

2. While ∀UTO∃∨∧L reduces the need for manual annotation, generating dynamic datasets and performing formal verification may require significant computational resources, especially for large-scale datasets and complex logical structures.
Yes
No ethics review needed.
- Given that formal verifiers are central to your evaluation process, how do you handle cases where the verifier fails or produces ambiguous results? Are there fallback mechanisms in place?
- Can your dynamic dataset generation approach be extended to more complex natural language tasks that do not rely on formal syntax? If so, how would this impact the scalability and performance of your evaluation framework?
- What steps have you taken to ensure that your benchmark remains relevant as LLMs evolve? Specifically, how do you plan to update the benchmark as new models with different architectures or capabilities are developed?
- In your empirical analysis, how many different LLMs were tested? It would be useful to know whether your results generalize across a broad range of models or are specific to a few.
- The use of CFGs to dynamically generate out-of-distribution datasets is a significant strength.
- The use of formal verifiers to check the semantic equivalence of LLM outputs is a good method that avoids brittle syntactic checks. This allows for a more robust evaluation of truth maintenance across different formal syntaxes.
The paper introduces autoeval benchmark, designed for the autonomous evaluation of LLMs in formal tasks like truth maintenance and logical reasoning. The benchmark offers several features, such as dynamic dataset generation using CFGs and the use of formal verifiers to assess correctness. The authors argue that their approach mitigates common issues in existing benchmarks, like overfitting to static datasets, and provides a scalable method for evaluating LLMs without relying on human annotations. Empirical results show that performance on this benchmark correlates well with other established benchmarks.
- While the paper focuses on formal tasks like truth maintenance and logical reasoning, it remains unclear how well the proposed benchmark generalizes to less structured or more complex natural language tasks. The reliance on formal verifiers may limit its applicability to broader LLM use cases, such as creative writing or conversational AI, where formal correctness is less critical.
- Informalization, the process of converting formal syntax into natural language, is inherently ambiguous. The paper does not thoroughly address how it handles cases where multiple valid informalizations exist. This could lead to inconsistent evaluations when different LLMs produce semantically equivalent but syntactically different outputs.
- Weak evidence for the robustness of this method. While the paper claims that performance on autoeval correlates well with other benchmarks, the empirical validation seems somewhat limited. I would suggest that the authors test their method on a larger set of models. The current correlation results, while promising, could be influenced by noise or outliers, especially given the relatively small number of models tested, they might not be robust enough to generalize across different architectures or configurations. By increasing the number of models tested (e.g., to 50+), the authors could reduce the impact of potential outliers and noise in the data.
An automatic and scalable benchmark for evaluating LLMs for truth maintenance w.r.t. formal syntax.
@inproceedings{
anonymous2024forallutoexistslorlandl,
title={\${\textbackslash}forall\$uto\${\textbackslash}exists\$\${\textbackslash}lor{\textbackslash}!{\textbackslash}land\$L: Autonomous Evaluation of {LLM}s for Truth Maintenance and Reasoning Tasks},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=iv1TpRCJeK},
note={under review}
}
This paper presents $\forall$uto$\exists$$\lor\\!\land$L, a novel benchmark for scaling Large Language Model (LLM) assessment in formal tasks with clear notions of correctness, such as truth maintenance in translation and logical reasoning.  $\forall$uto$\exists$$\lor\\!\land$L is the first benchmarking paradigm that offers several key advantages necessary for scaling objective evaluation of LLMs without human labeling: (a) ability to  evaluate LLMs of increasing sophistication by auto-generating tasks at different levels of difficulty; (b) auto-generation of ground truth that eliminates dependence on expensive and time consuming human annotation; (c) the use of automatically generated, randomized datasets that mitigate the ability of successive LLMs to overfit to static datasets used in many contemporary benchmarks. Empirical analysis shows that an LLM's performance on $\forall$uto$\exists$$\lor\\!\land$L is highly indicative of its performance on a diverse array of other benchmarks focusing on translation and reasoning tasks, making it a valuable autonomous evaluation paradigm in settings where hand-curated datasets can be hard to obtain and/or update.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
Large Language Models Logical Reasoning Autoformalization Informalization Formal Translation Truth Maintenance
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/8bfc22650950d7730730ae197eb6810d22dd3769.pdf
datasets and benchmarks
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
/attachment/ba5b71ab3c87be2d551b8e84ed2d87011ee15a94.zip
$\forall$uto$\exists$$\lor\!\land$L: Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission