{"id":"29a42865-2a20-4fda-99a5-ffdd224c6905","arxiv_id":"2505.09191","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":1,"one_line_summary":"PACE.jl is a new Julia package applying certified symbolic-numeric algorithms to parameter identification, structural stability analysis, and H-infinity norm computation in control systems.","lead":"This paper introduces PACE.jl, a Julia package that combines exact symbolic algebra with interval arithmetic to solve control theory problems with certified guarantees. It demonstrates the package on parameter identification, stability analysis, and H-infinity norm computation, with runnable notebooks.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 4.1's worked identification example is internally inconsistent: the printed derivative estimates contradict the stated rational interpolant, and interpolation-based derivative estimation is not covered by the certified-solver guarantee.","rationale":"The reader's weakest assumption is exactly the load-bearing concern: the reduction from control data to a polynomial system, specifically the differentiation of an interpolant, must be correct for the certified solver's output to mean anything. The paper's stability and H-infinity examples work with exact polynomial/rational objects and rely on Sturm-Habicht sequences and discriminant varieties, which are plausible uses of the software; the weak point is identification. I checked the toy example independently: the printed constants do not match the displayed interpolant, confirming that the example as written is internally inconsistent. This is a localized but serious flaw: it undermines the paper's reproducibility claim and its claim that certified algorithms produced the reported identification result. It does not necessarily invalidate the software or the other examples, so conditional acceptance remains the appropriate verdict rather than outright rejection. A single exact recomputation of the three constants would settle whether the inconsistency is a typographical slip or a deeper methodological error in the identification pipeline.","tokens_in":10044,"tokens_out":5160,"duration_ms":51418,"concrete_test":"Recompute \\hat{y}(0), \\hat{y}'(0), and \\hat{y}''(0) from the stated rational interpolant in Section 4.1 using exact rational arithmetic. If the values are not (exactly or to the printed precision) 1.000, 0.608, and 0.227, then correct the interpolant or the printed constants, rerun the 4-solution polynomial solve with the corrected values, and verify that the recovered positive solution reproduces the ground truth (\\mu, x_0) = (0.60, 1.00). The toy example is not reproducible until these numbers are consistent.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that PACE.jl gives certified correct results on control problems, but the identification pipeline in Section 4.1 is only as reliable as the reduction from measured data to a polynomial system. That reduction uses derivatives of an interpolant \\hat{y}(t) built from the data; the polynomial system is then solved exactly, but the solver certifies only the approximate system, not the original parameter-estimation problem. No error bound or convergence statement is provided for the interpolation/differentiation step, so the 'guaranteed to be correct' language in the abstract and conclusion is not justified for identification. The toy example makes the problem concrete: the stated rational interpolant \\hat{y}(t) = (7.40t+54.02)/(1.52t^2-10.93t+27.01) gives \\hat{y}(0) = 54.02/27.01 = 2.000, whereas the paper prints 1.000; its first derivative at 0 is approximately 1.083, not 0.608; and the second derivative is approximately 0.652, not 0.227. Since the displayed polynomial system is built from those three constants, the system as written does not follow from the displayed interpolant, and the printed solutions are not shown to solve the system. This is not merely cosmetic: it invalidates the paper's only complete identification demonstration.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces PACE.jl, a Julia package that wraps and integrates certified symbolic elimination tools (rational univariate representation, discriminant varieties, Sturm-Habicht sequences, interval Newton methods, multi-precision interval arithmetic) and demonstrates their use on three control-theory problems: parameter identification, structural stability of multidimensional systems, and computation of the H-infinity norm. The main text explains the underlying algebraic objects, describes the package structure and its dependencies, and presents three worked examples with runnable notebooks. The authors claim that, by using certified algorithms, the displayed results are guaranteed to be correct.","tokens_in":10357,"tokens_out":3946,"duration_ms":38834,"significance":"If the claims are taken at face value, the paper is a useful software demonstration that brings a nontrivial stack of symbolic-certification algorithms (RUR, discriminant varieties, CAD, interval arithmetic) to bear on control problems in a reproducible Julia package. The strength of the paper is its packaging: it gives users access to certified zero-dimensional solving, parametric real-root counting, and exact interval output for H-infinity norm computation, with notebooks for all three applications. The significance is, however, tempered by two issues. First, the identification example in §4.1 is internally inconsistent as printed, with wrong numerical constants. Second, the identification pipeline interpolates data and differentiates the interpolant without any error bound, so the 'guaranteed to be correct' language in the abstract and conclusion is not justified for the identification application. The stability and H-infinity demonstrations appear sound and are the most compelling parts of the paper.","major_comments":[{"comment":"The numerical constants on the left-hand side of the displayed polynomial system are inconsistent with the rational interpolant given immediately above. For \\hat{y}(t) = (7.40t + 54.02)/(1.52t^2 - 10.93t + 27.01), one computes \\hat{y}(0) = 54.02/27.01 = 2.000, \\hat{y}'(0) \\approx 1.083, and \\hat{y}''(0) \\approx 0.652. The paper instead prints 1.000, 0.608, and 0.227. As a consequence, x0 = 1.000 does not satisfy x0^2 + x0 = 1.000 (it gives 2.000), and x0 = -2.000 does not satisfy it either. The four printed solutions (±0.604, 1.000) and (±0.427, -2.000) would be consistent with the system if the left-hand side were 2.000, 1.083, and 0.652, so the error appears to be in the printed constants rather than in the solution values, but the demonstration is nevertheless internally contradictory as written and must be corrected.","section":"§4.1, display after 'we evaluate the equations at t0 = 0.00'"},{"comment":"The reduction from measured data to a polynomial system is performed by interpolating the data with \\hat{y}(t), differentiating \\hat{y}(t) symbolically, and evaluating the resulting derivatives at t0. The certified solver then solves the polynomial system exactly, but that system is only an approximation to the true parameter-estimation problem unless the interpolation and differentiation step has a validated error bound or converges as the data density increases. No error estimate, convergence statement, or interval-enclosure of the derivatives is provided. Therefore the abstract and conclusion's claim that the identification results are 'guaranteed to be correct' is too strong; the guarantee applies to the solved algebraic system, not to the parameter estimates obtained from the interpolant. The authors should either supply an error analysis for the interpolation/differentiation step or qualify the guarantee language to state that certification covers only the polynomial system.","section":"§4.1, paragraph on the construction of the polynomial system"},{"comment":"The stability and H-infinity examples appear internally consistent and are the strongest support for the package's claimed capabilities. The H-infinity example gives two intervals, [1.59375, 1.625] and [1.617919921875, 1.6180419921875], that are both plausible as enclosures of the same norm (the second at higher precision), but the text should briefly explain why the first, 'minimum precision necessary to isolate the roots,' is so much wider than the second. This is a minor clarity issue, not a technical error.","section":"§4.2 and §4.3 (general assessment)"}],"minor_comments":[{"comment":"The sentence 'which is a polynomial in ∈ Q[U1,...,Ul]' contains a stray '∈' and should read 'which is a polynomial in Q[U1,...,Ul]'. Several similar typographical slips appear throughout, including 'a j,0,...a j,d1' where the index should be 'd_j'.","section":"§2, paragraph on parametric systems"},{"comment":"The definition of the sets Poi and Ptj is dense and has minor notation inconsistencies (e.g., 'd1' used in multiple levels). A reference to the precise algorithm or a clearer display would help a reader verify the decomposition claim.","section":"§2, definition of cells"},{"comment":"The table of ground-truth versus estimated parameters is not aligned in the extracted text, making it hard to read. Please format it with proper columns and report the error metric used to define 'relative error around 1%'.","section":"§4.1, Example 1"},{"comment":"The reference 'Bassik et al. (2023)' appears to be for a preprint (Robust parameter estimation for rational ordinary differential equations) but no DOI or arXiv identifier is given. Other entries have missing DOIs; adding them would improve reproducibility.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The inconsistency in §4.1 appears to be a typo in the printed constants rather than a fundamental flaw in the method, since the printed solutions match the correct derivatives of the stated interpolant. However, the broader issue of the unquantified interpolation/differentiation step is not a typo and directly affects the 'guaranteed correct' claim for identification. The paper is primarily a software demonstration with moderate novelty; its main value is the integration of certified tools into a usable Julia package with reproducible examples. With the numerical example corrected and the certification claims qualified, it would be a solid contribution to a systems/software-oriented venue."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, PACE.jl looks like a real contribution: a coherent Julia package that wraps RUR, discriminant varieties, Sturm-Habicht sequences, partial CAD, and MPFI, with runnable notebooks for three control applications. Second, the main identification example in Section 4.1 is internally inconsistent as written, and the stress-test note is right about the arithmetic. I checked it myself: the stated rational interpolant gives y(0)=2.000, y'(0)≈1.083, and y''(0)≈0.652, not 1.000, 0.608, and 0.227. And neither printed solution (µ,x0)=(±0.604,1.000) or (µ,x0)=(±0.427,−2.000) satisfies the displayed first equation 1.000=x0²+x0. This looks like a typo—probably the numbers should be 2.000, 1.083, 0.652, and then x0=1.000 works—but as published it invalidates the only complete identification demonstration.\n\nWhat the paper does well: the underlying algorithms are prior literature, properly cited (Rouillier, Lazard–Rouillier, Bouzidi et al.), and the new integration is genuinely useful. The NF-kB example shows a 73-variable polynomial system solved certifiedly in seconds, with about 1% error and refinement to 6 digits. The stability and H-infinity examples are plausible and follow the cited strategies, though I did not independently verify those outputs. The notebooks are a plus; reproducibility is real.\n\nThe soft spots are two. The numerical inconsistency is the obvious one and must be fixed. The subtler issue is that the certification guarantee covers the polynomial system, not the reduction from data to that system. The paper says results are \"guaranteed to be correct\" without qualification, but in Section 4.1 the derivatives come from interpolating noisy data, and no error bound is given for that step. The solver certifies the approximate system, not the parameter-estimation problem. That is an overreach in the abstract and conclusion.\n\nThe citation pattern is honest; self-citations are to the authors' own published algorithms, which is appropriate here. No invented entities, no circular fitting.\n\nWho should read this: people working on symbolic computation for control, and anyone considering a certified polynomial solver in Julia. With the example fixed and the guarantee qualified, I would take it. As is, it deserves a serious referee, but not acceptance without that correction. I'd also ask the authors to confirm the notebooks reproduce the printed outputs exactly.\n\nMy recommendation: send it to peer review with a request for a careful revision of Section 4.1 and a caveat about the interpolation step.","headline":"A genuinely useful Julia toolbox for certified polynomial solving, but the paper's only complete identification example has inconsistent numbers and the 'guaranteed to be correct' language outruns what is actually certified.","tokens_in":10845,"tokens_out":3019,"would_cite":false,"duration_ms":29922,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68W30","93B40"],"pacs":[],"model":"deepseek-v4-flash","headline":"A Julia package brings certified exact solving to control-theory problems.","keywords":["PACE.jl","certified computation","symbolic elimination","rational univariate representation","discriminant variety","parameter identification","structural stability","H-infinity norm"],"falsifier":"Differentiate the rational interpolant $\\hat{y}(t) = \\frac{7.40t + 54.02}{1.52t^2 - 10.93t + 27.01}$ at $t=0$ and compare with the printed equations $1.000 = x_0^2 + x_0$, $0.608 = 2x_0x'_0 + x'_0$, $0.227 = 2x'_0{}^2 + 2x_0x''_0 + x''_0$. The interpolant gives $y(0) = 2.000$, $y'(0) \\approx 1.083$, and $y''(0) \\approx 0.652$, so the printed system cannot be the evaluation of the stated interpolant; reproducing the code would show which half of the example is in error.","tokens_in":9870,"feed_emoji":"🎛️","tokens_out":7824,"duration_ms":71780,"temperature":0.7,"pith_summary":"The paper presents PACE.jl, a Julia package that wraps symbolic elimination algorithms—discriminant varieties, Rational Univariate Representation, Sturm–Habicht sequences, interval Newton refinement, and cylindrical algebraic decomposition—and applies them to three control-theory tasks. It claims that these tasks can be solved with guarantees of correctness: parameter estimation from ODE data, structural stability of multidimensional systems, and $H_\\infty$-norm computation. The payoff is that outputs come as isolating intervals or rational descriptions of the solution set, so a user can trust the result without relying on heuristic numerical iteration. Demonstrations include a 16-state NF-kB identification model, a parametric two-dimensional stability test, and a transfer-matrix norm example.","feed_headline":"PACE.jl brings certified exact solving to control problems","feed_subtitle":"Parameter identification, stability checks, and H-infinity norms come back as guaranteed intervals, not numerical guesses.","key_machinery":"The engine is the certified solving pipeline: from a polynomial system with rational coefficients, compute a Rational Univariate Representation (RUR), a rational parametrization of the zero-dimensional solution set by a univariate polynomial; then isolate the real roots of that univariate polynomial in rational-bounded intervals and refine with multi-precision interval Newton steps. For parametric problems, discriminant varieties mark parameter values where the solution behavior can change, and the cells of maximal dimension of a cylindrical algebraic decomposition give regions where stability is uniform. The Sturm–Habicht sequence is the sign-counting device used for real-root counting and for the $H_\\infty$ computation. These objects, not a single theorem, carry the certification.","core_discovery":"On its own terms, the paper claims that a bundle of classical exact-computation tools can be wrapped into a single Julia package and solve control problems with certifiable outputs. In parameter identification, the ODE is differentiated repeatedly and evaluated at an interpolant of the data, yielding a polynomial system whose Rational Univariate Representation isolates all candidate parameters and initial states, which can then be refined to arbitrary precision. In stability analysis of multidimensional systems, structural stability of a transfer-function denominator is reformulated as a real algebraic condition, and parametric stability regions are classified by computing a discriminant variety and cell decomposition. In $H_\\infty$-norm computation, the norm is located as the maximal real $\\gamma$-projection of solutions of a zero-dimensional polynomial system, obtained via Sturm–Habicht sign variations. The outputs in all three settings are intervals with rational bounds that are guaranteed to contain the true value.","pith_inferences":["Because every candidate parameter set is enumerated as an isolated solution, identifiability itself is certified in practice: if the polynomial system has a unique real solution consistent with the domain and sign constraints, the parameters are identifiable under the stated reduction.","The derivative-estimation step is the natural place to push certification further: replacing the rational interpolant with interval-based derivative bounds, such as interval Taylor enclosures, would make the identification pipeline fully verified from data to parameters rather than verified only after the polynomial system is formed.","The same Sturm–Habicht machinery used for $H_\\infty$ on transfer matrices should extend to parametric transfer functions once discriminant-variety methods for the norm are implemented, which is the paper's announced next direction.","A corrected toy example would make the identification demonstration reproducible, since the printed constants do not match the stated interpolant; this is a simple check anyone can run before relying on the tool."],"forward_implications":["Certified parameter identification becomes a finite exact computation: all possible parameter vectors consistent with the data appear as isolated solutions of the polynomial system, and each can be refined to any requested precision.","Structural stability of a parametric multidimensional system can be certified region by region, with a sample point returned for every stable and unstable region, so no exhaustive simulation search is needed.","$H_\\infty$ norms can be returned as rigorous intervals whose width shrinks as the requested precision grows, making them usable as certificates in robustness analysis.","The same pipeline handles both parameter-free and parameter-dependent systems, so a user can solve one parametric model and obtain all stability regions at once."],"supporting_citations":[{"why":"defines the Rational Univariate Representation used to encode all solutions of a zero-dimensional polynomial system.","marker":"Rouillier (1999)"},{"why":"introduces discriminant varieties, which are used to split parameter space into regions with uniform solution behavior.","marker":"Lazard and Rouillier (2007)"},{"why":"supplies the reduction of ODE parameter estimation to solving a polynomial system, the starting point of the identification section.","marker":"Bassik et al. (2023)"},{"why":"provides the certified non-conservative stability test for multidimensional systems, including the Möbius change of variables.","marker":"Bouzidi et al. (2019)"},{"why":"gives the symbolic methods for computing the L-infinity / H-infinity norm as the maximal gamma-projection of a zero-dimensional system.","marker":"Bouzidi et al. (2021)"},{"why":"defines Sturm–Habicht sequences and the sign-variation technique used for real-root counting.","marker":"González-Vega et al. (1998)"},{"why":"states the criterion gamma greater than the norm that reduces the norm computation to checking a determinant.","marker":"Kanno and Smith (2006)"},{"why":"reduces structural stability of n-D systems to univariate conditions plus one multivariate condition.","marker":"Decarlo et al. (1977)"}],"fun_headline_variants":["PACE.jl delivers certified intervals for control problems","PACE.jl: exact solving, guaranteed control outputs","Control certification via PACE.jl algebraic tools","PACE.jl wraps exact algebra for verified control answers","Certified control: PACE.jl with interval guarantees"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The identification pipeline rests on the assumption that the polynomial system obtained from the differentiated ODE and the estimated derivatives faithfully represents the true data; in the printed toy example the recorded derivative values do not match the stated rational interpolant, so that step is not actually certified as written.","fun_headline_variants_meta":{"raw":{"variants":["PACE.jl delivers certified intervals for control problems","PACE.jl: exact solving, guaranteed control outputs","Control certification via PACE.jl algebraic tools","PACE.jl wraps exact algebra for verified control answers","Certified control: PACE.jl with interval guarantees"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000272,"raw_usage":{"total_tokens":1547,"prompt_tokens":774,"completion_tokens":773,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":390,"completion_tokens_details":{"reasoning_tokens":695}},"tokens_in":390,"tokens_out":773,"duration_ms":7255,"temperature":1.0,"reasoning_tokens":695,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:38:12.535020+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Differentiate the rational interpolant $\\hat{y}(t) = \\frac{7.40t + 54.02}{1.52t^2 - 10.93t + 27.01}$ at $t=0$ and compare with the printed equations $1.000 = x_0^2 + x_0$, $0.608 = 2x_0x'_0 + x'_0$, $0.227 = 2x'_0{}^2 + 2x_0x''_0 + x''_0$. The interpolant gives $y(0) = 2.000$, $y'(0) \\approx 1.083$, and $y''(0) \\approx 0.652$, so the printed system cannot be the evaluation of the stated interpolant; reproducing the code would show which half of the example is in error.","supporting_citations":[{"cited_title":"and Rouillier, F","cited_arxiv_id":null,"evidence_quote":"introduces discriminant varieties, which are used to split parameter space into regions with uniform solution behavior."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"supplies the reduction of ODE parameter estimation to solving a polynomial system, the starting point of the identification section."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the certified non-conservative stability test for multidimensional systems, including the Möbius change of variables."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"gives the symbolic methods for computing the L-infinity / H-infinity norm as the maximal gamma-projection of a zero-dimensional system."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"defines Sturm–Habicht sequences and the sign-variation technique used for real-root counting."},{"cited_title":"and Smith, M.C","cited_arxiv_id":null,"evidence_quote":"states the criterion gamma greater than the norm that reduces the norm computation to checking a determinant."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"reduces structural stability of n-D systems to univariate conditions plus one multivariate condition."}],"review_version":1}