{"id":"2df2ffc9-ffbd-4956-9239-4a8894379858","arxiv_id":"2412.08739","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"VEL is a Coq-verified EL++ subsumption reasoner with extracted OCaml code; the formalization found two errors in Baader et al.'s completeness proof and fixed them with an A-extension and a strengthened lemma.","lead":"A team built VEL, a reasoner for the OWL2 EL logic whose correctness is checked by the Coq proof assistant and then turned into runnable OCaml code. The project found and fixed two gaps in the original 2005 correctness proof of the underlying algorithm, one involving a missing transitivity property and one under-specifying concrete-domain solutions.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Extracted code's unverified concrete-domain solvers and 64-bit int extraction break the end-to-end soundness/completeness guarantee claimed for runnable outputs.","rationale":"The reader's weakest assumption exactly identifies the unverified concrete-domain oracles and native-int extraction as the point where the end-to-end guarantee breaks. My read of the paper confirms that the Coq theorem itself is stated about an idealized function whose concrete-domain checker is specified but not implemented in Coq, and that the shipped executable substitutes unverified OCaml code and possibly overflowing integers. This is a genuine correctness risk for the central claim if the abstract is interpreted as covering the runnable artifact. The reader's conditional acceptance is appropriate: the formal development may be valuable, but the paper does not provide the Coq artifact, and even with it, the extracted code's correctness would remain contingent on the unverified TCB components. An honest limitation statement already appears in the TCB and Extraction sections, so the paper does not hide the issue; nonetheless, the strength of the 'all possible inputs' claim in the abstract exceeds what the machine-checked proofs establish for the executable. I agree with the reader's verdict and see no reason to move it; the concrete test above would either confirm the risk or demonstrate that the unverified components are correct on the tested inputs.","tokens_in":11380,"tokens_out":12118,"duration_ms":123785,"concrete_test":"Differentially test the OCaml concrete-domain satisfiability and implication checkers against an independent reference implementation (e.g., brute-force enumeration over a bounded set of rational and string values) on randomly generated predicate conjunctions with up to, say, 6 predicates and 3 feature names. Any mismatch between the unverified checker and the reference for a test case directly invalidates the end-to-end soundness/completeness guarantee for the extracted reasoner on inputs that involve that conjunction.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 2 states a Coq theorem about the abstract `check_subsumption` function, but the paper's end-to-end claim is about the extracted OCaml reasoner. The 'String and Rational Number Domains' section says satisfiability and implication checks for concrete domains are delegated to an 'unverified OCaml program' using GLPK and OCamlgraph; the 'Extraction' section replaces Coq naturals and integers with 64-bit OCaml ints, acknowledging possible overflow unsoundness. The 'Trusted Computing Base' lists these unverified components as trusted, but the abstract asserts 'machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs' for the reasoner. If the GLPK-based linear program checker or the OCamlgraph string-implication checker returns a wrong answer on some input, or if a rational coefficient exceeds 2^63-1, the extracted `check_subsumption` can return a result that contradicts Theorem 2. The formal theorem holds only for the idealized Coq function, which relies on a specification axiom for the concrete-domain checker; the actual runnable code's correctness is not machine-checked. This gap is the load-bearing weakness for any claim that VEL provides verified reasoning on all inputs.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents VEL, a Coq formalization of a subsumption checker for the EL++ description logic, following the algorithm of Baader, Brandt, and Lutz. The formalization covers the EL++ language, semantics, normalization, a newly introduced A-extension step, and classification, and it culminates in Theorem 2, a Coq statement that the checker function is sound and complete with respect to EL++ subsumption. The authors extract OCaml code from the Coq development, add rational-number and string concrete domains backed by GLPK and OCamlgraph, and argue that the machine-checked proofs ensure correctness of the reasoner's outputs for all inputs. They also report discovering two errors in the original completeness proof, which motivate the A-extension and a strengthened concrete-domain solution lemma.","tokens_in":11642,"tokens_out":3023,"duration_ms":32188,"significance":"If the Coq development is as described, this would be a substantial contribution to verified reasoning: it mechanizes the semantics of EL++, provides a machine-checked proof of a nontrivial classification algorithm, identifies genuine gaps in a well-known pen-and-paper proof, and introduces reusable proof techniques such as role trees. The A-extension and the strengthened solution-existence lemma are concrete, falsifiable improvements over the original completeness argument. The paper also demonstrates a working extraction pipeline with two concrete domains. However, the advertised end-to-end guarantee for runnable outputs currently rests on unverified components and an acknowledged overflow risk, so the significance of the work as a verified reasoner depends on the authors closing or precisely qualifying that gap.","major_comments":[{"comment":"The paper states that satisfiability and implication checks for concrete domains are delegated to an unverified OCaml program using GLPK and OCamlgraph, and the Trusted Computing Base section lists these as trusted. This means Theorem 2, which is proved for the Coq function check_subsumption, does not by itself establish correctness of the extracted reasoner. If the unverified checker returns a wrong answer, the runnable code can contradict Theorem 2. The authors should make explicit how the Coq formalization interfaces with these unverified calls (e.g., as axioms or assumed specifications), and should either prove the checkers correct or clearly state that the end-to-end guarantee applies only to the Coq function, not the extracted executable.","section":"String and Rational Number Domains / Trusted Computing Base"},{"comment":"The Extraction section acknowledges that extracting Coq naturals and integers to 64-bit OCaml ints introduces possible overflow unsoundness. Since Theorem 2 quantifies over all inputs and the abstract claims \"validity of outputs across all possible inputs,\" the extracted code does not meet that claim. The authors should either use Coq's default extraction to unbounded integers, or restrict the correctness statement to inputs and intermediate values that fit in 64 bits, with a clear statement that the extracted program is not guaranteed to be sound on all inputs.","section":"Extraction"},{"comment":"No artifact, repository link, or commit hash is provided, so the reader cannot inspect the Coq definitions, the proof scripts, or the extraction setup. For a formal-verification paper, the machine-checked proofs are the main evidence, and a named version of the development is essential for reproducibility. The authors should make the Coq development and the extracted OCaml code available and reference a specific commit or version in the paper.","section":"General (artifact availability)"}],"minor_comments":[{"comment":"The function signature in Listing 2 appears to contain a typo: check_subsumption(C, C, D) uses C twice, likely intending check_subsumption(C, C, D) with distinct arguments; this should be corrected for clarity.","section":"Listing 2"},{"comment":"The performance table shows highly non-monotonic runtimes (e.g., concept inclusions go from 4s at 20 constraints to 278s at 30 constraints and 192s at 40 constraints), with no error bars, number of runs, or explanation of variance. If the evaluation is meant to support scalability claims, it needs a more systematic methodology; otherwise it should be presented as anecdotal.","section":"Evaluation"},{"comment":"The proof-effort numbers (165 definitions, 387 theorems, 11.3x proof overhead) are useful, but the paper does not state which version of Coq or which library dependencies (other than mlvoqc) were used; this information should be added for reproducibility.","section":"Evaluation"},{"comment":"The Trusted Computing Base lists \"OCaml run-time and libraries\" and GLPK, but it does not mention the extraction mechanism itself or the axioms used for the concrete-domain checkers; the TCB should be stated in terms of the logical assumptions and the code-generation trust boundary.","section":"Trusted Computing Base"}],"recommendation":"major_revision","confidential_remarks":"The core formalization appears plausible and the claimed discovery of errors in Baader et al.'s proof is interesting, but the paper's central claim of a fully verified reasoner is currently overstated because the runnable code depends on unverified concrete-domain solvers and an overflow-prone integer extraction. I would be willing to reconsider after the authors provide the artifact, state the theorem precisely for the extracted program, and either verify or explicitly unclaim the concrete-domain checkers. The performance evaluation is too noisy to be load-bearing and should be either strengthened or downplayed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague, here's my take on VEL. The genuine core is the Coq formalization of the EL++ classification algorithm and the two concrete-domain extensions, and the discovery of two real gaps in Baader et al.'s pen-and-paper completeness proof: the non-transitivity of the ~ relation and an under-specified solution lemma. The A-extension fix is a clean way to force nonemptiness, and the modified NF2 rule addresses a termination issue. These are substantive, checkable contributions, and the paper is honest about its TCB.\n\nThe soft spots are real but should be proportioned. The biggest issue is the gap between the theorem and the extracted code. Theorem 2 is about the Coq function `check_subsumption`, which is parameterized by an assumed specification for the concrete-domain satisfiability/impl checkers. The actual runnable OCaml calls unverified GLPK and OCamlgraph-based programs, and Coq's unbounded naturals/integers are extracted to 64-bit ints. So the abstract's 'all possible inputs' claim is not supported for the executable. The paper does state this in the TCB section, so it's not hidden, but it is undersold. That may be an acceptable engineering tradeoff, but it should front the paper.\n\nNo artifact or commit hash is shipped, which for a verified-systems paper is a serious omission. I can't check the Coq development. That alone warrants conditional acceptance, not rejection.\n\nThe performance evaluation is too sketchy to mean much: random KBs, high variance, 192s for 40 constraints. Not a strong point.\n\nThe proof-effort ratio (11.3x) is plausible and gives a sense of scale. The role-tree invariant is an elegant way to mechanize the completeness argument; I'd like to see more detail on how it avoids the 'induction over selected rule applications' problem.\n\nBottom line: this deserves a serious referee. If the proofs are real, it's a useful addition to the verified-reasoning literature and the first EL++ reasoner with string and rational concrete domains in Coq. But the authors need to ship the artifact, clarify exactly what Theorem 2 covers, and soften the abstract's end-to-end claim.","headline":"Solid formalization work with real proof fixes, but the end-to-end guarantee is oversold and the missing artifact makes the machine-checked claims unverifiable.","tokens_in":12143,"tokens_out":3502,"would_cite":true,"duration_ms":32515,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper establishes that VEL, a formally verified EL++ reasoner, is sound and complete for every input, with the proof machine-checked and executable OCaml code extracted from it.","keywords":["formal verification","description logic","EL++","OWL2 EL profile","subsumption checking","concrete domains","proof extraction","machine-checked proofs"],"falsifier":"Run the extracted reasoner on a knowledge base whose rational-number constraints force arithmetic beyond a 64-bit integer, or where the external solver's answer differs from the mathematical satisfiability of the constraint conjunction; a wrong subsumption verdict would refute the end-to-end guarantee for the runnable code.","tokens_in":11217,"feed_emoji":"✅","tokens_out":11474,"duration_ms":110438,"temperature":0.7,"pith_summary":"VEL is a reasoner for the EL++ description logic that underlies the OWL2 EL profile, and its central claim is that the reasoner's subsumption answers are guaranteed correct for every possible input. Subsumption here means the question of whether one concept is logically forced to be a subclass of another under the ontology. The authors prove this guarantee with machine-checked proofs and then extract executable OCaml code from the verified definitions, so the guarantee is carried by the code itself rather than by any test suite. The proof effort also found two real errors in the published completeness proof of the base algorithm, which the authors repaired by changing the algorithm.","feed_headline":"Formally verified reasoner answers every EL++ subsumption query","feed_subtitle":"Machine-checked proofs cover every input and exposed two errors in the original algorithm.","key_machinery":"The load-bearing objects are the normalized CBox and the classification records $S$ and $R$: $S$ maps each concept description to the concept descriptions it subsumes, and $R$ maps each role to the pairs of concept descriptions it relates. The repaired algorithm runs transformation, normalization, A-extension, and classification before checking whether $B$ (or $\\bot$) appears in $S(A)$. A-extension adds a fresh individual $t$ and role $r_t$ with the axiom $\\{t\\} \\sqsubseteq \\exists r_t.A$, forcing $A$ to be nonempty in every model and restoring transitivity of the $\\sim$ relation. The completeness proof is carried by role trees, an inductive structure recording how a pair $(C,D)$ entered $R(r)$ through the rules CR3, CR10, and CR11, which lets the proof maintain an invariant at every classification step instead of inducting over groups of rule applications.","core_discovery":"The central result is Theorem 2: for every knowledge base $\\mathcal{C}$ and concept descriptions $C,D$, $\\texttt{check\\_subsumption}(\\mathcal{C},C,D)=\\texttt{true}$ exactly when $C \\sqsubseteq_{\\mathcal{C}} D$. Soundness and completeness are proved inside an interactive proof assistant for the full pipeline, namely transformation, normalization, A-extension, classification, and the final subsumption test, and the verified functions are extracted into runnable OCaml. Mechanizing the published completeness argument exposed two defects in it: the $\\sim$ relation on reachable concept descriptions is not transitive in models where the queried concept $A$ has an empty extension, and the lemma that builds counterexample solutions for concrete-domain predicates was underspecified. The paper's fixes are an A-extension preprocessing step that forces $A$'s extension to be nonempty in all models, a modified normalization rule NF2, and a strengthened solution-existence lemma, with the remaining trust in the unverified concrete-domain checkers made explicit.","pith_inferences":["Beyond the paper, the A-extension device suggests a general recipe for repairing completeness proofs that implicitly need some concept to be nonempty: add a fresh nominal and role that force nonemptiness at the classification level.","Beyond the paper, the unverified concrete-domain checkers are the most promising boundary to attack next; replacing them with verified or proof-producing satisfiability procedures would make the end-to-end claim fully closed.","Beyond the paper, the role-tree invariant is a transferable technique for mechanizing completeness proofs that originally require induction over selected rule applications rather than single steps.","Beyond the paper, one could benchmark VEL against production EL reasoners after swapping the functional $S$ and $R$ representation for persistent maps, since the paper identifies the lookup overhead as the main performance cost."],"forward_implications":["The extracted OCaml reasoner's subsumption answers come with a static, machine-checked guarantee: no input can make it return a wrong answer, modulo the stated trusted computing base.","The two corrections, A-extension and the strengthened concrete-domain lemma, are necessary parts of the verified algorithm; the paper leaves open whether the original unmodified algorithm is complete.","The formalization provides a reusable semantic foundation for EL++ that other verified reasoners or ontology tooling can build on.","Because correctness is proved statically, the reasoner avoids runtime proof-certificate generation and checking, unlike validation-based approaches.","The supported concrete domains, rational numbers and strings, make the verified core usable on ontology queries that involve datatypes, at the price of trusting the unverified domain checkers."],"supporting_citations":[{"why":"Supplies the EL++ classification algorithm and the pen-and-paper soundness and completeness proofs that VEL formalizes and corrects.","marker":"Baader, Brandt, and Lutz 2005"},{"why":"Provides the proof assistant and extraction mechanism used to obtain the executable OCaml code.","marker":"The Coq Development Team 2024"},{"why":"Defines the linear-programming satisfiability algorithm for the rational-number concrete domain that the unverified checker implements.","marker":"Lutz 2002"},{"why":"Defines the graph-based satisfiability algorithm for the string concrete domain that the unverified checker implements.","marker":"Lutz 2004"},{"why":"Supplies the GLPK linear-programming solver that backs the unverified rational-number satisfiability checker.","marker":"Free Software Foundation 2024"},{"why":"Provides the extraction library used to map Coq numbers and strings to native OCaml types for better performance.","marker":"Hietala et al. 2021"}],"fun_headline_variants":["Verified EL++ reasoner fixes two completeness errors","Machine-checked proofs cover all inputs for EL++ subsumption","Coq-verified reasoner closes gaps in Baader et al. algorithm","Formal verification catches two flaws in OWL reasoner proof","Sound and complete: Coq-extracted reasoner for OWL2 EL"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The end-to-end guarantee is only as strong as the separately written, unverified programs that decide satisfiability and implication for rational-number and string constraints, plus the assumption that numbers never exceed 64-bit computer integers.","fun_headline_variants_meta":{"raw":{"variants":["Verified EL++ reasoner fixes two completeness errors","Machine-checked proofs cover all inputs for EL++ subsumption","Coq-verified reasoner closes gaps in Baader et al. algorithm","Formal verification catches two flaws in OWL reasoner proof","Sound and complete: Coq-extracted reasoner for OWL2 EL"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000196,"raw_usage":{"total_tokens":1352,"prompt_tokens":928,"completion_tokens":424,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":544,"completion_tokens_details":{"reasoning_tokens":334}},"tokens_in":544,"tokens_out":424,"duration_ms":4894,"temperature":1.0,"reasoning_tokens":334,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T17:36:37.878700+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the extracted reasoner on a knowledge base whose rational-number constraints force arithmetic beyond a 64-bit integer, or where the external solver's answer differs from the mathematical satisfiability of the constraint conjunction; a wrong subsumption verdict would refute the end-to-end guarantee for the runnable code.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the EL++ classification algorithm and the pen-and-paper soundness and completeness proofs that VEL formalizes and corrects."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the proof assistant and extraction mechanism used to obtain the executable OCaml code."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the linear-programming satisfiability algorithm for the rational-number concrete domain that the unverified checker implements."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the graph-based satisfiability algorithm for the string concrete domain that the unverified checker implements."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the GLPK linear-programming solver that backs the unverified rational-number satisfiability checker."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the extraction library used to map Coq numbers and strings to native OCaml types for better performance."}],"review_version":1}