{"id":"a3d7f101-6220-4980-99cb-6bafb1a297f7","arxiv_id":"2602.06737","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A knapsack-optimized piecewise-affine abstraction yields tighter verified output ranges for KANs than uniform piece allocation.","lead":"This paper describes a method for verifying Kolmogorov-Arnold Networks by replacing each learnable univariate activation with a piecewise-linear approximation carrying a bounded error, then allocating a fixed 'piece budget' across the network via a knapsack-style optimization. The authors report tighter verified output ranges than a uniform allocation baseline on 59/65 KAN benchmarks, though formal soundness of the error bounds needs clarification.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The DP's per-unit errors are grid errors unless the Appendix A correction is applied, but Section 7 never states that it was; if uncorrected, the reported 'verified' bounds are not guaranteed over-approximations.","rationale":"The reader's weakest assumption identifies the same point: the per-unit error used in the knapsack and MILP must be a valid continuous error bound, not merely the discretized error. This is exactly the load-bearing concern. The paper itself flags the issue in Section 4 and Appendix A, but the experiments section omits any statement that the correction was applied, making the reported 'verified' bounds unsubstantiated. If the correction is missing, Theorem 1's bound is unsound and the empirical tightness comparison is not a comparison of verified bounds. The reader's CONDITIONAL verdict remains appropriate because the issue is fixable by applying the correction or by choosing Δ small enough and stating so; it does not invalidate the overall approach. The malformed DP recurrence in Eq. (3) is a secondary reproducibility issue but not the central soundness problem.","tokens_in":18634,"tokens_out":6161,"duration_ms":73954,"concrete_test":"Recompute the F-xy KAN benchmark from scratch: build the trade-off tables using singlePieceError = grid_error + (cmax + ψ′max)Δ as in Theorem 4, then run the knapsack allocation and MILP encoding exactly as in Section 6. If the resulting output interval is wider than the KANO row in Table 1, or if it no longer contains the output range obtained by a fine global search on the original KAN, then the published bound relied on uncorrected grid errors and the central soundness claim fails. If the interval is unchanged, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's core soundness argument rests on Theorem 1, which bounds the overall KAN approximation error by Σ W(i)j,k × e(i)j,k. This is only valid if each e(i)j,k is a true bound on max_{z∈[-L,L]} |ψ(z) − ψ̂(z)|. However, Section 4 defines the DP objective as the discretized error e(Δ) over grid points, and only says the Appendix A correction 'can be used' to lift it to the continuum. The experimental section never states that singlePieceError or the trade-off tables actually add the correction term (cmax + ψ′max)Δ from Theorem 4. If the raw grid error is used, the MILP's error slack is too small, and the output intervals reported in Tables 1–3 are not guaranteed to contain the true KAN outputs. This directly undermines the central claim: a 59/65 tightness advantage over uniform allocation is only meaningful if the optimized abstraction is actually sound. The issue is fixable by applying Theorem 4 or choosing Δ small enough, but the manuscript as written does not establish that this was done. (A secondary issue is that the DP recurrence in Eq. (3) appears malformed, but that is a reproducibility concern; the discretization gap is the load-bearing soundness concern.)","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a verification framework for Kolmogorov-Arnold Networks (KANs) in which each univariate activation is replaced by a piecewise affine (PWA) approximation with a certified error. A dynamic programming routine is used to compute per-unit error-vs-piece trade-off tables, Theorem 1 derives a global error bound as a weighted sum of per-unit errors with weights given by path products of downstream Lipschitz constants, and the resulting allocation problem is formulated as a multi-choice knapsack problem. The abstracted network is then encoded in a MILP for range verification. The experiments compare the optimized abstraction against a vanilla uniform-piece abstraction on 65 KAN benchmarks and also compare KAN verification with MLP verification using Gurobi and LiRPA. The central claim is that the optimized abstraction produces tighter output intervals than the uniform allocation on 59 of 65 benchmarks at comparable cost.","tokens_in":18945,"tokens_out":14635,"duration_ms":172568,"significance":"If the identified gaps are fixed, the paper would make a useful contribution: the path-weighted error propagation in Theorem 1 is a clean structural idea, the reduction to multi-choice knapsack gives a principled way to allocate a limited number of PWA pieces, and the experimental corpus is broad and relevant. The paper also explicitly targets a gap in the literature, since KAN verification is relatively unexplored. However, the current manuscript does not fully establish the soundness of the reported verification bounds: the connection between the discretized DP error and the continuous error needed for verification is not shown to be enforced in the experiments, and the DP recurrence as written does not implement the claimed optimization. These issues are load-bearing for the paper's main claim and must be resolved before the results can be accepted.","major_comments":[{"comment":"The MILP constraints in Section 6 add an independent ±e slack at each unit, producing an over-approximation by allowing the per-unit errors to vary independently. Theorem 1 instead gives a single weighted global slack. The paper does not explain how the knapsack allocation, which is derived from the weighted bound, relates to the actual MILP bound. This may be an intended design choice, but it should be stated explicitly, since otherwise the connection between the theoretically optimized allocation and the empirically reported output widths is unclear.","section":"§6, MILP encoding"}],"minor_comments":[{"comment":"Typo: 'singplePieceError' should be 'singlePieceError'.","section":"§4"},{"comment":"The choice δ = 3.4 × δ_min is not motivated. Since this parameter controls the trade-off between tightness and the number of pieces, a brief explanation or an ablation would help the reader interpret the results.","section":"§7.1"},{"comment":"The full-text title, 'Optimal Abstractions for Verifying Properties of Kolmogorov-Arnold Networks (KANs)', differs from the arXiv title. These should be harmonized.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The paper is potentially a solid contribution to KAN verification, but the current version has a reproducibility-critical DP bug and an unresolved discretization-to-continuum gap that directly affect the soundness of the experimental claims. Both are fixable within the scope of a revision, so I recommend major revision rather than rejection. I would also encourage the authors to clarify the treatment of the outer univariate functions in Theorem 1, since the current indexing appears incomplete."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a useful paper for KAN verification, not a revolutionary one. The genuinely new piece is treating per-unit PWA error budgets as a multi-choice knapsack over the KAN graph, with path-Lipschitz weights converting local errors into a global bound. That framing is clean and, as far as I know, not in the cited KAN-verification literature. The local DP for best k-piece linearization is Bellman's algorithm, and the error propagation is standard CROWN-style Lipschitz accounting, but the integration is new and the empirical claim—optimized allocation beats uniform on 59/65 benchmarks—is credible as a trend.\n\nWhat it does well: the experiments span meaningful sizes and tasks, the comparison against MLP verifiers is useful, and Table 2 reports wins/losses/ties without hiding the losses. The sensitivity analysis is a nice demonstration of amortized abstraction over one precomputed model.\n\nSoft spots, in order of importance. First, the soundness gap in presentation. Theorem 1 is only valid if each e(i) is a bound over continuous z, not just grid points. Section 4 acknowledges discretization error and derives Theorem 4 in the appendix as a correction to singlePieceError, but the experimental section never states that the correction was applied, nor does it say how delta was chosen relative to the continuous error. Without that explicit statement, the reported 'verified' bounds are not guaranteed over-approximations. This is exactly the load-bearing issue, and it is fixable by stating that the corrected singlePieceError is used or by proving delta is small enough for all units. Second, the DP recurrence in Eq. (3) is malformed: the first two cases cover all values of \\hat{k}, making the recursive case dead code. Probably a typo in the conditions, but as printed it cannot be reproduced. Third, the knapsack formulation assumes integer weights after scaling by a constant; the paper asserts this without discussing the precision or rounding error introduced. Minor for practice, but it should be said. Fourth, the 'roughly comparable' runtime claim does not line up with Table 1: KANO is often much slower, e.g., 108s vs 7.5s on Weather, 485s vs 1.8s on Prosthetic. The overhead may be amortizable, but as presented it is an overstatement.\n\nWho this is for: verification researchers working on KANs, and anyone using MILP-based range analysis with learned univariate splines. It deserves serious referee time, conditional on clarifying the discretization correction and fixing the DP equation. I would send it to review.","headline":"The knapsack-style allocation of PWA pieces across KAN units is a real and useful idea, with an honest 59/65 tightness win over uniform allocation, but the paper's central soundness claim depends on a discretization-to-continuum correction that the main text never says was applied.","tokens_in":19485,"tokens_out":3063,"would_cite":false,"duration_ms":35992,"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":"Verifying a KAN reduces to deciding how many linear pieces each activation gets, with error allocated like a knapsack budget.","keywords":["Kolmogorov-Arnold networks","neural network verification","piecewise affine abstraction","range analysis","knapsack problem","dynamic programming","mixed-integer linear programming","Lipschitz error propagation"],"falsifier":"Take any single KAN activation on a bounded interval, build the trade-off table with a coarse discretization step, and omit the discretization correction; then compute max_z |ψ(z) − ψ̂(z)| densely (or by exact optimization). If the dense or true error exceeds the tabulated e, the abstraction is unsound. A network-level falsifier is to verify a small KAN with the optimized method, then evaluate the original network with a global optimizer over the input box: any true output outside the claimed interval refutes the soundness claim.","tokens_in":18501,"feed_emoji":"📐","tokens_out":7348,"duration_ms":77872,"temperature":0.7,"pith_summary":"Kolmogorov-Arnold networks replace fixed activations with learned univariate functions, which makes formal verification hard because the usual ReLU-style reasoning does not apply. The paper's central claim is that this difficulty can be managed by replacing every activation with a piecewise-linear approximation that carries a bounded error, and then choosing how many linear pieces to spend on each activation as a global budget-allocation problem. The key theorem states that the total approximation error of the whole network is bounded by a weighted sum of per-activation errors, where each weight counts all output paths through downstream Lipschitz constants. That structure turns the choice of approximations into a multi-choice knapsack problem, solvable by dynamic programming, and the resulting abstraction is encoded as a mixed-integer linear program for range verification. Across 65 KAN benchmarks, the optimized allocation yields tighter verified output ranges than a uniform piece allocation, with comparable overall verification time.","feed_headline":"Budgeting linear pieces tightens verified KAN bounds on 59 of 65 tests","feed_subtitle":"Putting more linear segments where Lipschitz-weighted error matters most yields tighter verified output ranges.","key_machinery":"The load-bearing identity is Theorem 1: |y − ŷ| ≤ Σ W(i)j,k e(i)j,k, with the weights W(i)j,k defined as the sum over all paths from unit ψ(i)j,k to the network output of the products of downstream Lipschitz constants. This additive decomposition is what converts a network-level approximation problem into a per-unit budgeting problem: once each unit has a dynamic-programming 'trade-off table' listing the best error achievable with k linear pieces, choosing how many pieces to give every unit under a total error budget is a multi-choice knapsack problem. The weighted error bound therefore determines both the objective and the feasibility of the allocation, and the resulting piecewise-linear ne","core_discovery":"On its own terms, the paper establishes that the best verified output range for a KAN is obtained by treating abstraction quality as a scarce resource. For every activation ψ(i)j,k, replacing it by a piecewise-linear function with error e(i)j,k contributes at most W(i)j,k · e(i)j,k to the final output error, where W(i)j,k is the sum, over every path from that activation to the output, of the products of the Lipschitz constants of the downstream activations along that path. Summing these contributions bounds the global error, so minimizing total error for a fixed number of pieces is exactly a multi-choice knapsack problem. The paper computes per-activation trade-off tables with dynamic progra","pith_inferences":["The paper leaves implicit that the knapsack view also gives a dual formulation: instead of fixing total pieces and minimizing error, one could fix an error budget and ask for the cheapest MILP (fewest total pieces), yielding the same DP machinery as a Pareto frontier over verification cost and bound tightness.","Because the error decomposition only uses path products of Lipschitz constants and the additivity of KAN layers, a natural testable extension is applying the same weighted-budget allocation to other additive or residual architectures; the paper does not claim this, but the Theorem 1 proof structure suggests it.","A straightforward experiment to stress the soundness claim is to compare the verified interval against exact nonlinear global optimization on small KANs: if the discretization correction is omitted or the grid is too coarse, the verified interval may exclude true outputs, so the correction is not a formality but load-bearing.","The reported sensitivity numbers (output changes of 8.6°C and 23.8° in weather and prosthetic models under 0.01 perturbations) suggest that practitioners should treat these KAN models as highly non-robust; that is an editorial reading of the paper's application study, not a claim the paper generalizes."],"forward_implications":["If the central bound holds, optimizing piece allocation rather than using a fixed number of segments per activation gives tighter verified output ranges; the paper reports 59 of 65 benchmarks improved over uniform allocation.","Range verification of a KAN becomes solvable by standard MILP solvers, so nonlinear learned activations no longer require a bespoke verifier.","The abstraction can be computed once and reused: sensitivity analysis that sweeps many input perturbations becomes cheap because the per-unit tables and knapsack solution are amortized.","The same pipeline applies to any activation satisfying the paper's mild assumptions (bounded domain, differentiability, and an interval procedure for derivatives), including spline, Chebyshev, Fourier, and other KAN variants.","The tightness guarantee is quantitative: for a chosen δ, the returned output interval is within δ of the true attainable range, so users control the precision/cost trade-off explicitly."],"fun_headline_variants":["Knapsack-based piece allocation shrinks verified KAN bounds","DP-optimized PWA abstractions tighten neural net range proofs","Optimal linear-piece budget yields tighter KAN verification","Allocate pieces wisely: knapsack approach tightens KAN bounds"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole soundness argument rests on each tabulated per-activation error e(i)j,k being a genuine upper bound on the continuous error between the activation and its piecewise-linear approximation over the entire input range, not merely the error on the discrete grid used by the dynamic program.","fun_headline_variants_meta":{"raw":{"variants":["Knapsack-based piece allocation shrinks verified KAN bounds","DP-optimized PWA abstractions tighten neural net range proofs","Optimal linear-piece budget yields tighter KAN verification","Allocate pieces wisely: knapsack approach tightens KAN bounds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00024,"raw_usage":{"total_tokens":1413,"prompt_tokens":864,"completion_tokens":549,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":608,"completion_tokens_details":{"reasoning_tokens":477}},"tokens_in":608,"tokens_out":549,"duration_ms":6008,"temperature":1.0,"reasoning_tokens":477,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T06:07:01.979698+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any single KAN activation on a bounded interval, build the trade-off table with a coarse discretization step, and omit the discretization correction; then compute max_z |ψ(z) − ψ̂(z)| densely (or by exact optimization). If the dense or true error exceeds the tabulated e, the abstraction is unsound. A network-level falsifier is to verify a small KAN with the optimized method, then evaluate the original network with a global optimizer over the input box: any true output outside the claimed interval refutes the soundness claim.","supporting_citations":[],"review_version":1}