Review: ICSE 2027 Submission #396 (QFOL)

SUMMARY

QFOL generates first-order-logic reasoning tasks whose depth, width, label, distractor count, and topic can be set independently. An LLM verbalizes each formal structure; a round-trip translation checked by the Vampire prover guards against meaning drift. The authors build QFOLBench (2,880 tasks), evaluate eight models, and report degradation with complexity, a bias toward True labels, and topic sensitivity.

STRENGTHS

- Deriving True, False, and two Unknown variants from a single DAG's implicit rule is elegant: labels vary, difficulty stays matched.
- The prover-checked round-trip repairs a real defect in ProverQA and FOLIO, whose verbalizations go unverified.
- Distractors are label-preserving by construction; the correct-to-wrong transition analysis and token-padding ablation are careful.
- The error analysis catches something concrete: DeepSeek imports outside knowledge on the Mathematics topic. The artifact is complete.

WEAKNESSES

- Related work is lacking. FLD (ICML 2023), LogicBench, Multi-LogiEval, JustLogic, AutoLogi, ZebraLogic, and SATBench generate logic tasks with controllable difficulty; SATBench already pairs LLM verbalization with solver-side consistency checks. None is cited.
- Unary predicates, one universal variable, no quantifier alternation: these tasks are propositional reasoning in FOL dress, the very charge the paper levels at RuleTaker.
- Gemini-3.1-Pro scores 99.0%. The benchmark saturates at release, undercutting its goal of keeping pace with models.
- DeepSeek-V3.2-Thinking translates both directions, and regenerate-until-pass may select sentences it parses best; it then scores 90.9% as a test subject. Only 50 of 2,880 tasks were checked by hand.
- 180 tasks per depth-width cell, three seeds, no confidence intervals. Several Figure 4 cells improve as depth grows, yet the text narrates uniform degradation.

DETAILED COMMENTS

The novelty is incremental: independent dimension control appears in PrOntoQA-OOD and CogniLoad, prover-backed generation in ProverGen. What is new, and worth keeping, is the label-verified round-trip gate and the implicit-rule construction. Sharpen the paper around those.

Suggestions. 
(1) Verify formula-level equivalence, not label agreement; a mistranslation that preserves the label slips through. Back-translate with a different model; report per-configuration rejection rates. 

(2) Scale depth and width until frontier models fail; controllability needs headroom to matter. 

(3) "Width" is a global count spread over randomly chosen rules, so two W=20 tasks can differ wildly; report the per-rule width distribution. 

(4) The distractor definition promises label invariance for any conclusion, but Algorithm 2 never establishes it; Vampire checks only the one conclusion posed. Say so. 

(5) Add a nonsense-predicate topic to separate semantic familiarity from knowledge conflict. 

(6) Publishing 2,880 fixed instances recreates the contamination the paper warns of; the durable contribution is the generator, so specify a regeneration protocol. 

(7) Report cost in tokens; wall-clock seconds mostly measure API queues. 

(8) The software-engineering hook is thin for ICSE. Framing the consistency check as metamorphic testing would help; so would dropping "test case generation" from the title.

Solid engineering and honest analysis, but the missing 2023–2025 literature and the saturation problem must be fixed. 
