Technical Summary: LOVER (Logic-Regularized Verifier)

Problem Statement

Verifiers are essential for enhancing the reasoning capabilities of Large Language Models (LLMs) by optimizing parameters (via RL) or selecting optimal outputs (via inference scaling). However, existing verifiers face two primary limitations:

1. Data Dependency: Traditional supervised verifiers require expensive, resource-intensive labeled datasets. Collecting high-quality annotations, particularly for specialized domains or step-level process annotations, is costly and time-consuming.
2. Diversity and Generalization: Reliance on expert annotations can lead to a lack of solution diversity, as annotators may favor familiar reasoning patterns over equally valid but less intuitive ones. Furthermore, recent unsupervised approaches like CoT-Decoding are sensitive to backbone model choices, while others like CCS are limited to Yes-No questions and struggle to scale to general reasoning tasks.

The central question addressed is whether it is possible to build effective verifiers without the supervision process, leveraging the intrinsic knowledge already present in LLMs.

Methodology: LOVER

The authors propose LOVER (Logic-Regularized Verifier), an unsupervised probabilistic verifier regularized by logical rules. LOVER treats the verification task as inferring a binary latent variable (truth value) based on the internal activations of an LLM, without modifying the LLM's weights or requiring labeled data.

Core Components

1. Contrastive Assertions:
   For a given question $q$ and a generated reasoning path $s_i$, the input is augmented with text templates to form contrastive assertions:

   • $x^+_i = q \oplus s_i \oplus \text{"This is a true answer."}$
   • $x^-_i = q \oplus s_i \oplus \text{"This is a false answer."}$
     This process aims to elicit the model's internal "beliefs" or "knowledge" regarding the validity of the reasoning path.

2. Latent Verifier Model:
   The verifier is a lightweight Multi-Layer Perceptron (MLP) that takes the hidden state representations (specifically from middle layers) of the assertions as input. It outputs a probability $p_\theta(z|x)$, where $z \in \{0, 1\}$ indicates the validity of the statement.

3. Logical Constraints (Regularization):
   To bridge discrete logical rules with continuous neural networks, LOVER enforces three logical constraints via soft probabilistic objectives:

   • Negation Consistency: For a pair of contrastive assertions ($x^+_i, x^-_i$), their truth probabilities must sum to 1 and differ significantly (Law of Excluded Middle). This prevents degenerate solutions where both are assigned the same probability.
   • Intra-group Consistency: Reasoning paths grouped by the same final answer should share similar correctness probabilities. This enforces consistency among solutions leading to the same conclusion.
   • Inter-group Consistency: Among multiple groups of reasoning paths (each group corresponding to a distinct final answer), exactly one group's "true" assertion should be valid. This is enforced using a sum constraint and an entropy regularization term to prevent uniform probability distribution across groups.

4. Training and Inference:

   • Training: The model is trained end-to-end by minimizing the sum of the three loss functions derived from the logical constraints. No ground-truth labels are used.
   • Inference: Given a question, $N$ candidate solutions are generated. For each solution, the verifier predicts the correctness probability of the "true" assertion. Solutions are grouped by their final answers, and the group with the highest aggregate score (using either max or sum strategies) is selected as the final answer.

Key Contributions

1. Principled Unsupervised Framework: LOVER provides a scalable framework for verifying reasoning paths by leveraging intrinsic LLM knowledge regularized by logical rules, eliminating the need for supervised data.
2. Soft Probabilistic Objectives: The paper introduces soft probabilistic formulations for discrete logical constraints, enabling the differentiable, end-to-end training of the verifier.
3. General Compatibility: The method is compatible with any off-the-shelf white-box LLM and applicable to general reasoning tasks, not limited to specific question types like Yes-No.

Experimental Results

Experiments were conducted on 10 datasets, including mathematical reasoning (GSM8K, iGSM), open-domain knowledge (HotpotQA, MMLU-Pro), and out-of-distribution (OOD) tasks from BIG-Bench Hard.

• Performance vs. Baselines: LOVER significantly outperforms unsupervised baselines (Greedy, Majority Voting, CoT-Decoding).
  • On average, LOVER (sum) achieves performance comparable to supervised verifiers, reaching approximately 95% of the supervised verifier's performance level.
  • LOVER (sum) achieves an average absolute accuracy gain of 3.3% over Majority Voting and 2.9% over CoT-Decoding.
  • LOVER demonstrates robustness across different model scales (from 0.5B to 32B parameters) and decoding strategies.
• Ablation Studies:
  • Logical Constraints: Removing the inter-group consistency loss ($L_{inter}$) caused the most significant performance drop, indicating its critical role in distinguishing correct answer groups. Negation consistency ($L_{nega}$) was also crucial for preventing identical scoring of true/false assertions.
  • Decoding Strategy: LOVER performs best with natural CoT decoding and is less sensitive to decoding strategy changes compared to CoT-Decoding, which relies heavily on specific output formats.
  • Hidden States: Utilizing hidden states from middle layers (e.g., layer 15 or 20 in Mistral-7b) yields optimal performance.
• OOD Generalization: LOVER demonstrates strong generalization on OOD datasets (Boolean Expressions, Web of Lies, etc.), outperforming Majority Voting and CoT-Decoding across all tested scenarios, suggesting it learns domain-agnostic patterns for evaluating assertion correctness.

Significance and Claims

The paper claims that LOVER represents a significant step toward building verifiers that do not rely on the expensive supervision process. By treating the verifier as a binary latent variable and enforcing logical consistency on multiple reasoning paths, LOVER effectively harnesses the "latent knowledge" within LLMs.

The authors position LOVER as an unsupervised probe guided by logic rules, offering a practical alternative to supervised verifiers. It addresses the limitations of existing unsupervised methods (which are either heuristic-based and sensitive to model choice, or limited to specific question types) by providing a flexible, scalable solution for general reasoning tasks. The work suggests that logical constraints can serve as effective priors to unlock the reasoning capabilities of LLMs without human annotation.

Limitations Noted: The method inherently requires access to the hidden states of the LLM, restricting its application to white-box models and preventing direct use in black-box scenarios.