{"id":"2b943ff9-aedb-4a6b-9c05-629476607843","arxiv_id":"2507.17482","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"LTLZinc generates image-based temporal reasoning and continual learning benchmarks from LTLf formulas over MiniZinc constraints, and experiments show existing methods often fail.","lead":"LTLZinc is a new benchmarking framework that generates temporal reasoning and continual learning datasets by combining temporal logic formulas with constraints over image classification data. It provides ten ready-made tasks showing current neuro-symbolic and continual learning methods struggle with time-structured constraints.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Load-bearing risk: generated labels/curricula are never independently checked against LTLf semantics, and the paper's own Until definition (§2) is nonstandard and inconsistent with its generated tasks.","rationale":"This paper's central claim is conditional: if LTLZinc works as described, a researcher can generate correctly labeled temporal-reasoning and continual-learning tasks. The truth of that sentence hinges on the semantic correctness of the generation pipeline, not on the experimental baselines. I therefore focus on the weakest link: label correctness. The reader identified the same link (flloat plus the constraint cache); I agree, but the issue is sharper than \"third-party code may have bugs.\" Section 2 defines Until with φ1 required at the same position as φ2. Under that definition, the paper's own CL Task 1 formula from Section 8.1.1 is unsatisfiable, even though the paper reports generated positive curricula for it. Consequently the implementation must be using a different (standard) Until semantics than the one the paper states, and a reader cannot verify from the manuscript which semantics the datasets encode. Correct labels are therefore delegated to flloat and to MiniZinc solving of every transition guard, with no independent validation reported. This is the load-bearing point: if a transition guard solution is wrong or incomplete, all derived annotations, curricula, and experiments inherit the error. The proposed check is decisive and inexpensive: re-evaluate all shipped sequence and curriculum annotations with an independent LTLf checker under the standard semantics, and secondarily brute-force one small task's transition guards against the cache. The code release is a real asset because it makes the test runnable. The experiment-level issues raised by the reader (discarding diverging runs, custom baselines) are legitimate but secondary; they affect the strength of the \"state-of-the-art methods struggle\" claim, not the correctness of the generator. I therefore recommend the reader's verdict stands: conditional acceptance, with the condition extended to include independent semantic validation of generated labels and correction of the Section 2 Until definition.","tokens_in":44285,"tokens_out":15471,"duration_ms":178339,"concrete_test":"Run an independent audit on the released datasets: for each sequence in at least one sequential task and one continual-learning task, recompute each constraint's truth value from the stored per-timestep image labels using the MiniZinc definitions in the paper, evaluate the original LTLf formula with a standard checker (aalta, Lydia, or NuSMV) under textbook Until semantics, and compare against the shipped sequence label and curriculum acceptance. A single mismatch on a positive or negative sequence demonstrates the flloat/SFA/cache pipeline does not produce the claimed annotations. As a secondary check, brute-force enumerate all satisfying Y-assignments for one small-domain transition guard and verify the constraint cache contains exactly that set.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that LTLZinc faithfully turns an LTLf formula over MiniZinc constraints into correctly labeled datasets and curricula. That requires two unverified links: the flloat LTLf-to-SFA conversion and the MiniZinc transition-guard cache. One concrete inconsistency appears in Section 2: it defines Until as \"for some t′ ≤ |π|: π,t′ |= φ2 and for all t′′ ≤ t′: π,t′′ |= φ1\", which requires φ1 to hold at the same position as φ2. Under this definition, the class-continual Task 1 formula ¬zero ∧ (¬zero U (zero ∧ e□¬zero)) is unsatisfiable, yet the paper reports generated positive datasets for it. The implementation must therefore be following standard LTLf semantics (as flloat does), not the semantics printed in the manuscript. A reader cannot tell from the paper which semantics the datasets obey, and correct labels depend entirely on the compiler and on every transition CSP being solved and cached exactly. The paper reports no independent validation of generated labels (no second LTLf checker, no brute-force guard audit); the released code is valuable but is not a correctness proof. If either link is wrong—a compiler miscompilation, an incomplete cache, or an incorrectly reified constraint—every positive/negative label and every continual-learning curriculum in the ten tasks is unreliable, and the experimental conclusions inherit that error.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces LTLZinc, a framework that generates temporal reasoning and continual learning datasets from LTLf specifications over MiniZinc constraints, grounded in arbitrary image classification datasets. The generation pipeline converts an LTLf formula into a symbolic finite automaton via the flloat compiler, solves transition-guard constraint satisfaction problems with a cache, and produces either labeled sequences (sequential mode) or multi-episode curricula (incremental mode). The authors release the generator and ten tasks, and report experiments with modular neuro-symbolic pipelines on six sequence classification tasks and with continual learning strategies on four class-continual tasks. The central claims are that LTLZinc can produce expressive, correctly annotated temporal benchmarks and that current methods struggle on them.","tokens_in":44585,"tokens_out":4579,"duration_ms":53364,"significance":"If the generation pipeline is correct, LTLZinc fills a real gap: it combines temporal logic, relational constraints, and arbitrary perceptual domains, with per-timestep annotations that support several training regimes, and it can generate curricula automatically from a single formula. The paper's strengths include a clearly described generator architecture, a public codebase, use of off-the-shelf components (flloat, MiniZinc, Scallop, ProbLog), extensive experiments across two benchmark families, and explicit release of the ten tasks. However, the manuscript currently contains a load-bearing inconsistency in the formal semantics of Until, and the experimental claims rest on runs that are discarded without counts and on mean values computed over as few as one surviving run. These issues need to be resolved before the framework and its benchmark results can be fully trusted.","major_comments":[{"comment":"The printed semantics of Until in §2 are not the standard LTLf semantics and are inconsistent with the generated tasks. The definition requires that for some t′ ≤ |π|, π,t′ |= φ2 and for all t′′ ≤ t′: π,t′′ |= φ1; this makes φ1 mandatory at the same position as φ2. Under this definition, the class-continual Task 1 formula in §8.1.1, F : ¬zero ∧ (¬zero U (zero ∧ e □¬zero)), is unsatisfiable, yet the paper reports generated positive datasets and experimental results for it. The implementation must therefore be following standard LTLf semantics (as flloat does), not the semantics printed in the manuscript. The authors must correct the formal definition to the standard reading (φ1 required for positions strictly before φ2) and state explicitly which semantics the generated datasets obey.","section":"§2 and §8.1.1"},{"comment":"The correctness of every generated label and curriculum rests on two unverified links: the flloat LTLf-to-SFA conversion and the MiniZinc transition-guard cache. The paper reports no independent validation of the generated labels—no second LTLf checker, no brute-force audit of transition guards, no re-checking of sampled traces against the original formula. Since a miscompiled transition or an incorrectly reified constraint would invalidate all positive/negative labels and all curricula, the authors should add and document such validation (e.g., randomized trace re-checking with an independent tool, unit tests for the guard cache, and a statement of which compiler version and MiniZinc configuration were used).","section":"§4 and §7/§8"},{"comment":"The experimental results discard diverging runs without reporting how many runs were discarded, making the reported means and standard deviations unreliable. Appendix A.4 states that runs diverging due to NaN or infinite gradients are discarded, and the text around Figure 3 and Table 1 admits that zero variance is often due to only one experiment converging. For example, Table 1 Task 6 reports 0.60±0.00 and 0.50±0.00 for several configurations, and Task 5 shows very large standard deviations consistent with one or two surviving runs. The authors should report the number of successful runs for every reported cell, analyze whether divergences are systematic across methods, and either include the failed runs in the comparison or justify their exclusion.","section":"Appendix A.4 and Tables 1–2"},{"comment":"The description of negative-sequence generation is underspecified with respect to the backtracking and length-lowering procedure. The text says that when no path of the target length satisfies the target label, the generator lowers the sequence length until the minimum is reached; it is not clear whether a negative label is always verified against the automaton by the same acceptance test used for positives, or whether a trace that becomes accepting at a shorter length can be relabeled as positive. The authors should specify the exact acceptance/labeling rule and ensure that negative labels are defined by the same LTLf semantics as positive labels.","section":"§4, sequence sampling"}],"minor_comments":[{"comment":"Table 2 contains two rows both labeled \"Task 2(long)\"; the second of these rows appears to correspond to Task 3(long). Please correct the labels.","section":"Table 2"},{"comment":"The displayed formula for Task 1 appears to have unbalanced parentheses (\"¬zero ∧ (¬zero U (zero ∧ e □¬zero).\"), and the weak-next operator is written without clarifying parentheses. Please reformat the formula so that its parse is unambiguous.","section":"§8.1.1"},{"comment":"There is a typo in the Core50 description: \"contidions\" should be \"conditions\".","section":"§3"},{"comment":"The figure legend says \"green: symbolic, reddish: neural\", but the plots in Figures 3 and 4 use different colors and markers; please align the color/marker conventions between the figure caption and the text.","section":"Figure 2"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a strong candidate for a benchmarking paper once the semantic definition is corrected and the generation pipeline is independently validated. The Until semantics issue is serious because it affects the formal foundation of the framework, but it is fixable by correcting the definition and stating explicitly that flloat's standard LTLf semantics are used. The missing run counts and independent label validation are also fixable. I would not recommend rejection, but the current version should not be accepted with these gaps."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"LTLZinc is a genuinely useful contribution. The combination of LTLf over finite traces with MiniZinc constraints over arbitrary image datasets, plus the two generation modes, is new relative to KANDY, LTLBench, Temporal Logic Video, and DeepDFA. The code and ten ready-to-use tasks are released, and the generation pipeline is described in enough detail to reproduce. The experiments are extensive and honestly report difficulties. This fills a real gap at the intersection of neuro-symbolic AI and continual learning.\n\nThe main issue is in Section 2: the printed semantics for U are nonstandard. As written, until requires φ1 to hold at the same position as φ2, which makes formulas like Task 1 of Section 8 unsatisfiable. Presumably the implementation uses the standard flloat semantics, but the manuscript and the generated tasks disagree. That is a documentation bug, easy to fix, yet without the fix the reader cannot know what the datasets actually express. Relatedly, the paper never independently validates that generated labels and curricula match the intended LTLf semantics. This is a legitimate concern, though not evidence of a bug. A small audit using a second LTLf checker would settle it.\n\nThe experimental soft spots are real but secondary. Diverging runs are discarded without counts, and some results come from a single run; three seeds is not many. The 'state-of-the-art' framing is too strong given that the baselines are custom modular pipelines rather than published systems. Still, the purpose of the experiments is to show the tasks are challenging, and they do.\n\nThe stress-test note is worth heeding but not fatal. The central argument holds up: the framework does what it claims, modulo the semantics documentation issue. This paper deserves peer review. I would recommend conditional acceptance, asking for the semantics fix, the discarded-run counts, and ideally a label audit.","headline":"Solid benchmark generator with a fixable semantics bug in Section 2; worth reviewing, conditional accept.","tokens_in":45077,"tokens_out":2828,"would_cite":true,"duration_ms":32249,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"LTLZinc establishes that an LTLf formula over MiniZinc constraints and arbitrary image domains is enough to generate expressive, fine-grained temporal reasoning and continual learning datasets, and that current neuro-symbolic and…","keywords":["LTLZinc","linear temporal logic on finite traces","neuro-symbolic AI","continual learning","dataset generation","temporal reasoning","constraint satisfaction","sequence classification"],"falsifier":"Generate a small dataset from a short LTLZinc formula, then independently recheck every sequence label with a different LTLf model checker or by exhaustive enumeration of the constraint alphabet; any mismatch would show the automaton conversion or the constraint solving is wrong.","tokens_in":44119,"feed_emoji":"⏳","tokens_out":7303,"duration_ms":76138,"temperature":0.7,"pith_summary":"LTLZinc is a dataset generator that starts from a linear temporal logic formula over finite traces (LTLf), written on top of MiniZinc constraints between symbolic labels, and produces either labeled sequences of images (sequential mode) or sequences of learning episodes (incremental mode). The same specification can be instantiated over any image classification domain, and each timestep carries image labels, constraint truth values, automaton states, and a sequence-level label. The paper reports that six neuro-symbolic sequence classification tasks and four class-continual learning tasks built this way are hard for current methods: purely neural pipelines often fail on the temporal objective, and continual learners without injected temporal knowledge lose rare classes. The point of the framework is to give the community a single, customizable source of temporal benchmarks with controllable relational constraints and multiple supervision levels.","feed_headline":"LTLZinc turns temporal-logic formulas into ready-made AI benchmarks","feed_subtitle":"Write an LTLf rule, choose an image set, and get labeled sequences plus continual-learning curricula.","key_machinery":"The load-bearing object is the symbolic finite automaton obtained from the LTLf specification—a finite automaton whose transition guards are expressions over the user's MiniZinc constraints rather than single alphabet symbols. LTLZinc compiles the formula into this automaton once, then generates every dataset by random walks over it, fixing the sequence label by whether the walk ends in an accepting state. For each transition the generator builds and solves a MiniZinc constraint satisfaction problem that makes the symbolic labels satisfy the guard, caches all solutions, and samples from the cache to fill timesteps; this cache is what turns a potentially exponential per-sample cost into a constant-time draw after a one-time per-transition solve. The same automaton also serves as background knowledge and as the annotation source for automaton-state traces, which the experiments use for next-state prediction and for knowledge-unit injection in continual learning.","core_discovery":"On its own terms, the paper's claim is that a user-defined temporal specification—an LTLf formula whose atomic propositions are MiniZinc constraints over symbolic labels—is enough to define a benchmark family with a precise semantics. LTLZinc converts the formula into a symbolic finite automaton, samples random walks of chosen length from the start state, and labels a sequence positive exactly when its walk ends in an accepting state; each transition's guard is turned into a constraint satisfaction problem whose solutions are cached and sampled to populate the timesteps with concrete images and labels. In sequential mode the output is a dataset of positive and negative sequences with per-timestep annotations, and in incremental mode the single positive walk becomes a curriculum of episodes that shares the same temporal property across different random seeds. The experimental sections argue that these generated tasks separate methods: neural-only pipelines have low temporal accuracy, symbolic components help but are harder to optimize, and in class-continual tasks knowledge of the temporal structure (predicate or automaton-state units) is what prevents rare classes from being forgotten. The central discovery is therefore a generative reduction: temporal reasoning and continual learning benchmarks can be produced from a compact declarative specification rather than hand-crafted per-task code.","pith_inferences":["Editorial extension: because the perceptual domain is decoupled from the temporal specification, one could hold a formula fixed and swap image difficulty, isolating whether failures come from perception or from temporal reasoning—an experiment the paper reports only partially.","Editorial extension: the constraint cache implies generation cost depends on the number of automaton transitions, not the dataset size; the practical ceiling is the automaton blow-up of the LTLf-to-SFA conversion, so very long or heavily nested formulas are where the generator will first slow down.","Editorial extension: a testable use of the framework would be to generate negative sequences that violate the formula only in one controlled way (wrong timing rather than wrong constraints), and probe whether neuro-symbolic models learn the temporal rule or a shallower correlation."],"forward_implications":["Given one LTLf formula and one image domain, a researcher can generate many datasets with different lengths, positive/negative balance, and—in incremental mode—different curricula that all satisfy the same temporal specification.","Because every timestep is annotated with image labels, constraint values, and automaton state, the same generated data supports end-to-end sequence classification, temporally distant supervision with intermediate annotations, and constraint induction over time.","If the experimental results hold, purely neural sequence models are not enough for relational-temporal tasks, and replacing or augmenting neural modules with symbolic constraint reasoning and automaton knowledge improves temporal accuracy while being harder to optimize.","In class-continual tasks, injecting temporal background knowledge (which predicates or automaton states are active in an episode) is what prevents catastrophic forgetting of rare classes that appear once.","The released generator and ten ready-to-use tasks give other researchers a shared testbed for comparing neuro-symbolic and continual learning methods under the same temporal specifications."],"supporting_citations":[{"why":"Defines LTLf semantics over finite traces, the formalism every LTLZinc specification uses.","marker":"[16]"},{"why":"Defines MiniZinc, the constraint language used to write the relations that appear inside LTLZinc formulas.","marker":"[58]"},{"why":"Introduces symbolic finite automata, the representation LTLZinc compiles formulas into for random-walk generation.","marker":"[75]"},{"why":"Prior work by the authors that this framework builds on, cited as the preliminary investigation of the research avenue.","marker":"[43]"},{"why":"Supplies the reasoning-shortcut and non-i.i.d. continual-learning examples that motivate the temporal benchmark design.","marker":"[52]"},{"why":"Provides the neuro-symbolic automaton architecture used as a next-state prediction baseline and knowledge source.","marker":"[47]"},{"why":"Grounds LTLf specifications in image sequences, a baseline approach the sequence-classification experiments build on.","marker":"[72]"},{"why":"Establishes the distant-supervision framework whose tasks LTLZinc generalizes to the temporal setting.","marker":"[48]"}],"fun_headline_variants":["LTLZinc generates temporal AI benchmarks from logic specs","Write LTL rules, get continual-learning datasets: LTLZinc","LTLZinc: from LTLf to labeled benchmarks for neuro-symbolic AI","Spec-driven benchmark generation tests temporal reasoning limits","LTLZinc turns temporal logic into challenging AI tasks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole generator trusts that turning an LTLf formula into an automaton and solving every automaton transition's constraint problem is done correctly, because every sequence label and curriculum is derived from those two steps.","fun_headline_variants_meta":{"raw":{"variants":["LTLZinc generates temporal AI benchmarks from logic specs","Write LTL rules, get continual-learning datasets: LTLZinc","LTLZinc: from LTLf to labeled benchmarks for neuro-symbolic AI","Spec-driven benchmark generation tests temporal reasoning limits","LTLZinc turns temporal logic into challenging AI tasks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001121,"raw_usage":{"total_tokens":4709,"prompt_tokens":1035,"completion_tokens":3674,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":651,"completion_tokens_details":{"reasoning_tokens":3586}},"tokens_in":651,"tokens_out":3674,"duration_ms":25878,"temperature":1.0,"reasoning_tokens":3586,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T14:46:31.757726+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Generate a small dataset from a short LTLZinc formula, then independently recheck every sequence label with a different LTLf model checker or by exhaustive enumeration of the constraint alphabet; any mismatch would show the automaton conversion or the constraint solving is wrong.","supporting_citations":[{"cited_title":"J., Becket, R., Brand, S., Duck, G","cited_arxiv_id":null,"evidence_quote":"Defines MiniZinc, the constraint language used to write the relations that appear inside LTLZinc formulas."},{"cited_title":"Symbolic au- tomata constraint solving","cited_arxiv_id":null,"evidence_quote":"Introduces symbolic finite automata, the representation LTLZinc compiles formulas into for random-walk generation."},{"cited_title":"A Neuro-Symbolic Framework for Sequence Classification with Relational and Temporal Knowledge","cited_arxiv_id":"2505.05106","evidence_quote":"Prior work by the authors that this framework builds on, cited as the preliminary investigation of the research avenue."},{"cited_title":"Neuro-Symbolic Continual Learning: Knowledge, Reasoning Shortcuts and Concept Rehearsal","cited_arxiv_id":"2302.01242","evidence_quote":"Supplies the reasoning-shortcut and non-i.i.d. continual-learning examples that motivate the temporal benchmark design."},{"cited_title":"Grounding ltlf specifications in image sequences","cited_arxiv_id":null,"evidence_quote":"Grounds LTLf specifications in image sequences, a baseline approach the sequence-classification experiments build on."},{"cited_title":"Deepproblog: Neural probabilistic logic programming","cited_arxiv_id":null,"evidence_quote":"Establishes the distant-supervision framework whose tasks LTLZinc generalizes to the temporal setting."}],"review_version":1}