About
    • AMMDI is an open-notebook hypertext writing experiment, authored by Mike Travers aka mtraven. It's a work in progress and some parts are more polished than others. Comments welcome! More.
Search
Page Contents
Full

Emergence/pre-engagement

12 Nov 2026 - 13 Nov 2026
Open in Logseq
    • Alright Emergence dude is probably for business stuff. My agenda
      • Pay (asked 250, accepted 150)
      • Deliverables / Expectations
      • Work process
        • (who do I report to, Paul presumably)
        • coding standards etc (prob not his baliwick)
      • Is this a trial run for full-time? I mean, doesn't have to be official but would be good to know thinking.
      • IP issues
    • Emergence consultng agreement notes
      • Name: should be "Michael Travers" throughout (legal name). I'd like to sign as d/b/a Hyperphor if that's OK.
      • Email is wrong, should be: mt@alum.mit.edu
      • 2.4: I don't mind agreeing to let Emergence use my name in publicity if I get the reciprocal right to use theirs
      • 2.1 and 2.6 contradict each other; I prefer the language in 2.6
      • Start date: How about Nov 23? Contract has Nov 30, I assume you prefer an earlier start. Note: if it will make setup easier could start even earlier with less than full time commitment.
      • 25K/month is slightly over 150/hr so that's good I guess
      • SOW
        • Some of the points are kind of vague. Guess that's ok.
    • Q for Ravi
      • really hard to estimate time these days. limiting factor not coding but understanding.
        • I've always been a learn-by-building guyt an dthings are different now
        • my usual model: find a domain expert, understand their problems and thought processes, build an ontology and tooling
      • scope
        • ontology curation (seems to be main focus)
          • what is current state? What are immediate goals?
        • ontology evolution
          • from nl docs
          • from domain experts in loop
          • automated
          • custtomer-deriven
        • ontology quality measurement
        • talk-to-data
        • how much integration/learning
      • work mode (people, tools, meetings, etc)
      • hyperphor tooling
    • Emergence work plan (pre official SOW)
      • NLP --> Ontology + logical axioms
      • They have ontology best practices.
        • TASK: Write those best practices down, first as instructions and context for agents,
        • TASK: then built into a reasoning system
          • (OK those are pretty different tasks)
        • TASK: Automate how the ontology grows, with a subject-matter expert in the loop who isn’t an ontologist.
          • Slightly contradictory, automate and human-in-the-loop, but I think I know what you want
          • Some UI work here, also will need a domain expert
          • TASK (prerequiesite) – scenarios for "growth", there are a lot of possibilities and it depends on state and scale of current ontology
        • TASK Possibly add critic or adversary agents that attack the ontology and suggest improvements.
          • sounds like part of prior task, that's ok.
          • any prior art for that
            • Ask Claude
              • Yes, there's solid prior art across two distinct lineages:

              • Prior Art: Critic/Adversary Agents for Ontology Improvement

              • 1. Classic Ontology Debugging (pre-LLM)

              • This is well-established territory:
              • OntoDebug (Protégé plugin):
              • debugging tools that localize faults in ontologies by finding explanations of discrepancies between the actual ontology and the intended ontology.
              • It uses an interactive loop where
              • the user iteratively states queries in the form of wrong and correct axioms, and OntoDebug automatically recomputes its diagnoses and suggests new queries.
              • Hidden error detection via contextual knowledge:
              • an ontology can be coherent and consistent internally, but if evaluated with respect to other knowledge bases, conflicts may arise.
              • Work exists on using external ontologies like DBpedia as an adversarial reference to surface contradictions that internal reasoning misses.
              • Provenance-based debugging of evolving ontologies:
              • allows answering questions such as "When has this inconsistency been introduced and who is responsible for this change?"
              • — directly relevant to tracking ontology growth over time.

              • 2. LLM Adversarial/Critic Agent Patterns (recent)

              • This is the more directly applicable prior art for an agent-based system:
              • Multi-agent critique is the established pattern:
              • multi-agent critique implements collaborative validation through multiple LLM instances assigned distinct evaluative perspectives, where specialized critic agents independently assess from their respective viewpoints, producing diverse critiques that collectively provide more comprehensive error detection.
              • Adversarial agents are distinct from validators:
              • an adversarial agent is a second AI agent whose explicit job is to challenge, critique, stress-test, or attempt to break the output of a primary agent — not a validator that checks against a fixed ruleset. It's an active, reasoning critic that thinks about why something might be wrong, not just whether it matches a schema.
              • Specifically for ontologies, there's direct prior art:
              • adversarial critique is considered non-negotiable for LLM-assisted ontology work, because LLMs are sycophantic and will confidently execute changes that harm the ontology.
              • The recommended pattern is to use antagonistic reasoning agents, and surface the debate to a human ontologist.
              • Why generic critique fails:
              • LLMs trained with RLHF exhibit a documented sycophantic bias — when asked "is this design good?", the model tends to agree, accepting the problem framing and optimizing within it without questioning the framing itself.
              • The fix is structured lens criteria: explicit, non-negotiable coverage requirements that force the model to seek failure modes it would otherwise omit.
              • Practical limit:
              • too many critique rounds creates its own problem — after enough rounds of "but what if you're wrong?", an agent can become so hedged and qualified that it's useless. Two to three adversarial rounds is usually the practical sweet spot before diminishing returns set in.

              • Key Takeaway for Emergence

              • The prior art strongly validates this idea. The most useful synthesis is: use structured adversarial lenses (not just "find problems") targeting specific ontology failure modes (naming inconsistency, missing disjointness, over-broad classes, axiom conflicts with external KBs), run 2–3 rounds, and surface the debate — not a resolved verdict — to the human domain expert. That last point directly connects to the human-in-the-loop requirement from the prior task.
            • Great please add references
              • Ask Claude
                • Here are the references, organized by the two main threads of prior art relevant to this task:

                • Prior Art: Critic/Adversary Agents Attacking and Improving Structured Knowledge

                • Thread 1: Classical Ontology Debugging & Repair (Formal Methods)

                • This is the established ontology engineering literature — before LLMs, debugging was a formal/symbolic problem:
                • **Schlobach & Cornet (2003)** — first tableau-based algorithm for ontology debugging. The foundational paper on locating unsatisfiable concepts. Referenced widely as the origin of the field.
                • "Completing and Debugging Ontologies: State of the Art and Challenges" (Lambrix et al., IJCAI 2022 survey) —
                • a key survey formalizing the repairing step as an abduction problem and situating the state of the art in ontology debugging and completion.
                • OntoDebug —
                • one of the few interactive approaches in debugging of ontologies, implementing test-driven ontology debugging.
                • (Schekotihin et al.; Protégé plug-in)
                • RIO: Minimizing User Interaction in Debugging of Knowledge Bases (Rodler et al., 2013) — https://arxiv.org/pdf/1302.2465 — reduces expert burden in interactive ontology debugging via a learning strategy.
                • "Repairing EL Ontologies Using Weakening and Completing" (ESWC 2023) —
                • traditional debugging techniques repair ontologies by removing unwanted axioms but may remove consequences that are correct in the domain; this paper proposes an interactive approach using axiom weakening and completing.
                • Research has also shown that by playing simple interaction games, agents can effectively repair random networks of ontologies.

                • Thread 2: LLMs as Ontology Critics

                • Recent work applying LLMs specifically to ontology evaluation and critique:
                • "Knowledge Engineering With Large Language Models: A Capability Assessment in Evaluating Ontology Property Restrictions" (Tsaneva et al., 2026) —
                • experimental results show that LLMs perform well in syntax checking and inconsistency detection for small ontologies, across four subtasks: detecting inaccurate axiom modeling, classifying mistake types, explaining issues, and generating correct alternatives.
                • ChatGPT-4 verified axioms with 92.2% accuracy, improving to 96.7% with refinement.
                • VSPO: Validating Semantic Pitfalls in Ontology via LLM-Based CQ Generation —
                • the first evaluation framework assessing LLM-based competency question generation not by surface-level similarity, but by the model's ability to validate semantic pitfalls in ontologies.
                • "Large Language Models for Ontology Engineering: A Systematic Literature Review" (Semantic Web Journal) —
                • as Human Evaluators, LLMs demonstrate strong performance in verifying ontology correctness, including bug detection: identifying and reporting errors or inconsistencies.
                • The evaluator role remains underexplored but promising for advancing ontology validation.
                • NeOn-GPT (Semantic Web Journal) —
                • uses OWL reasoners and modeling-pitfall detection tools to iteratively verify and repair ontology axioms, using ROBOT as an explanation engine for logical inconsistency.
                • OaK: Toward Effective and Reliable LLM Agents via Dynamic Ontology —
                • a framework that dynamically constructs and refines task-oriented ontologies for LLM agents, using judge feedback to iteratively refine both the ontology and its knowledge graph.

                • Thread 3: Adversarial/Critic Agent Patterns (General, Applicable to Ontologies)

                • The architectural pattern of "one agent builds, another attacks" has strong prior art in the broader LLM/agent literature:
                • Constitutional AI (Anthropic/Bai et al., 2022) —
                • humans define a set of principles and the AI uses these principles to critique and revise its own outputs, through supervised fine-tuning on self-critique examples and reinforcement learning from AI-generated preferences.
                • The canonical reference for rule-grounded self-critique loops.
                • Self-Refine (Madaan et al., 2023) —
                • formalized the self-critique-and-revise pattern, building on Constitutional AI's demonstration that models can evaluate outputs against written principles.
                • Key caveat:
                • replacing self-generated critique with evaluation from a separately trained critic enhances reasoning, since self-correction degrades when the critique source shares the generator's blind spots.
                • This directly motivates a separate adversary agent rather than self-critique for ontologies.
                • CRITIC (tool-interactive critique) —
                • tool-interactive critiquing consistently outperforms pure self-critique
                • — directly relevant since ontology reasoners (e.g., HermiT, ELK) are deterministic tools that can serve as the external verifier.
                • Generator-Critic Pattern —
                • an adversarial agent is a second AI agent whose explicit job is to challenge, critique, stress-test, or attempt to break the output of a primary agent — not a validator that checks against a fixed ruleset, but an active reasoning critic that thinks about why something might be wrong.
                • **AlphaLab Builder–Critic–Tester loop** —
                • a multi-agent adversarial loop where a Builder constructs a framework, a Critic (a fresh agent with no shared context) audits for bias and errors, and a Tester runs automated tests — the loop terminates when tests pass or a max iteration count is reached, since an LLM instructed to find issues will continue to flag things indefinitely.
                • ARCADE (Adversarial Critique Architecture for Document Evaluation) —
                • a three-stage semantic pipeline using a dedicated critic agent to improve analysis through structured critique.

                • Key Design Insight from the Literature

                • Absent external feedback, LLMs largely cannot self-correct reasoning, and naive self-correction can make answers worse. The field has quietly moved from closed-loop self-critique to human-on-the-loop verified refinement.
                • This is exactly the architecture being proposed here — the adversary agent needs an external ground truth (the ontology reasoner + domain expert) to be effective, not just another LLM talking to itself.
        • TASK let customers and system-integrator partners extend the ontology themselves, so they can keep trade secrets private.
          • Sounds a lot harder, just in practical terms. Also I don't know if ontologies should be trade secrets?
        • TASK Talk-to-data: Their English-to-SQL system is a slow, non-deterministic multi-agent pipeline (interpret → ground → plan → generate → validate). They want it replaced with fast, deterministic SQL generation driven by an ontology of database metadata and domain meaning.
        • TASK Specs and verification: How to represent specs for complex programs so code can be generated and checked, using Dafny where the spec is complete enough and logic to find gaps between LLM-written code and incomplete specs. Paul wasn’t sure this fits your background.
          • Probably doesn't, don't know jack shit about Dafny. Actually give me the basics
            • Ask Claude
              • Here's what Dafny is about:
              • Dafny: The Basics
              • What it is
              • Dafny is a verification-aware programming language with built-in support for specifications and a static program verifier.
              • It was originally developed at Microsoft Research and is now actively supported by Amazon's Automated Reasoning group.
              • **Core idea: Code + Spec together**
              • The user writes executable code together with annotations, and Dafny translates the annotated program into verification conditions that are discharged by automated reasoning.
              • The key annotation types are:
              • requires — preconditions (what must be true when a function is called)
              • ensures — postconditions (what the function guarantees on return)
              • Loop invariants — assertions that hold before and after every loop iteration
              • Termination metrics, frame conditions, ghost state
              • How verification actually works
              • Dafny translates code and specs into an intermediate representation (Boogie), computes the weakest precondition wp(s,Q), generates a verification condition of the form P ⟹ wp(s,Q), encodes it into First-Order Logic, and dispatches it to the SMT solver Z3. If the solver determines the negation is unsatisfiable, the program is verified.
              • Practically: code that is not verifiable will not compile.
              • A concrete example
              • A method computing 1+⋯+n can be annotated with ensures s == n * (n + 1) / 2, and the loop invariant states the closed form for the partial sum after each iteration, giving the verifier the inductive fact needed to establish the final result.
              • What it can prove
              • Dafny's primary strength lies in its ability to verify program correctness at compile time, ensuring the absence of common runtime errors such as null dereferences, array out-of-bounds access, or division by zero.
              • Beyond that, Dafny offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.
              • It's a real programming language too
              • Dafny programs can be compiled into C#, Java, JavaScript, Go, and Python.
              • So it's not just a proof assistant — you can ship the code.
              • Real-world use
              • AWS rewrote and verified its policy authorization engine in Dafny, which is invoked 1 billion times per second.
              • Microsoft used Dafny to formally verify security libraries and kernels; ConsenSys applied it for Ethereum Virtual Machine verification.
              • Relevance to the Emergence task: The task is about representing specs for complex programs so that generated code can be checked against them. Dafny is the natural fit when specs are complete — you write requires/ensures clauses and the verifier either passes or gives you a counterexample. The harder problem they're pointing at is what to do when specs are incomplete (which is the typical LLM-generated-code scenario) — using logic to find gaps between what the code does and what the underspecified intent probably was. That gap-finding piece is less standard Dafny and more of a research problem. Paul's instinct that it's outside your wheelhouse is probably right for the gap-finding side; the core Dafny mechanics are learnable but have a steep annotation burden.
              • How's it compare with Lean
                • Ask Claude
                  • Here's a clean comparison:

                  • Dafny vs. Lean

                  • Fundamental orientation
                  • Lean is designed first and foremost to formalize mathematics. While Dafny is a programming language that uses a prover, Lean is a theorem prover, pure and simple.
                  • More concretely: proof languages fall into categories — dedicated theorem provers like Lean and Agda, and programming languages designed to be verified, like Dafny and F*.
                  • How verification works under the hood
                  • Dafny: outsources to Z3 (SMT solver). You write annotations, the solver either discharges them or not. Mostly automatic.
                  • Lean: relies on a minimal logical kernel as its sole verification authority, so even when an LLM produces unpredictable or creative proof attempts, correctness is guaranteed by a small, well-audited checker rather than a complex solver stack.
                  • The trust tradeoff
                  • Dafny's high automation comes at the cost of a large trusted computing base (TCB). Correctness relies on the soundness of the SMT solver (e.g., Z3), a massive software system with a known history of bugs. In contrast, Lean is founded on a small, trusted kernel. While currently less automated, Lean offers a significantly higher standard of assurance. As models improve, they have the potential to bring this "kernel-level trust" to software verification, a capability that SMT-based systems structurally cannot provide.
                  • Ease of use / automation
                  • Dafny wins on automation for typical program verification tasks.
                  • Dafny solves more problems in direct comparison, while Lean's grind tactic still covers some problems Dafny misses — for example, IMO 1959 Problem 1 requires a substantial proof in Lean but verifies with an empty proof in Dafny.
                  • This does not make Dafny a replacement for Lean-style formal mathematics, whose expressiveness and libraries are substantially richer.
                  • Practical deployability
                  • Lean's only production compilation target is C. Dafny compiles verified code to Python, Go, JavaScript, Java, and C#. For "write new verified logic and ship it to a Django or Express codebase," Dafny is the more practical choice today.
                  • **LLM tooling (relevant for the Emergence context)**
                  • Lean exposes the entire proof construction process to the LLM agent. Such an interactive loop is particularly suitable for iterative, model-driven verification.
                  • That said, models trained primarily on general code show limited Dafny-specific knowledge, often confusing Dafny syntax with Lean — so LLMs currently have better coverage of Lean due to its larger community and math benchmark ecosystem.
                  • Bottom line for Emergence's use case: Dafny is the more practical fit for the stated task (spec + verify generated code, ship it). Lean is the right choice if you need the highest assurance guarantees or are doing deep mathematical reasoning — not the typical software verification scenario they're describing.