Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks

Authors: Rushang Karia, Daniel Richard Bramblett, Daksh Dobhal, Siddharth Srivastava
Primary area: datasets and benchmarks
Keywords: Large Language Models, Logical Reasoning, Autoformalization, Informalization, Formal Translation, Truth Maintenance

Abstract:
This paper presents AutoEval, 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. AutoEval 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 AutoEval 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.

Decision: accept (poster)
Reviewer scores: 8, 6, 5

Reviews and discussion:
<thread>
creation date:
1730440227539

thread_type:
official_review

<thread_object>
creator: reviewer_t14z

<content>
summary:
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.

strengths:
- 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.

weaknesses:
- 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.

questions:
- 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.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730441315430

thread_type:
official_review

<thread_object>
creator: reviewer_jcxm

<content>
summary:
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.

strengths:
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.

weaknesses:
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.

questions:
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?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730749772750

thread_type:
official_review

<thread_object>
creator: reviewer_caky

<content>
summary:
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.

strengths:
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

weaknesses:
1. Explanation on how the generated dataset is having diverse data points or quality is missing. 

Update: Rebuttal answered various points about this and mentioned they have added more information in appendix.

questions:
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
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper presents $\forall$uto$\exists$$\lor\land$L, an innovative autonomous benchmark for evaluating LLMs on formal reasoning tasks. The key strengths include: (1) dynamic dataset generation using CFGs that prevents overfitting, (2) automated ground truth generation eliminating human annotation needs, and (3) formal verifiers ensuring semantic correctness. The main findings demonstrate strong correlation between performance on $\forall$uto$\exists$$\lor\land$L and other established benchmarks. While initially tested on 7 LLMs, the authors expanded to 16 diverse models (4B-70B parameters) during rebuttal, strengthening the empirical validation. The paper makes a clear contribution by introducing a scalable, automated evaluation framework for formal reasoning capabilities in LLMs.