{"id":"d05ad425-5e75-4019-841f-d6c28ffef0d6","arxiv_id":"2607.10918","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Minimal LTL formulas can be learned from uncertain traces by Hamming-ball groups plus a Pseudo-Boolean optimization that forces at least one consistent estimate per group.","lead":"The paper gives a way to learn short LTL formulas from system traces that may be corrupted by sensor noise or data loss. It does this by treating each observed trace as a ball of Hamming-neighbors and requiring the formula to fit at least one neighbor per ball, then solving the resulting Pseudo-Boolean program.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"The known fixed Hamming radius k (and true-trace-in-ball guarantee) is the single point on which the “closer-to-ground-truth” claim rests; if it fails the group constraints become unsound.","rationale":"The Reader already isolates the identical assumption (known fixed k + true trace inside every ball) as the weakest link and correctly rates the empirical support as preliminary. The encoding itself is a faithful reduction of Problem 2 once that assumption is granted; the only material risk to the strongest claim is therefore the fragility of the assumption. No deeper inconsistency in the PBO formulation or the tables was found, so the Reader’s CONDITIONAL verdict and high confidence remain appropriate. The concrete test above simply makes the dependence falsifiable.","tokens_in":12437,"tokens_out":516,"duration_ms":35032,"concrete_test":"Re-generate the six ground-truth families of Table II, corrupt each positive/negative trace with Hamming distance exactly k+1 (or with random symbol erasures of the same total weight), keep every other hyper-parameter identical, and re-run Flie / Modified-Flie / Robust. If the qualitative “closer alignment” advantage of Robust disappears or reverses, the claim is shown to rest on the exact ball model.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (abstract, §V) is that the group-selection encoding recovers LTL formulas closer to ground truth than MaxSAT baselines under uncertainty. That claim is only valid when Definition 1 holds: a known a-priori bound k such that the unknown true trace always lies inside the Hamming ball C^k_tr of every observed demonstration. Under that assumption Pest/Nest contain at least one consistent estimate per group, Φ_sel + Φ_grp are sound, and the PBO objective (eqs. 12–13) correctly minimises group loss. If the true corruption exceeds k, is structured (bursts, erasures, continuous sensor noise), or k is misspecified, the balls exclude the true traces; the hard selection constraints then force consistency with incorrect estimates and the recovered formula can be arbitrarily far from ground truth. Tables I–II only ever inject noise of radius ≤k, so they never probe this failure mode. All other modelling choices (syntax tree, soft group loss, user constraints) are secondary; they inherit soundness from the ball assumption.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper proposes a framework for learning minimal LTL formulas from finite traces that may be corrupted by bounded uncertainty (sensor faults, measurement error, data loss). Uncertainty is modeled by Hamming balls of a known radius k around each observed trace; these form estimate groups. The learning problem requires that at least one estimate per group be consistent with the formula (while still allowing a group-level misclassification budget κ). The problem is encoded as a Pseudo-Boolean Optimization whose hard constraints capture LTL syntax/semantics, trace selection, and optional user constraints, while the soft objective minimizes the fraction of groups that contribute no consistent estimate. The method is compared with the MaxSAT learner Flie (and a user-constraint variant) on an HVAC example and six synthetic LTLf patterns; the authors report that the recovered formulas more often preserve temporal structure present in the ground-truth specifications.","tokens_in":12753,"tokens_out":1135,"duration_ms":22896,"significance":"If the modeling assumptions hold, the work fills a genuine gap: prior SAT/MaxSAT LTL learners handle only label noise or exact traces, whereas real sensor streams are frequently bit-flipped or incomplete. The reduction to Pseudo-Boolean Optimization is clean and re-uses standard syntax-tree encodings, so the technique is immediately usable by the existing community. The explicit group-selection variables and the soft group-loss objective are a natural, reusable extension. Even the modest empirical gains already shown would be practically useful for verification and controller synthesis in safety-critical domains once the evaluation is strengthened.","major_comments":[{"comment":"§III-A (Definition 1) and the construction of Pest/Nest: soundness of Φ_sel + Φ_grp (Eqs. 7–10) and therefore of the central claim that recovered formulas align better with ground truth rests on the guarantee that the unknown true trace always lies inside every Hamming ball of the a-priori radius k. Tables I–II only ever inject noise of radius ≤ k; they never probe misspecified k, bursty/structured corruption, or continuous sensor noise. Without such experiments the empirical claim remains conditional on an untested modeling assumption.","section":"§III-A, Def. 1; §V Tables I–II"},{"comment":"§V and Tables I–II: the evaluation comprises a single HVAC system and six synthetic formulas. Formula quality is assessed only by informal visual inspection; no quantitative distance (syntactic, semantic, or language-based) to the ground-truth formula is reported, even though the authors themselves list this as future work in §VI. With so few instances and no metric it is difficult to judge how often, and by how much, the method truly improves over the baselines.","section":"§V, Tables I–II; §VI"},{"comment":"§IV-D, Eqs. (12)–(13): the Pseudo-Boolean objective correctly encodes group misclassification under the ball assumption, yet the paper never discusses the failure mode when the assumption is violated (true corruption >k). A short sensitivity study or negative experiment would make the contribution far more robust and would clarify the practical scope of the method.","section":"§IV-D, Eqs. (12)–(13)"}],"minor_comments":[{"comment":"Fig. 1 caption and surrounding text: the soft/hard distinction is stated clearly, but the figure itself does not visually mark which conjunct is soft; a simple dashed box or color legend would help.","section":"Fig. 1"},{"comment":"Notation for the extended sample Test = (Pest, Nest) is introduced with an abuse-of-notation remark; a short explicit definition of the union would remove any ambiguity for readers implementing the encoding.","section":"§III-A"},{"comment":"Table I, last row: the formula returned by the robust method is syntactically complex and still far from the ground truth; a brief remark on why the solver preferred that particular local minimum would aid interpretation.","section":"Table I"},{"comment":"Several typos appear (“Flie” vs. “FLIE”, “efficient”, “suffix”). A careful proof-reading pass is needed.","section":"throughout"}],"recommendation":"major_revision","confidential_remarks":"The technical core (group encoding + PBO reduction) is solid and publishable after revision. The current experimental section is too thin for a full journal article; I would expect either a substantially larger benchmark suite or a clear statement that the work is a short technical note. The arXiv version already flags the missing distance metrics as future work, so the authors are aware of the gap."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The new piece is the group-selection encoding: Hamming balls around each observed trace, selection variables z_tr, hard “at-least-one-per-group” soft constraints, and a Pseudo-Boolean objective that minimises group misclassification. That does not collapse into the earlier MaxSAT label-noise formulations (Neider & Gavran, Gaglione et al.). The reduction itself (Eqs. 7–13) is cleanly written and the syntax/semantics scaffolding is standard and correct.\n\nWhat the paper does well is state a realistic robustness problem and give a solver-ready encoding that, on the tiny benchmarks they run, recovers more of the intended temporal structure than the unmodified and lightly modified Flie baselines. Tables I–II show the pattern clearly: Flie collapses to trivial formulas, Modified Flie gets partial implications, and their method keeps more of the global operators. The HVAC example and the six synthetic LTLf patterns are enough to illustrate the idea.\n\nThe soft spots are proportional. The evaluation is small (one control system + six formulas), recovery is only partial (often the causal direction flips), no code or data are released, and runtime is higher, as expected for PBO. The load-bearing modelling assumption is the known fixed radius k with the true trace guaranteed to lie inside every ball. The stress-test note is right that Tables I–II never inject noise outside that radius, so they do not probe the failure mode. That is a real limitation of the claim “more closely align with ground-truth,” but it is not a hidden circularity or an internal contradiction; it is simply the modelling premise the authors state in Definition 1. Free parameters (k, κ, n) are explicit.\n\nThis is for people who already work on SAT/MaxSAT LTL learning or who need robust specs from noisy symbolic traces in robotics/CPS. It is a solid method paper, not a finished validation. I would send it to peer review; the encoding is worth refereeing even if the experiments need expansion and the k-assumption needs stress-testing. Worth a look if you care about the formal-methods side of learning from demonstrations.","headline":"Clean encoding of Hamming-ball uncertainty into LTL learning; the technical step is real, the evaluation is still thin, and the whole claim rests on a known radius k.","tokens_in":13344,"tokens_out":524,"would_cite":false,"duration_ms":5470,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"When traces are noisy, force the learner to trust at least one Hamming-neighbor per observation and it recovers LTL formulas closer to ground truth.","keywords":["LTL learning","trace uncertainty","Hamming distance","Pseudo-Boolean optimization","specification mining","MaxSAT","finite traces"],"falsifier":"Generate traces from a known LTL formula, corrupt them with bit-flips whose Hamming distance systematically exceeds the radius k supplied to the learner, and check whether the recovered formula still matches the ground truth better than an ordinary MaxSAT baseline; if not, the claim fails.","tokens_in":13338,"feed_emoji":"📡","tokens_out":533,"duration_ms":5406,"temperature":0.7,"pith_summary":"Real system logs are rarely clean: sensors drop bits, labels flip, packets go missing. Existing LTL learners treat every recorded trace as exact truth (or at most as mislabeled) and therefore invent spurious temporal rules when the data are corrupted. This paper shows that if you treat each observation as the center of a small Hamming ball and require only that at least one trace inside that ball be consistent with the learned formula, a Pseudo-Boolean optimizer recovers formulas that stay closer to the true specification. The method is demonstrated on an HVAC controller and on common finite-trace LTL patterns; under controlled noise it outperforms both the original MaxSAT learner and a user-constraint-augmented variant.","feed_headline":"Noisy traces still yield correct LTL specs","feed_subtitle":"Require one Hamming-neighbor per observation and the learner stays closer to ground truth.","key_machinery":"Uncertainty groups C_k(tr) together with the soft group-selection constraint that at least one estimate inside each group is chosen (and must then satisfy the formula), reduced to a weighted Pseudo-Boolean objective.","core_discovery":"Under a known Hamming-radius bound, the robust LTL learning problem—find a minimal formula such that every uncertainty group contributes at least one consistent trace—can be encoded as a Pseudo-Boolean optimization whose solutions recover formulas that more closely match the ground-truth specification than standard MaxSAT learners that treat traces as exact.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Hamming-ball uncertainty still yields ground-truth LTL formulas","PBO recovers minimal LTL when every group has one consistent trace","Noisy demos: learn LTL closer to truth than exact MaxSAT methods","One valid Hamming neighbor per observation keeps LTL faithful","Robust LTL learning from incomplete traces via Pseudo-Boolean opt"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The true underlying trace always lies inside a known, fixed Hamming ball of radius k around the observed trace; if the real corruption is larger or structured differently, the groups become incorrect.","fun_headline_variants_meta":{"raw":{"variants":["Hamming-ball uncertainty still yields ground-truth LTL formulas","PBO recovers minimal LTL when every group has one consistent trace","Noisy demos: learn LTL closer to truth than exact MaxSAT methods","One valid Hamming neighbor per observation keeps LTL faithful","Robust LTL learning from incomplete traces via Pseudo-Boolean opt"]},"model":"grok-4.5","effort":"low","cost_usd":0.00643,"raw_usage":{"total_tokens":1581,"prompt_tokens":668,"num_sources_used":0,"completion_tokens":92,"cost_in_usd_ticks":64300000,"prompt_tokens_details":{"text_tokens":668,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":821,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":668,"tokens_out":92,"duration_ms":6743,"temperature":1.0,"reasoning_tokens":821,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-14T08:17:50.274370+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Generate traces from a known LTL formula, corrupt them with bit-flips whose Hamming distance systematically exceeds the radius k supplied to the learner, and check whether the recovered formula still matches the ground truth better than an ordinary MaxSAT baseline; if not, the claim fails.","supporting_citations":[],"review_version":1}