{"id":"217b15a2-e775-43c5-8642-81b07ce8df27","arxiv_id":"2411.10601","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"QUINTIC learns deterministic quantitative automata from preference queries using SMT-based conjectures over variable equivalences, with claimed guarantees of completeness and minimalism.","lead":"This paper introduces QUINTIC, an active learning algorithm that infers quantitative automata, such as summation and discounted-sum machines, from preference comparisons over sequences. It would let systems learn behavior models from rankings, which are easier to collect than exact numeric labels, if the stated guarantees held.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Algorithm 1 Line 13 requires exhaustive enumeration of concrete hypotheses over an infinite rational output alphabet, so the claimed termination guarantee does not follow.","rationale":"The paper's headline claim is that QUINTIC 'performs a complete search over the space of automata, and is guaranteed to be minimal and correctly terminate.' The reader's weakest assumption targets the one place where the algorithm actually has to iterate over concrete hypotheses: Line 13 of Algorithm 1. I agree this is the single most load-bearing weakness. The output alphabets for summation, discounted summation, and product are infinite (rationals / positive rationals per Table 1), so the set of concrete hypotheses consistent with C is generally infinite; even strong feedback only fixes values of counterexample sequences, not all state labels. Thus the exhaustive 'test all concrete hypotheses' loop cannot terminate by enumeration. The formal definition in Section 3 also requires finite Sigma_O, contradicting Table 1. Other concerns, such as the minimalism proof in Theorem 2 being a non-sequitur, are serious, but the Line 13 issue alone invalidates the termination guarantee that is the central claimed contribution. The empirical results on 25 hand-constructed targets do not address this, since they use finite runs with solver timeouts or budgets. A concrete reproduction on a two-state target with weak feedback would settle whether an implicit bound is needed.","tokens_in":24559,"tokens_out":3355,"duration_ms":34043,"concrete_test":"Run the learner on a two-state summation automaton with input alphabet {a}, state labels 0 and 1, using weak-feedback equivalence queries. Instrument Algorithm 1 Line 13 to count concrete hypotheses enumerated before finding the correct automaton. If the loop requires an added finite bound on rational output values or an iteration cap to terminate on this toy target, the exhaustive-enumeration step is not executable as stated, and the termination guarantee fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central termination guarantee rests on Algorithm 1, Line 13, which says: 'Exhaustively test all concrete hypotheses h under symbolic hypothesis H and constraints C using EquivQ(h) ... until an h is found to be correct or there exist no more valid h under H and the updated constraints C.' A concrete hypothesis h is an assignment of output-alphabet values to the table variables. For summation, discounted summation, and product, Table 1 sets the output alphabet to the rationals (or positive rationals), which is infinite. Even after collecting preference constraints and counterexample feedback, the constraint set C typically admits infinitely many rational assignments; for example, a constraint v1 < v2 has continuum many rational solutions. Weak feedback only adds disequalities, which does not reduce this to a finite set. Therefore the exhaustive loop in Line 13 cannot be executed in finite time for these valuations, and the algorithm's termination guarantee is not established. This is not merely a missing implementation detail: Section 3 defines a deterministic quantitative automaton with a finite output alphabet, yet Table 1 uses an infinite output alphabet, so the problem itself is not well-formed under the paper's own definitions.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces QUINTIC, an active learning algorithm for deterministic quantitative automata from preference and equivalence queries. The learner maintains a symbolic observation table, infers variable equivalences from preference constraints using valuation-specific inference rules, encodes equivalence conjectures as a MaxSMT problem, and uses iterative deepening over a bounded number of SymbolicFill calls to search for a hypothesis. The authors claim that the search is complete, that the output is minimal, and that the algorithm terminates, and they report experiments on 25 hand-constructed target automata under summation, discounted summation, product, and classification valuation functions.","tokens_in":24825,"tokens_out":3914,"duration_ms":42325,"significance":"The problem is well motivated, and the idea of combining symbolic observation tables with SMT/MaxSMT solving for learning quantitative automata from constraints is interesting and potentially useful. The paper also provides a nontrivial implementation and empirical ablations, which gives some support for the practical behavior of the algorithm. However, the central theoretical guarantees are not established: Theorem 1's completeness proof does not connect the bounded chain search to the target automaton, Theorem 2's minimality proof assumes the very object it must construct, and the exhaustive concrete-hypothesis loop in Algorithm 1 requires enumerating an infinite set for the rational output alphabets used in Table 1. The empirical evaluation is limited to hand-constructed targets, and the main baseline is the authors' prior work Remap, so the evidence for the claimed completeness and minimality is not convincing.","major_comments":[{"comment":"The claimed termination guarantee does not follow because Line 13 requires exhaustively testing all concrete hypotheses h under a symbolic hypothesis H and constraints C, but for summation, discounted summation, and product, Table 1 sets the output alphabet to the rationals or positive rationals, which is infinite. Even after preference constraints and weak feedback constraints are collected, the constraint set C typically admits infinitely many rational assignments, e.g., a constraint v1 < v2 has infinitely many rational solutions, and weak feedback only adds disequalities. Therefore the exhaustive loop in Line 13 cannot be executed in finite time, so the algorithm's termination guarantee is not established. This is compounded by Section 3, which defines a deterministic quantitative automaton as having a finite output alphabet, making the problem itself ill-posed under the paper's own definitions.","section":"§4, Algorithm 1 Line 13, Table 1"},{"comment":"The proof of Theorem 1 asserts that iterative deepening depth-first search over SymbolicFill budgets is complete, but it does not show that the target automaton is represented by a chain of length at most M for some finite M, nor that the alternating SymbolicFill/Expansion process actually enumerates all relevant hypotheses. In particular, no argument is given that the space of output-label assignments is finite or enumerable in the claimed sense; as noted above, Line 13's exhaustive enumeration is over an infinite set for the rational-valued valuations. Thus the statement that QUINTIC performs a complete search over automata space is not established.","section":"Theorem 1, §5.3"},{"comment":"The minimality proof assumes the existence of a set Ω of infinitely many tables that are 'isomorphic by construction to the target' and then asserts that QUINTIC finds the shortest chain to an element of Ω. No construction or proof of the existence of Ω is given, and the claim that reaching any element of Ω yields a minimal automaton is asserted rather than demonstrated. The construction in Equation 1 only collapses duplicate rows; it does not by itself prove that the resulting automaton has the minimum number of states among all automata equivalent to the target. The proof therefore essentially restates the conclusion it is supposed to establish.","section":"Theorem 2, §5.3"},{"comment":"The inference rules for determining variable equivalences are central to the algorithm, since they drive the closedness and consistency checks, but the paper states that 'inference rules can be derived' and presents a decision tree without proving that the rules are sound and complete for the stated preference-query models. The paper also explicitly acknowledges that variable equivalence cannot always be determined from preference queries alone, yet the correctness of the table-unification procedure depends on exactly which equivalences are inferred and which are merely conjectured. A formal statement and proof of the decision-tree inference rules are needed before the completeness and termination arguments can be assessed.","section":"§5.1"}],"minor_comments":[{"comment":"The description of the variants contains an apparent typo: 'W-CC-VE (W feedback, CC disabled)' should presumably read 'W-CC-VE (W feedback, CC enabled)', since the preceding sentence states that CC-VE denotes the variant with the closedness-and-consistency objective enabled.","section":"§6.1"},{"comment":"The table header appears corrupted as 'Valuation, Symbol Output Alphabet'; the intended distinction between the symbolic output alphabet and the concrete output alphabet should be stated clearly, especially because the finiteness of the output alphabet is part of the automaton definition in Section 3.","section":"Table 1"},{"comment":"The decision-tree diagram is hard to read: the labels 'Ris<', 'Ris>', 'Ris=', and 'Ris?' are abbreviated without a legend, and the relationship between the two preference-query pairs and the inferred relation R is not visually explicit. A concrete example of each region would improve clarity.","section":"Figure 3"},{"comment":"The phrase 'learning underΠ fails to terminate' has a formatting issue ('underΠ'), and the ablation discussion would benefit from stating whether the non-termination is a divergence in the search chain or a failure of the underlying SMT loop to find a model.","section":"§6.6"},{"comment":"The paper does not state whether the implementation and experimental scripts are publicly available, which would be useful for reproducing the reported results and for comparing against future baselines.","section":"§6.1"}],"recommendation":"reject","confidential_remarks":"The paper addresses an interesting and timely problem, and the empirical effort is substantial. However, the main theoretical claims are not supported by the current proofs: the infinite enumeration in Algorithm 1, the gap in the completeness argument, and the circularity of the minimality proof are load-bearing issues that cannot be fixed by small local revisions. I would recommend rejection, but I could see a substantially revised version re-submitting after the termination and completeness conditions are made precise, the output alphabet is handled consistently, and the proofs are completed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this paper introduces a genuinely new learning problem and a plausible algorithm, but the completeness and minimality guarantees are not established. The stress-test concern about Line 13 is correct, not a nitpick.\n\nWhat is new and worth credit: the problem of actively learning deterministic quantitative automata from preference and equivalence queries, without numeric membership queries, is a real extension of Remap to recursive valuations (summation, discounted summation, product). The decision-tree rules for inferring variable equivalences from preference pairs are neat, and the idea of searching over conjecture–expansion chains with a MaxSMT objective is clever. The empirical work is thorough: 25 targets, four valuations, strong/weak feedback, ablations, error bars. The approach clearly does something in practice.\n\nSoft spots: Algorithm 1, Line 13 asks the learner to 'exhaustively test all concrete hypotheses' under a symbolic hypothesis and constraints. With Table 1's rational (or positive rational) output alphabets, the set of satisfying assignments to the table variables is typically infinite—a constraint like v1 < v2 admits continuum many rational solutions. Exhaustive enumeration therefore cannot be completed in finite time, so the termination guarantee fails as stated. This also clashes with the paper's own Section 3 definition, which assumes a finite output alphabet. The proofs of Theorems 1 and 2 are sketches: Theorem 1 assumes the target is reachable in some bounded chain without showing it, and Theorem 2 assumes the existence of an isomorphic table set and then declares minimalism. These are load-bearing gaps, not cosmetic ones. The evaluation is on hand-constructed targets, with the authors' own Remap as the only baseline and no code or data release, so independent verification is hard.\n\nWho the paper is for: researchers in automata learning, reward machine inference, and preference-based RL. The problem formulation and the variable-equivalence inference rules are worth their attention. But I would not cite it for its guarantees.\n\nRecommendation: it deserves a serious referee. The problem and approach are new, and the flaws are specific and potentially fixable. I would send it to review with a clear instruction to fix the termination argument (finite output alphabets or a real bound on labels) and to make Theorems 1 and 2 rigorous. As is, it should be a major revision at best.","headline":"A plausible new problem and a clever algorithm, but the advertised guarantees don't hold—the infinite enumeration in Line 13 is a real blocker.","tokens_in":25253,"tokens_out":4831,"would_cite":false,"duration_ms":47111,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q32"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that deterministic quantitative automata—machines that assign numbers to strings by summation, discounted summation, product, or classification—can be learned from preference and equivalence queries alone, with the…","keywords":["active automata learning","quantitative automata","preference queries","equivalence queries","symbolic observation table","constraint solving","MaxSMT","iterative deepening"],"falsifier":"With weak feedback only, take a one-state summation target with an unknown rational label $c$ and answer every query consistently with $V(s)=c\\cdot |s|$; because infinitely many rational $c$ satisfy any finite set of such constraints, watch whether the exhaustive hypothesis-testing loop terminates, and if it does, record what bound on $c$ it used.","tokens_in":24373,"feed_emoji":"🤖","tokens_out":11345,"duration_ms":103264,"temperature":0.7,"pith_summary":"The paper proposes learning deterministic quantitative automata—machines that assign numbers to strings by summing, discount-summing, multiplying, or classifying labels along a run—without ever asking for concrete input-output values. Instead, the learner asks only comparison questions and equivalence questions, translates the answers into constraints over table variables, and deduces the automaton using a background theory such as the theory of rationals. The claim is that the resulting algorithm, QUINTIC, exhaustively searches the space of automata, is guaranteed to return the minimal equivalent automaton, and is guaranteed to terminate. This matters because explicit numeric labels are often expensive or unnatural to obtain, whereas ranking and preference data are cheap and common in robotics, reinforcement learning, and other settings.","feed_headline":"Learn quantitative automata from comparisons, not examples","feed_subtitle":"QUINTIC guarantees the minimal automaton from preference and equivalence queries alone.","key_machinery":"The load-bearing object is the symbolic observation table, a two-dimensional array of variables with a constraint set, together with the requirement that a table be unified, closed, and consistent before it yields an automaton hypothesis. Equally central are the inference rules that convert pairs of preference-query answers into relations between table variables for each valuation function, encoded as decision trees, and the MaxSMT objective that maximizes the number of conjectured variable equalities while satisfying the constraints, guiding the search toward fewest states. Iterative deepening depth-first search, realized by budgeting symbolic-fill calls, is the mechanism that turns a potentially infinite conjecture–expansion chain into a complete, minimality-preserving search, and equivalence-query feedback supplies the constraints that invalidate wrong conjectures.","core_discovery":"On the paper's own terms, the central discovery is that active learning of deterministic quantitative automata can be driven entirely by constraints derived from preferences rather than by membership observations. QUINTIC maintains a symbolic observation table whose entries are variables, uses inference rules tied to the recursive structure of the valuation function to decide which variables must be equal, and conjectures the remaining equalities as part of a maximum-satisfiability problem. Because variable equivalence can be genuinely ambiguous, greedy unification is impossible; the algorithm therefore backtracks over chains of conjectures and table expansions, with iterative deepening bounding the chain length. The authors argue that this yields a complete search over automata and a minimal result, and they demonstrate the method on summation, discounted summation, product, and classification automata over the rationals.","pith_inferences":["The same recipe could be instantiated for other recursively defined valuation functions—average reward, min/max accumulation, or min-plus—whenever inference rules analogous to the paper's decision trees can be derived; the paper demonstrates only the four listed valuations.","A practical deployment with human preference data would infer reward machines from rankings without numeric rewards, provided the human's comparisons are consistent with a single target valuation; noisy preferences are outside the paper's model.","One could test how the completeness guarantee changes when preference queries are answered approximately or adversarially, since the proof assumes a teacher whose answers are perfectly consistent with the target.","The symbolic-table plus constraint-solving design suggests a modular library of valuation theories in which swapping the recursive definition and inference rules changes only the theory component of the learner."],"forward_implications":["For any target representable by a deterministic quantitative automaton under summation, discounted summation, product, or classification semantics, a learner with only preference and equivalence queries can in principle return an equivalent automaton.","The returned automaton is guaranteed to be minimal in the number of states.","The algorithm terminates despite an infinite hypothesis space because iterative deepening bounds the length of conjecture–expansion chains.","In the reported experiments QUINTIC learns all 25 ground-truth automata, with discounted summation and product being the hardest valuations and disabling iterative deepening causing non-termination for product targets."],"supporting_citations":[{"why":"Supplies the L*-style active learning loop and observation table that QUINTIC adapts.","marker":"[1]"},{"why":"Defines the quantitative automata and valuation functions that form the class of objects being learned.","marker":"[6]"},{"why":"Supports the discounted summation valuation used as one of the four target semantics.","marker":"[7]"},{"why":"The SMT/MaxSMT solver used to implement the constraint-solving step in experiments.","marker":"[11]"},{"why":"Introduces the symbolic observation table and preference-query formulation that QUINTIC extends and uses as a baseline.","marker":"[16]"},{"why":"The prior approach learning automata from membership and preference queries that QUINTIC generalizes.","marker":"[22]"}],"fun_headline_variants":["Learn automata from preferences, not examples","No examples needed: automata from preferences","QUINTIC: minimal automata via preference constraints","Preference-driven automata learning, guaranteed minimal"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"To terminate, the algorithm must exhaustively try every concrete automaton that fits the current table and constraints, but with rational labels there are infinitely many such automata, so the proof depends on an unstated way to make that infinite list finite.","fun_headline_variants_meta":{"raw":{"variants":["Learn automata from preferences, not examples","No examples needed: automata from preferences","QUINTIC: minimal automata via preference constraints","Preference-driven automata learning, guaranteed minimal"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000173,"raw_usage":{"total_tokens":1245,"prompt_tokens":879,"completion_tokens":366,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":495,"completion_tokens_details":{"reasoning_tokens":308}},"tokens_in":495,"tokens_out":366,"duration_ms":5038,"temperature":1.0,"reasoning_tokens":308,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T19:30:54.759267+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"With weak feedback only, take a one-state summation target with an unknown rational label $c$ and answer every query consistently with $V(s)=c\\cdot |s|$; because infinitely many rational $c$ satisfy any finite set of such constraints, watch whether the exhaustive hypothesis-testing loop terminates, and if it does, record what bound on $c$ it used.","supporting_citations":[{"cited_title":"weighted automata","cited_arxiv_id":null,"evidence_quote":"Defines the quantitative automata and valuation functions that form the class of objects being learned."},{"cited_title":"In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p","cited_arxiv_id":null,"evidence_quote":"The SMT/MaxSMT solver used to implement the constraint-solving step in experiments."},{"cited_title":"Automata Learning from Preference and Equivalence Queries","cited_arxiv_id":"2308.09301","evidence_quote":"Introduces the symbolic observation table and preference-query formulation that QUINTIC extends and uses as a baseline."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The prior approach learning automata from membership and preference queries that QUINTIC generalizes."}],"review_version":1}