From 2f6c1609cc8fb481ae17f28a4c7f037b4a96ed59 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 13:30:30 -0700 Subject: [PATCH 1/9] chore: scaffold principled-agent-architectures-review folder --- .../principled-agent-architectures-review/.gitignore | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/.gitignore diff --git a/papers/ai_and_agents/principled-agent-architectures-review/.gitignore b/papers/ai_and_agents/principled-agent-architectures-review/.gitignore new file mode 100644 index 0000000..125c517 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/.gitignore @@ -0,0 +1,6 @@ +generated/ +*.pdf +*.aux +*.log +*.out +*.toc From 19c509b143bdc253fe4e70417517345abe840032 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 13:36:40 -0700 Subject: [PATCH 2/9] feat: add Dublin Core + Schema.org metadata block --- .../src/00-metadata.xml | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/src/00-metadata.xml diff --git a/papers/ai_and_agents/principled-agent-architectures-review/src/00-metadata.xml b/papers/ai_and_agents/principled-agent-architectures-review/src/00-metadata.xml new file mode 100644 index 0000000..9e1a1e5 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/src/00-metadata.xml @@ -0,0 +1,46 @@ + + + + + Principled Agent Architectures: A Neuro-Symbolic Blueprint Beyond Large Language Models — Critical Review and Repository Audit + metavacua research session (Claude Sonnet 4.6, 2026-06-23) + Neuro-Symbolic AI; Agent Architecture; Curry-Howard Correspondence; Formal Verification; Large Language Models; Program Synthesis + A critical review of the NSAM paper with adversarial verification of 6 key empirical and novelty claims, sourced from 23 primary and secondary papers, plus a relevance audit of 7 GitHub repositories in the metavacua project portfolio. + metavacua/Theory (GitHub) + 2026-06-23 + ScholarlyArticle + application/xml + en + AGPL-3.0-or-later + Deep research workflow (105 agents, 1307 tool uses, 2,247,194 subagent tokens) + + + From acef4e8f24acb29a2a971ed14d84af4bd08fcf0f Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:45:08 -0700 Subject: [PATCH 3/9] feat: encode original NSAM paper as DocBook 5.2 XML --- .../src/01-original-paper.xml | 208 ++++++++++++++++++ 1 file changed, 208 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/src/01-original-paper.xml diff --git a/papers/ai_and_agents/principled-agent-architectures-review/src/01-original-paper.xml b/papers/ai_and_agents/principled-agent-architectures-review/src/01-original-paper.xml new file mode 100644 index 0000000..e8f0aeb --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/src/01-original-paper.xml @@ -0,0 +1,208 @@ + +
+ + + Principled Agent Architectures: A Neuro-Symbolic Blueprint Beyond Large Language Models + + This document is a faithful DocBook 5.2 encoding of the reviewed paper proposing the Neuro-Symbolic Abstract Machine (NSAM) architecture. All text is reproduced verbatim from the source paper. The paper argues for a principled, hybrid agent design synthesizing efficient neural networks with symbolic reasoning grounded in the Curry-Howard correspondence. + + + +
+ Introduction: The Limitations of the Monolithic LLM Brain + + The field of artificial intelligence is currently dominated by an agent architecture paradigm of remarkable simplicity and power: the "brain, memory, tools" model, where the "brain" is a monolithic Large Language Model (LLM). This approach, leveraging the vast, pre-trained knowledge and impressive fluency of models like GPT-4, has catalyzed an explosion of applications in conversational AI, content generation, and task automation. By treating the LLM as a central reasoning engine that can be prompted to access memories and utilize external tools, developers have rapidly created agents with a wide range of apparent capabilities. However, this rapid progress has come at the cost of architectural and theoretical rigor, creating a paradigm whose foundational weaknesses represent a significant barrier to the development of truly robust, reliable, and intelligent agents for high-stakes, safety-critical applications. The very nature of these LLM-centric systems stands in opposition to decades of progress in formal methods and high-assurance software engineering, which were developed precisely to provide mathematical guarantees of correctness in domains where failure is not an option. +
+ +
+ The Current Paradigm: Agents as LLM-Wrapper Systems + + The prevalent agent architecture can be characterized as an LLM-wrapper system. In this model, the agent's cognitive functions—perception, planning, and reasoning—are outsourced to an API call made to a massive, remotely hosted neural network. The agent's "thought process" is often a "chain-of-thought" prompt, where the LLM generates natural language text that rationalizes a sequence of actions, including calls to external tools like calculators or search engines. This architecture has been undeniably successful in tasks that benefit from the LLM's strengths: its encyclopedic knowledge base, its ability to process and generate human language, and its capacity to perform zero-shot or few-shot generalization to new problems. For applications where fluency is paramount and strict logical consistency is secondary, this paradigm has proven to be a powerful and accessible tool for building seemingly intelligent systems. +
+ +
+ Foundational Critiques of the LLM-centric Brain + + Despite its successes, the LLM-as-brain paradigm is built on a foundation that is fundamentally unsuited for applications demanding reliability, verifiability, and trustworthiness. Its weaknesses are not incidental flaws to be engineered away but are inherent to the nature of LLMs themselves. + +
+ Opacity and Lack of Interpretability + LLMs are quintessential "black boxes." Their decisions emerge from the complex interplay of billions or trillions of numerical weights, a process that is opaque even to their creators. While techniques exist to generate post-hoc explanations, such as the chain-of-thought, these explanations are themselves generated text; they are rationalizations, not a faithful trace of the underlying computational process, and are equally susceptible to hallucination. This lack of true interpretability is a non-starter in critical domains like medicine, finance, and autonomous systems, where the ability to audit and understand a decision-making process is a legal and ethical requirement. +
+ +
+ Logical Inconsistency and Hallucination + A core misunderstanding of LLMs is to mistake their linguistic fluency for logical competence. An LLM is a probabilistic token predictor, not a formal logic engine. Its objective is to generate the most statistically likely sequence of words, not to verify the truth or logical soundness of its statements. This leads to their well-documented struggles with complex logical problems, where they can produce articulate, confident, yet entirely incorrect reasoning chains. Factual hallucination, where the model invents plausible-sounding but false information, is not a bug to be fixed but an intrinsic feature of a system that generates content based on statistical patterns rather than grounded knowledge and deductive inference. +
+ +
+ Computational and Data Inefficiency + The performance of modern LLMs is predicated on "scaling laws," an empirical observation that bigger models trained on more data perform better. This has led to an arms race in model size, with parameter counts reaching into the trillions. The computational resources required to train and even run inference on these models are immense, making them economically and environmentally costly and centralizing their development in the hands of a few large corporations. This paradigm is fundamentally at odds with the goal of creating lightweight, efficient agents that can operate in resource-constrained environments. +
+ +
+ The Problem of Verifiability + Perhaps the most profound limitation is the impossibility of formal verification. Formal methods, the cornerstone of high-assurance software, rely on the ability to create a mathematical specification of a system's behavior and then prove that the system's implementation adheres to that specification under all possible inputs. LLMs, trained on the chaotic entirety of the public internet, lack any such formal specification. It is impossible to mathematically guarantee that an LLM will not produce a harmful, biased, or dangerously incorrect output. As Edsger Dijkstra famously noted, "testing shows the presence, not the absence of bugs". For a system as vast and non-deterministic as an LLM, testing can only ever probe a vanishingly small fraction of its potential behaviors, leaving its performance in novel situations a matter of hope rather than mathematical certainty. Building an agent's core reasoning faculty on such a foundation is a philosophical and engineering regression from the principles of safety-critical system design. +
+
+ +
+ Thesis: The Imperative for a Principled, Hybrid Architecture + + The limitations of the monolithic LLM brain necessitate a paradigm shift. This report posits that a superior agent architecture can be engineered by moving beyond a purely statistical approach and embracing a principled, hybrid design. The central thesis is that a more robust, lightweight, and trustworthy agent brain can be constructed by synthesizing the powerful pattern-recognition capabilities of modern, efficient neural networks with the rigorous, verifiable, and interpretable structure of symbolic reasoning systems. + + This approach reframes the agent's mind not as a single, monolithic neural network but as a dual-process cognitive architecture. It leverages neural components to perform "System 1" tasks—the fast, intuitive, and perceptual processes of making sense of unstructured real-world data. It then couples these with a symbolic core that performs "System 2" tasks—the slow, deliberate, and logical reasoning required for planning, deduction, and verifiable decision-making. + + To achieve this, this report will draw upon three key theoretical foundations: Neuro-Symbolic AI (NSAI), which provides the overarching framework for integrating neural and symbolic methods; Formal Language Theory, which offers the tools to define a precise, unambiguous internal language for the agent's thoughts and plans; and the Curry-Howard Correspondence, which establishes a profound link between logic and computation, providing the ultimate principled foundation for a verifiable reasoning engine. + + By weaving these threads together, this report will propose a concrete architectural blueprint for an agent brain that is not only more lightweight and efficient than its LLM-based counterparts but is also principled, interpretable, and verifiable by design. +
+ +
+ Foundational Paradigms for a New Cognitive Architecture + + To construct an agent brain that transcends the limitations of monolithic LLMs, it is necessary to build upon a more rigorous theoretical foundation. The proposed architecture is not an ad-hoc combination of components but a principled synthesis of three powerful paradigms from computer science, logic, and cognitive science. These paradigms—Neuro-Symbolic Integration, Formal Language Theory, and the Curry-Howard Correspondence—collectively provide the theoretical underpinnings for a system that can learn from the world, reason about it with logical precision, and produce verifiable plans of action. + +
+ Neuro-Symbolic Integration: The Dual-Process Brain + + Neuro-Symbolic AI (NSAI) represents a "third wave" of AI that seeks to unify two historically opposed traditions: the connectionist approach of neural networks and the logic-based approach of symbolic AI. The core principle of NSAI is to create hybrid systems that merge the respective strengths of each paradigm—the ability of neural networks to learn complex patterns from vast, unstructured, and noisy data, and the ability of symbolic systems to perform explicit, interpretable reasoning using structured knowledge and rules—to overcome their individual weaknesses. Neural networks are powerful learners but are opaque and struggle with explicit reasoning, while symbolic systems are interpretable and logical but are often brittle and require manually curated knowledge bases. + + This integration finds a powerful cognitive analogue in Daniel Kahneman's dual-process theory of human reasoning. In this view, cognition arises from the interplay of two distinct systems: System 1, which operates automatically and quickly, with little or no effort and no sense of voluntary control — it is intuitive, associative, and excels at pattern recognition, aligning directly with the capabilities of deep neural networks; and System 2, which allocates attention to the effortful mental activities that demand it, including complex computations — it is slow, deliberate, and capable of logical, step-by-step reasoning, corresponding to the function of symbolic AI systems. + + An NSAI architecture, therefore, can be conceptualized as an engineered dual-process brain. The neural components serve as the agent's System 1, responsible for perception, feature extraction, and intuitive heuristics. The symbolic components serve as its System 2, responsible for structured planning, logical inference, and explicit decision-making. This synthesis promises significant benefits over purely neural or symbolic approaches, including enhanced generalization from less data, greater robustness to novel situations, and, most critically for a principled design, inherent interpretability and explainability. The symbolic component provides a traceable, logical scaffold that makes the agent's reasoning process transparent and auditable, addressing the fundamental opacity of the LLM-as-brain model. +
+ +
+ Formal Language Theory: The Grammar of Thought + + A central failing of agents that "think" in natural language, such as those using chain-of-thought prompting, is that their internal representational medium is fundamentally flawed for computation. Natural languages like English are inherently ambiguous, context-dependent, and over-expressive, making them unsuitable for the kind of precise, verifiable reasoning required for a principled agent. A single sentence can have multiple interpretations, a problem that can lead to catastrophic failures in a system that needs to act deterministically. + + Formal language theory, originating with the work of Noam Chomsky, provides the solution. A formal language is a set of strings constructed from a finite alphabet, where the validity of any given string is determined by a set of precise rules known as a grammar. This framework allows for the creation of languages that are completely unambiguous; every valid statement has exactly one meaning. The theory further defines automata—abstract machines like finite state machines or Turing machines—that can recognize, parse, or generate strings in a given formal language. + + The architectural implication for a principled agent is profound: its internal representations of the world, its goals, and its plans must be expressed in a formal language, not a natural one. The agent's "thought process" must be a sequence of operations on these formal structures, governed by a strict grammar. This ensures that every internal state of the agent is well-defined, machine-parseable, and verifiable. This stands in stark contrast to the unconstrained, probabilistic generation of natural language text that constitutes the "reasoning" of an LLM, providing a solid foundation for building a system whose internal logic can be formally analyzed and trusted. +
+ +
+ The Curry-Howard Correspondence: Computation as Logical Deduction + + While formal language theory provides the syntax for an agent's internal thoughts, the Curry-Howard correspondence provides the semantics for its reasoning process. This principle, also known as the "proofs-as-programs" isomorphism, reveals a deep and direct structural equivalence between formal logic and computer programs. It is not merely an analogy but a formal mapping that has become a cornerstone of programming language theory and proof theory. + + The correspondence establishes an isomorphism between propositions in a system of logic (specifically, intuitionistic or constructive logic) and types in a model of computation (specifically, a typed lambda calculus). The key equivalences are: a logical proposition corresponds to a type; a proof of that proposition corresponds to a program (or a term) that has that type; and the process of proof simplification corresponds to the process of program evaluation (computation). The mapping extends across fundamental constructs: Implication (A→B) corresponds to a function type (A→B); Conjunction (A∧B) corresponds to a product type (a tuple or struct); Disjunction (A∨B) corresponds to a sum type (a tagged union or variant); Universal Quantification (∀x.P(x)) corresponds to a dependent product type (a dependent function or Pi-type); Existential Quantification (∃x.P(x)) corresponds to a dependent sum type (a dependent pair or Sigma-type). + + The architectural consequence of this correspondence is transformative. It provides the ultimate principled foundation for an agent's reasoning engine. If an agent's goal is framed as a proposition to be proven (a type to be inhabited) and its plan is framed as a proof (a program), then the very act of constructing a valid plan becomes equivalent to constructing a formal, mathematical proof of the goal's achievability. The resulting plan is not just a sequence of steps that seems plausible; it is a program that is, by its very construction, logically sound and guaranteed to satisfy its type—the goal. This elevates planning from a heuristic process to a form of logical deduction. + + When synthesized, these three paradigms reveal a clear path forward, but also a critical architectural challenge. The Curry-Howard correspondence provides a mechanism for provably correct reasoning within a formal system. Formal language theory provides the tools to define that system unambiguously. However, an agent must interact with the messy, ambiguous real world. This is where neuro-symbolic integration becomes essential. The NSAI framework dictates that a neural component must act as the bridge, performing the perceptual task of translating raw, unstructured sensory data into the clean, formal propositions that the logical core can operate on. This translation step—the act of semantic parsing—is a pattern recognition task, not a logical deduction. It is inherently probabilistic and fallible. Consequently, the entire system's correctness is bottlenecked by the reliability of this initial neuro-to-symbolic translation. While the agent's plan can be proven to be a correct deduction from its beliefs, it is not possible to formally prove that its beliefs are a correct representation of reality. This understanding dictates that the architectural design must place significant emphasis on constraining, validating, and potentially iterating upon this critical perceptual interface. +
+
+ +
+ A Survey of Architectural Components and Integration Patterns + + Transitioning from theoretical foundations to practical design requires a comprehensive understanding of the available building blocks and the established patterns for combining them. The field of Neuro-Symbolic AI is not monolithic; it encompasses a wide spectrum of integration strategies, each with distinct trade-offs in terms of coupling, differentiability, and information flow. This section provides a systematic survey of these architectural patterns, catalogs the lightweight neural components suitable for the perceptual "System 1," and explores the differentiable symbolic reasoners that can bridge the gap between neural learning and logical inference. + +
+ A Taxonomy of Neuro-Symbolic Architectures + + A clear vocabulary is essential for discussing and designing hybrid systems. The taxonomy developed by Henry Kautz provides a widely adopted and effective framework for classifying the primary modes of neuro-symbolic integration. This taxonomy categorizes architectures based on how the neural and symbolic components interact and which component takes the lead role. + + The primary architecture types are: (1) Symbolic→Neural→Symbolic — a sequential pipeline where symbolic input is processed by a neural network to produce a symbolic output, with the neural network acting as a complex, learnable transformation function (canonical example: LLMs where text tokens are encoded, processed, and decoded); (2) Symbolic[Neural] — a symbolic system invokes a neural component as a subroutine to perform a specific, often perceptual, sub-task (canonical example: AlphaGo, where the symbolic Monte Carlo Tree Search algorithm calls a neural network to evaluate board positions); (3) Neural[Symbolic] — a neural system calls an external symbolic reasoning engine as a tool to perform precise computations or logical inferences (canonical example: an LLM using a calculator plugin or querying WolframAlpha); (4) Neural|Symbolic — neural and symbolic components operate as interconnected coroutines, iteratively collaborating to solve a problem through a feedback loop; (5) Neural:Symbolic→Neural — a symbolic system generates or labels a large dataset used to train a neural network (canonical example: using a symbolic mathematics system like Macsyma to create solved equations to train a neural network); (6) NeuralSymbolic (Compiled) — symbolic rules are compiled directly into the architecture of the neural network, often by constraining its structure or loss function (canonical examples: Logic Tensor Networks and Logical Neural Networks). + + This taxonomy reveals a fundamental duality in integration philosophy. In architectures like Neural[Symbolic], the symbolic component is treated as an external, opaque tool. In contrast, in compiled architectures like NeuralSymbolic, logic becomes the differentiable substrate of the network itself. The design of a new agent brain must consciously choose where on this spectrum it intends to operate. +
+ +
+ Lightweight Neural Modules (The "Neuro" Component) + + A core requirement for the proposed agent brain is that it be "lightweight," avoiding the immense computational and memory footprint of state-of-the-art LLMs. The neural components in our proposed architecture are not tasked with being general-purpose reasoning engines; instead, they serve specialized roles as perceptual processors and heuristic guides. This allows for the use of a new generation of highly efficient neural architectures: + + State Space Models (SSMs): Models like Mamba have emerged as powerful alternatives, replacing the quadratic-complexity self-attention mechanism of Transformers with a linear-time state space model. Mamba exhibits linear scaling in sequence length and can handle contexts of over 100,000 tokens on a single GPU with significantly reduced memory usage. + + Hybrid Architectures: To balance efficiency with capability, hybrid models have been developed. Jamba, for instance, combines Mamba layers with traditional Transformer blocks, using a mixture-of-experts (MoE) approach. This design leverages the efficiency of SSMs for the bulk of sequence processing while retaining the power of attention for higher-level reasoning, achieving a 3x throughput improvement over comparable models while handling massive contexts. + + Attention-Free and Linear Attention Models: Another line of research has focused on replacing or approximating the attention mechanism. FNet discards attention entirely in favor of Fourier Transforms, achieving an 80% speedup in training on GPUs with a minimal memory footprint by replacing learned parameters with a parameter-free mathematical operation. cosFormer uses a cosine-based reweighting mechanism to achieve linear complexity, reducing memory usage by 10x while retaining 92-97% of a traditional Transformer's accuracy. Other models like Linformer and Performer use different approximation techniques to achieve linear or near-linear complexity with minimal performance degradation. + + The existence of these diverse, efficient architectures confirms that the "neuro" part of a neuro-symbolic agent does not need to be a monolithic, multi-billion parameter LLM. +
+ +
+ Differentiable Symbolic Reasoners (The "Symbolic" Bridge) + + A key challenge in neuro-symbolic AI is bridging the gap between the continuous, gradient-based world of neural networks and the discrete, logical world of symbolic reasoning. A new class of "differentiable symbolic reasoners" addresses this: + + Logic Tensor Networks (LTNs): LTNs provide a framework for translating First-Order Logic (FOL) into a differentiable computational graph. In this paradigm, logical constants are represented as tensors of features, and predicates are represented as neural networks that map these tensors to a truth value in the range [0,1]. Logical connectives are implemented using fuzzy logic operators, specifically t-norms, which are differentiable functions. This allows an entire knowledge base of logical axioms to be used as a loss function. + + Logical Neural Networks (LNNs): LNNs offer a different but related approach where the network architecture itself mirrors the structure of a logical formula. Each neuron has a direct, interpretable meaning as a component of a formula in a weighted real-valued logic. Inference is omnidirectional, corresponding to logical deduction, and learning is driven by a novel loss function that directly minimizes logical contradiction within the system. A key feature of LNNs is their ability to handle incomplete knowledge by maintaining upper and lower bounds on truth values, naturally supporting the open-world assumption. + + Other Differentiable Frameworks: The field includes a variety of other approaches. Differentiable Inductive Logic Programming (∂ILP) introduces soft unification mechanisms to allow for gradient-based learning of logical rules from data. Neural Theorem Provers (NTPs) model the recursive process of proof construction in a continuous vector space. The Scallop framework provides a general-purpose neuro-symbolic programming language based on Datalog that supports efficient, differentiable reasoning. +
+
+ +
+ Blueprint for a Principled, Lightweight Agent Brain + + Synthesizing the foundational paradigms and architectural components surveyed in the preceding sections, this chapter presents a concrete blueprint for a novel agent brain. This architecture is designed from the ground up to be principled, verifiable, and lightweight, directly addressing the core weaknesses of the monolithic LLM paradigm. The proposed design is a Neuro-Symbolic Abstract Machine (NSAM), a system that operationalizes the Curry-Howard correspondence by structuring the agent's reasoning process as the synthesis and execution of a program in a typed functional language. + +
+ The Core Architecture: A Neuro-Symbolic Abstract Machine (NSAM) + + The cognitive core of the proposed agent is an NSAM, which can be understood as a neural network that is structurally equivalent to a programming language interpreter. This design choice moves beyond mere analogy and directly implements the "proofs-as-programs" isomorphism as the agent's central reasoning mechanism. + + In this architecture: Goal Representation as Types — a goal provided to the agent is translated into a formal type (e.g., the command "stack the red block on the blue block" is represented as the type On(RedBlock, BlueBlock)); Planning as Proof Search and Program Synthesis — the act of planning is reframed as a search for a program (a proof term) that inhabits the goal type, constructed from primitive functions corresponding to the agent's basic actions; Verifiability by Construction — the type system provides an intrinsic verification mechanism, so if the agent successfully constructs a program p that has the type T_goal, it is a mathematical certainty that the program p, when executed, will satisfy the properties described by T_goal. + + This architectural choice directly leverages the Curry-Howard correspondence as a blueprint for a reasoning engine. It replaces the ill-defined, heuristic process of "agent reasoning" with the well-defined, verifiable computer science problem of automated theorem proving and program synthesis in a constructive logic. +
+ +
+ Integrating Neural Perception (System 1) + + While the core of the NSAM is a formal, symbolic system, the agent must be able to perceive and act in the unstructured real world. This interface is managed by specialized, lightweight neural modules operating in a cooperative Neural|Symbolic pattern. Two key neural modules are proposed: + + Semantic Parser Module: A lightweight neural network trained for the specific task of semantic parsing. Its function is to take raw, unstructured sensory input (e.g., a camera image, a user's natural language command) and translate it into a set of discrete, formal symbolic propositions that can be ingested by the logical core. For example, upon viewing a scene, the parser might output: Is(b1, Block), Color(b1, Red), Is(b2, Block), Color(b2, Blue), OnTable(b1), OnTable(b2), Clear(b1), Clear(b2). + + Heuristic Guidance Module: A second neural module that acts as a learned heuristic to guide the proof search of the logical core. Trained via reinforcement learning or imitation learning, this module can predict the most promising proof steps or program structures to explore next, given the current goal and state. This combines the intuitive pattern recognition of a neural network with the formal rigor of the symbolic search, dramatically pruning the search space without sacrificing logical soundness. +
+ +
+ The Reasoning Process as Verifiable Program Synthesis + + The agent's cognitive cycle follows a clear, verifiable flow: (1) Goal Specification — a high-level goal is parsed into a formal type, T_goal; (2) Perception and Context Formulation — the Semantic Parser generates formal propositions Γ representing the current known facts; (3) Proof Construction (Planning) — the logical interpreter attempts to construct a program term p that can be proven to have type T_goal given axioms Γ, formally denoted Γ ⊢ p : T_goal, guided by the Heuristic Guidance Module; (4) Intrinsic Verification — the type system enforces correctness at each step; the final type-checking of p serves as formal verification; (5) Execution — the verified program p is executed by translating it into commands for the agent's actuators. +
+ +
+ Formal Language as the Agent's Internal Language (The "Grammar of Thought") + + The agent's internal formal language contains: Types (logical predicates describing states): On(Block, Block), Clear(Block), Holding(Block), OnTable(Block); Terms (constants for objects and functions for actions); Action Functions with formal types encoding preconditions and effects: + pickup: ∀x. (OnTable(x) ∧ Clear(x) ∧ HandEmpty) → Holding(x) + stack: ∀x, y. (Holding(x) ∧ Clear(y)) → On(x, y) + Rules of Inference that specify how new truths can be derived, encoding the "physics" of the agent's environment. +
+
+ +
+ Comparative Analysis and Implementation Pathways + + The fundamental differences in the underlying principles of LLM-based agents and the proposed NSAM architecture lead to starkly contrasting capabilities. On logical inference: LLM-based agents use probabilistic and correlational reasoning, prone to logical fallacies and factual hallucination, while NSAM uses deterministic and deductive inference equivalent to formal proof construction, guaranteeing logical consistency. On interpretability: LLM agents are opaque black boxes where chain-of-thought is a post-hoc rationalization, while NSAM is a transparent glass box where the outputted program/proof is a complete, verifiable, and auditable trace. On computational efficiency: LLM agents require massive parameter counts and computationally expensive attention mechanisms, while NSAM is lightweight with a simple logical engine and small specialized neural modules. On data efficiency: LLM agents require massive internet-scale datasets, while NSAM is dramatically more data-efficient because logical structure provides a strong inductive bias and domain knowledge is encoded explicitly as rules. On formal verifiability: LLM agents cannot be formally verified, while the NSAM core reasoning engine is formally verifiable using formal methods to prove safety and correctness properties. + + The Logic-LM framework demonstrated that offloading reasoning to a dedicated symbolic solver improves performance by an average of 39.2% over standard LLM prompting. The NSAM internalizes this principle, making sound logical deduction its native mode of operation. + + Building a prototype of the NSAM agent is a feasible engineering task. A potential implementation would leverage: PyReason for the symbolic backbone (Python-based framework supporting generalized annotated logic, designed for reasoning over graph-based data); Scallop for an end-to-end differentiable alternative (differentiable programming language based on Datalog integrated with PyTorch); LNN library from IBM for the Heuristic Guidance Module; LTNtorch library for training the Semantic Parser Module. +
+ +
+ Conclusion and Future Directions + + The core of the NSAM proposal is the operationalization of the Curry-Howard correspondence, which reframes agent reasoning as a process of verifiable program synthesis. The agent's brain is architected as an interpreter for a typed formal language, where goals are represented as types and plans are well-typed programs. This guarantees that any plan the agent generates is, by construction, logically sound and correct with respect to its perceived state and internal knowledge. + + This symbolic "System 2" reasoning core is integrated with a neural "System 1" perceptual system. Lightweight, efficient neural modules, serving as semantic parsers and heuristic guides, form the bridge to the unstructured real world. This neuro-symbolic synthesis combines the learning and pattern-recognition strengths of neural networks with the rigor and transparency of formal logic, creating a system that is designed to be both lightweight and trustworthy. + + Remaining challenges include: The Semantic Grounding Problem — the entire logical soundness of the NSAM's reasoning rests on the assumption that its neural Semantic Parser correctly translates sensory data into formal axioms; Automated Knowledge Acquisition (Rule Learning) — the agent must be able to acquire new rules and modify existing ones from experience, pointing to the need for Inductive Logic Programming techniques; Handling Uncertainty and Incompleteness — the core logical system is deterministic but the real world is probabilistic, requiring probabilistic or fuzzy logic extensions; Scalability of Proof Search — proof search in a rich logical system can suffer from combinatorial explosion requiring more powerful and efficient neural heuristics. + + The ultimate goal is to move the field of AI from an empirical discipline, where systems are validated by testing, to a formal one, where systems can be accompanied by mathematical proofs of their correctness and safety properties. +
+ +
From 1082180d4c57cb78f69320606b3ee26ba828d094 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:51:50 -0700 Subject: [PATCH 4/9] feat: encode full critical review with 6 verified findings as DocBook 5.2 XML Co-Authored-By: Claude Sonnet 4.6 --- .../src/02-critical-review.xml | 287 ++++++++++++++++++ 1 file changed, 287 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/src/02-critical-review.xml diff --git a/papers/ai_and_agents/principled-agent-architectures-review/src/02-critical-review.xml b/papers/ai_and_agents/principled-agent-architectures-review/src/02-critical-review.xml new file mode 100644 index 0000000..b935b12 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/src/02-critical-review.xml @@ -0,0 +1,287 @@ + +
+ + + + Critical Review: Principled Agent Architectures — Adversarially Verified Findings + +
+ Executive Summary + The NSAM paper's empirical anchors are partially accurate but materially overstated. + The Logic-LM headline figure (39.2%) is a multi-dataset average that the paper applies without + qualification, while the CoT comparison (18.4%) is the more honest measure of incremental gain. + The Mamba linear-scaling and FNet 80%-speedup claims are accurate as stated, but the paper's + "5x throughput" and "92–97% accuracy" figures for these systems did not survive adversarial + verification. The paper's central architectural novelty — applying the Curry-Howard + correspondence to agent planning (goals-as-types, plans-as-proofs) — is substantially + anticipated by prior work, most directly by the Proof-Carrying Plans line (PPDP 2020, PADL 2019) + and more broadly by decades of linear-logic planning research. PyReason's claimed role as an + "exact yet scalable" NSAM core is unsupported by comparative benchmarks against peer systems + (Scallop, DeepProbLog, LTN, LNN), and the broader neurosymbolic community's recent comparative + study excluded PyReason from its empirical tables entirely. The paper is best read as a + well-motivated integration blueprint that overstates both its empirical evidence and its novelty + relative to the literature it does not cite. +
+ +
+ Review Statistics + + + + Search angles5 + Sources fetched23 + Claims extracted109 + Claims verified25 + Confirmed14 + Killed (refuted)11 + After synthesis6 + Agent calls105 + Subagent tokens2,247,194 + + + +
+ +
+ Verified Findings + +
+ Finding 1: Logic-LM 39.2% figure lacks qualification + Claim: Logic-LM's 39.2% improvement figure is a + multi-dataset average and is model-specific; when applied to individual datasets (e.g., FOLIO, + 17.7 pp) or stronger models (GPT-4, ~25% relative), the headline figure is substantially + smaller and not independently reproducible with a single methodology. + Confidence: High + Vote: CONFIRMED WITH CAVEATS — the 39.2% figure is + real but the NSAM paper's presentation strips essential context (model-specificity, averaging + methodology, per-dataset variation). + Evidence: The Logic-LM paper reports 39.2% average + improvement over standard prompting and 18.4% over CoT (EMNLP 2023 Findings, peer-reviewed). + These are averages across five benchmarks (ProofWriter, PrOntoQA, FOLIO, LogicalDeduction, + AR-LSAT). On FOLIO specifically with GPT-3.5 Turbo, Logic-LM scores 62.80% vs. standard + prompting at 45.09% — a 17.71 pp gain, not 39.2%. A 2025 replication study (arXiv:2502.17216) + could not reproduce the exact 39.2% figure, finding 45.23% or 24.98% depending on model and + averaging methodology. Logic-LM++ (ACL 2024 Workshop) achieves only ~5% average improvement + over Logic-LM, with Logic-LM++ actually underperforming Logic-LM on FOLIO/GPT-3.5 (62.25% + vs. 62.80%). The NSAM paper citing 39.2% as a headline without qualification misleads by + applying an average across five datasets as if it were a general improvement figure. + Sources: + EMNLP 2023 Findings, + arXiv:2305.12295, + Logic-LM++ (arXiv:2407.02514) + +
+ +
+ Finding 2: Mamba linear scaling confirmed; 5x throughput refuted + Claim: Mamba's linear scaling in sequence length + (vs. Transformers' quadratic attention) is accurately characterized; however, the "5x + throughput" figure cited in the NSAM paper did not survive adversarial verification. + Confidence: High + Vote: SPLIT — linear scaling claim CONFIRMED; 5x + throughput claim REFUTED. + Evidence: The Mamba paper (Gu & Dao 2023, + arXiv:2312.00752) explicitly claims "linear scaling in sequence length" in its abstract, + achieved via hardware-aware parallel scan during training and recurrent mode during inference. + This is confirmed by the Mamba-2 and Mamba-3 (ICLR 2026) follow-on literature. However, + the NSAM paper's cited "5x higher throughput than Transformers at inference time" claim was + rejected 0-3 in adversarial verification — the primary source reports a different throughput + figure and the 5x number does not appear as stated in the paper. + Sources: + Mamba (arXiv:2312.00752) + +
+ +
+ Finding 3: FNet 80% speedup confirmed; 92–97% accuracy retention contested + Claim: FNet achieves 80% faster per-step training + throughput on GPUs than BERT-base at 512 input lengths; this claim is accurately sourced + from the primary paper. + Confidence: High + Vote: CONFIRMED for speedup; REFUTED for the 92–97% + GLUE accuracy retention figure. + Evidence: The FNet paper (Lee-Thorp et al., NAACL 2022, + arXiv:2105.03824) states "80% faster on GPUs and 70% faster on TPUs at standard 512 input + lengths" in its abstract. The experimental basis is 8 V100 GPUs, batch size 64, comparing + FNet-Base (169 ms/batch) to BERT-Base (305 ms/batch). The NSAM paper's paraphrase of "80% + faster training speeds on GPUs… at standard 512 input lengths" is an accurate restatement. + However, the NSAM paper's accompanying claim that FNet "retains 92–97% of BERT's accuracy + on GLUE benchmarks" was rejected 1-2 in adversarial verification and should not be cited + without qualification. + Sources: + FNet (arXiv:2105.03824) + +
+ +
+ Finding 4: Curry-Howard for agent planning is not novel — anticipated by Proof-Carrying Plans + Claim: The NSAM paper's core novelty claim — + applying the Curry-Howard correspondence to agent planning (goals-as-types, plans-as-proofs) + — is substantially anticipated by prior published work and is not novel as of 2020. + Confidence: High + Vote: CONFIRMED — prior work definitively established + by primary peer-reviewed sources predating the NSAM paper by 4–6 years. + Evidence: The "Proof-Carrying Plans" paper (Hill, + Komendantskaya, Petrick, PPDP 2020, ACM DOI 10.1145/3414080.3414094; earlier version at + PADL 2019) explicitly treats "plans as functions and plan pre- and post-conditions as types," + directly instantiating the Curry-Howard correspondence for AI planning. An Agda implementation + predates even the 2019 publication. Further prior art includes: "Actions You Can Handle: + Dependent Types for AI Plans" (arXiv:2105.11267, 2021); "Planning Problems as Types, Plans + as Programs" (Heriot-Watt thesis). The broader connection between linear logic and AI planning + dates to Masseron, Tollu & Vauzeilles (FSTTCS 1990) and Kanovich & Vauzeilles (2001). + The NSAM paper should cite this body of work and reframe its Curry-Howard contribution as an + integration architecture, not a novel theoretical proposal. + Sources: + PCP (arXiv:2008.04165) + +
+ +
+ Finding 5: Scallop and A-NeSI claims accurate but require qualification + Claim: Scallop's accuracy on eight neurosymbolic + benchmarks matches or exceeds state-of-the-art, and A-NeSI performs approximate probabilistic + neurosymbolic inference in polynomial time without altering the semantics of probabilistic + logics — both claims are accurately sourced, but neither is cited by the NSAM paper with + sufficient methodological context. + Confidence: Medium + Vote: CONFIRMED with caveats — both characterizations + are accurate from primary sources, but the NSAM paper omits material qualifications about + bias, scale limits, and benchmark scope. + Evidence: The Scallop PLDI 2023 paper (Li, Huang, Naik; + ACM DOI 10.1145/3591280) states evaluation on "a suite of eight neurosymbolic applications" + with results "comparable or superior to state-of-the-art models." A-NeSI (arXiv:2212.12393, + NeurIPS 2023) "performs approximate inference in polynomial time without changing the semantics + of probabilistic logics." However, a 2024 hardness paper (arXiv:2406.04472) shows biased + gradient estimators for A-NeSI and that polynomial-time approximation cannot consistently + optimize some formulas. + Sources: + Scallop PLDI 2023, + A-NeSI (arXiv:2212.12393) + +
+ +
+ Finding 6: PyReason features confirmed; "exact yet scalable" claim unsupported + Claim: PyReason implements open-world temporal logic + over generalized annotated logic with explainable inference traces, but its designation as an + "exact yet scalable" NSAM core is unsupported by comparative benchmarks against peer systems. + Confidence: High + Vote: SPLIT — PyReason's stated features CONFIRMED; + "exact yet scalable" relative to peers NOT SUPPORTED by any comparative evidence. + Evidence: The PyReason paper (arXiv:2302.13482, + AAAI-MAKE 2023) confirms open-world temporal logic over generalized annotated logic, temporal + inference over finite periods, and fully explainable inference traces. The 2025 LAT Logic paper + (arXiv:2509.02958) reports "up to three orders of magnitude speedup and up to five orders of + magnitude memory reduction" vs. baselines — but these baselines are high-fidelity + military/game simulators (AFSIM, StarCraft II), not competing logic reasoners (Scallop, + DeepProbLog, LTN, LNN). The most recent independent comparative study of neurosymbolic + frameworks (arXiv:2509.07122, 2025) explicitly excluded PyReason from its empirical tables. + Sources: + PyReason (arXiv:2302.13482), + LAT Logic (arXiv:2509.02958) + +
+
+ +
+ Caveats + + Time Sensitivity: Several quantitative + performance comparisons (Mamba throughput, FNet GLUE accuracy) reflect a fast-moving + literature; hardware-specific numbers are version- and configuration-sensitive. Claims + accurate as of their publication year may be superseded. + Mamba 5x Throughput: The adversarial + rejection (0-3) of the 5x throughput figure means the specific number is unsupported, + but the precise correct figure from the primary source was not established in the verified + claims set — the NSAM paper's error is one of specificity, not direction. + PyReason Scalability: The "up to three + orders of magnitude" speedup (arXiv:2509.02958) was verified at medium confidence (2-1) + as an accurate quote of self-reported best-case results against non-peer-system baselines. + It does not establish comparative superiority over Scallop or DeepProbLog. + Curry-Howard Prior Art: The verified + prior-art landscape focuses on the PCP line (2019–2021); earlier linear-logic-planning + work (1990s) was cited in search results but the exact quotes were not directly verified + from primary papers in this review. + +
+ +
+ Open Questions + + What is the correct throughput ratio of Mamba vs. Transformers at inference + time, and under what sequence-length and hardware conditions — since the 5x figure was + rejected but no confirmed alternative figure was established? + Does any published work directly compare PyReason, Scallop, DeepProbLog, + LTN, and LNN on a shared benchmark suite, and if not, what would such a comparison require + to be methodologically fair given their different expressiveness profiles? + Is the NSAM paper's System 1/System 2 decomposition architecturally novel + relative to existing neuro-symbolic frameworks reviewed in Kautz's taxonomy, or does it + primarily re-label existing integration patterns? + Given that A-NeSI's gradient estimator is provably biased and polynomial-time + approximation cannot consistently optimize some probabilistic logic formulas, what is the + practical impact on NSAM agents that require reliable plan verification? + +
+ +
+ Refuted Claims (11) + + Logic-LM achieves a 39.2% performance improvement over standard LLM prompting + on logical reasoning benchmarks (averaged across five datasets). [Vote 1-2; + source] + The system architecture uses LLMs strictly as a translation layer, not as the + reasoning engine; a deterministic symbolic solver performs the actual inference. [Vote 0-3; + source] + Mamba achieves 5x higher throughput than Transformers at inference time. + [Vote 0-3; source] + FNet retains 92–97% of BERT's accuracy on GLUE benchmarks despite replacing + self-attention entirely with unparameterized Fourier transforms. [Vote 1-2; + source] + Applying the Curry-Howard correspondence to LLM Chain-of-Thought during + decoding is a novel approach. [Vote 0-3; + source] + The Curry-Howard correspondence maps LLM reasoning steps to typed proofs: + propositions become types, CoT traces become typed functional programs. [Vote 0-3; + source] + Planning in a constructive symbolic RL framework becomes theorem proving + under intuitionistic logic, where a state transition is only valid if the implication can + be constructively proven. [Vote 1-2; + source] + Goal-chaining via hierarchical subgoal decomposition can be represented as + recursive proof search Γ₀⊢G₁→Γ₁⊢G₂→…→Γₙ⊢G. [Vote 0-3; + source] + Scallop grounds differentiable reasoning in provenance semirings theory, + not neural network approximations, making its symbolic-to-gradient pathway mathematically + principled and distinct from DeepProbLog. [Vote 0-3; + source] + Scallop is built on Datalog, inheriting Datalog's polynomial-time data + complexity. [Vote 0-3; + source] + A-NeSI is the first end-to-end neurosymbolic method capable of solving + three tasks with exponential combinatorial scaling. [Vote 1-2; + source] + +
+ +
+ Priority Revisions for NSAM Paper + + Add related work section covering Proof-Carrying Plans, type-theoretic AI + planning, and linear logic planning literature (1990–2021). + Reframe the Curry-Howard contribution as architectural integration, not + foundational novelty. + Fix three empirical figures: Logic-LM (add dataset/model context), Mamba + (remove unsourced "5x"), FNet (drop contested 92–97% GLUE retention). + Replace or qualify PyReason with Scallop as the primary implementation + candidate, citing the neurosymbolic survey's exclusion of PyReason from empirical tables. + Add DeepProbLog and A-NeSI to the differentiable reasoner survey, with + the A-NeSI bias caveat. + +
+ +
From 46a1b22017fdee1073358bf2708b1e951dba4c90 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:53:01 -0700 Subject: [PATCH 5/9] feat: encode 7-repo relevance audit as DocBook 5.2 XML Co-Authored-By: Claude Sonnet 4.6 --- .../src/03-repository-audit.xml | 191 ++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/src/03-repository-audit.xml diff --git a/papers/ai_and_agents/principled-agent-architectures-review/src/03-repository-audit.xml b/papers/ai_and_agents/principled-agent-architectures-review/src/03-repository-audit.xml new file mode 100644 index 0000000..d778945 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/src/03-repository-audit.xml @@ -0,0 +1,191 @@ + +
+ + + + Repository Audit: NSAM Paper Relevance Across metavacua Portfolio + +
+ Audit Overview + Seven repositories in the metavacua GitHub portfolio were audited for relevance to the + "Principled Agent Architectures" (NSAM) paper. The audit reveals that the portfolio already + contains substantial implementations of both halves of the NSAM architecture: verumorphism + implements the symbolic reasoning core (HDL calculus, proof/refutation threads, REST API), + and larql-to-sparql implements the neural substrate (transformer weights as queryable DB, + mechanistic interpretability, Wikidata/DBpedia semantic grounding). These are architecturally + complementary exactly as the NSAM paper proposes — they are simply not yet wired together. + + + + + + Repository + Relevance + Primary Action + + + + + metavacua/Theory + HIGH + Primary placement: papers/ai_and_agents/principled-agent-architectures-review/ + + + metavacua/verumorphism + HIGH + IS the NSAM symbolic reasoning component; paper = architectural motivation + + + metavacua/CategoricalReasoner + MEDIUM-HIGH + Cite in docs/dissertation/chapters/curry-howard-extracted.tex as applied validation + + + metavacua/drstrangegoo + MEDIUM-HIGH + Note sequoia_engine (PR#4) as NSAM proof-search oracle candidate + + + metavacua/subclass + MEDIUM-HIGH + Cite Proof<L,R> phantom-type architecture as live Curry-Howard implementation + + + metavacua/larql-to-sparql + MEDIUM + IS the NSAM neural substrate; knowledge/ = semantic grounding layer + + + metavacua/GeodesicLangModel + LOW + "Adjacent Frameworks" footnote in references/README.md only + + + + +
+ +
+ metavacua/Theory — HIGH + The Theory repository contains approximately 60 papers in logic and language, including + subclassical sequent calculi, multiplicative-additive linear logic (MAOLL, OMALL, OMAffine), + a Chomsky hierarchy chapter, and categorical metalanguages. The repository includes a working + AGENTS.md, recently added a cs.LG citation, and uses convert.sh with LaTeXML for TeX-to-HTML + conversion. This repository is the natural primary placement for the NSAM critical review, + within the new papers/ai_and_agents/ subdirectory created for this work. + The linear logic material in Theory directly grounds the resource-sensitivity dimension + of the NSAM's typed planning language, where pickup and stack have dependent types encoding + preconditions as resource consumption. +
+ +
+ metavacua/verumorphism — HIGH + Despite having no public description, verumorphism is a substantial Common Lisp + codebase (SBCL/Quicklisp) implementing "RelWeaver"/"RWSDL" (Relational Weave Structure + and Distributed Logic). Its core components are: + + Concurrent proof/refutation SBCL threads (ProverV0.lisp, RefuterV0.lisp) + HDL (Hypersequent Dependence Logic) calculus with rules con_R/incon_L/dualR/dualL/dependenceR/independenceL + Ternary logic {0,1,i} encoded as complex numbers: proof=positive real, refutation=negative real, non-closure=zero + RelNet knowledge graph layer + REST API (refuter-api.lisp, Hunchentoot) + + The name "verumorphism" = truth-preserving morphism. This IS the symbolic reasoning + component the NSAM describes. The paper serves as architectural motivation for integrating + verumorphism's REST API as the NSAM's logical core, with larql-to-sparql as the neural + perceptual layer feeding formal propositions to it. +
+ +
+ metavacua/CategoricalReasoner — MEDIUM-HIGH + Working title "Catty." Contains dedicated dissertation chapters covering the + Curry-Howard correspondence in categorical formulation (Logic≅Type, proofs-as-programs, + LJ↔STLC, LL↔Linear Types, CCC semantics), linear logic as resource-sensitive substrate + (genesis.tex), and a 2D lattice of subclassical logics organized by structural rules + (logic-lattice-extracted.tex). The system constructs programs from logic and theory pairs. + Recommended action: cite in the curry-howard-extracted.tex chapter as applied validation + of the NSAM blueprint. Do not place this paper here as primary; CategoricalReasoner has no + agent architecture component. +
+ +
+ metavacua/drstrangegoo — MEDIUM-HIGH + Fork of the meta-logic/sequoia project. Implements a parameterized sequent calculus + engine in SML and Python. Concrete calculi implemented include intuitionistic logic + (constructive logic, imp_R rule = lambda abstraction under Curry-Howard) and linear logic + (tensor, lolli, bang, par). The engine auto-checks cut elimination (cut_elim.py/sml), + identity coherence, and rule permutability. YAML-based calculus definition schema. + PR#4 (feat/python-backend-restructure) builds a standalone sequoia_engine library — + this is a candidate NSAM proof-search oracle. The PR should note that sequoia_engine is + intended for NSAM planning proof search, connecting it to verumorphism's HDL calculus. +
+ +
+ metavacua/subclass — MEDIUM-HIGH + The main branch is a stub, but 20 branches and 11 open PRs contain substantial + content candidates for the main branch initialization. Content includes: a scholarly + monograph "The Logic of Logos: Variable Consequence and the Limits of Formalization" + (DocBook XML), a Java library (com.github.metavacua:subclass) implementing Curry-Howard + as phantom types (Proof<L,R>, @Theorem-annotated methods, compile-time + TheoremProcessor), full LK sequent calculus rules as typed Java objects, the Tetragram + structure (Classical⊃{Intuitionistic,Paraconsistent}⊃Common diamond lattice), a Chomsky + hierarchy chapter, and PR#9 VIndexFFNMapping in a ranked graph walk engine. + Branch claude/review-curry-howard-project-NVslf is the most complete. The + Proof<L,R> phantom-type architecture is a live Curry-Howard implementation and a + candidate for extension as an NSAM reference implementation. +
+ +
+ metavacua/larql-to-sparql — MEDIUM + A large Rust workspace. LARQL decompiles transformer model weights into a queryable + "vindex" format addressed via LQL (Lazarus Query Language, SQL-like DSL). The knowledge/ + pipeline processes Wikidata/DBpedia/WordNet triples through feature probing to produce + semantic labels on neural features. + Mechanistic interpretability hooks include: residual capture, ablation, steering, + activation patching, logit lens, and KV-cache surgery. Circuit-type taxonomy classifies + features as Identity/Transform/Projector/Suppressor/Inverter. Sparse FFN inference uses + gate KNN retrieval (K≈10 of 10,240 features per layer). The larql-probe tool + (~/.local/bin/larql-probe v0.3.0) provides a harness for all of these. + This IS the neural substrate of the NSAM. The knowledge/ directory = the semantic + grounding layer. The SPARQL bridge connecting LQL queries to standard triple stores is not + yet implemented (aspirational). The NSAM blueprint motivates closing that gap. +
+ +
+ metavacua/GeodesicLangModel — LOW + Studies LLMs through a geometric lens: Riemannian manifolds, attention as curvature, + geodesic graphs. Contains six hypotheses (H1–H6) and six experiment classes (A–F). Uses + Rosko (arXiv:2511.21296) and Mabrok (arXiv:2603.22301). Has no agent architecture + component and no neuro-symbolic AI connection. The framework is orthogonal to NSAM. + Recommended action: add an "Adjacent Frameworks" footnote in references/README.md + only, noting that GeodesicLangModel studies LLM geometry while the NSAM paper argues for + moving beyond LLMs entirely. +
+ +
+ Cross-Repository Synthesis + The portfolio already implements both halves of the NSAM architecture: + + Symbolic half: verumorphism — HDL calculus, + concurrent proof/refutation threads, REST API for external integration + Neural half: larql-to-sparql — transformer + weights as queryable database, mechanistic interpretability hooks, + Wikidata/DBpedia/WordNet semantic grounding + + These are architecturally complementary exactly as the NSAM paper proposes — the + neural perceptual layer (larql-to-sparql) translates raw data into formal propositions; + the symbolic reasoning layer (verumorphism) operates on those propositions via HDL calculus. + They are simply not yet wired together. The NSAM blueprint motivates building that integration + as the next concrete engineering milestone across both repositories. + Additionally, drstrangegoo's sequoia_engine (PR#4) provides a parameterized sequent + calculus that could serve as the proof-search oracle within verumorphism's HDL reasoning, + while subclass's Proof<L,R> phantom types in Java provide a type-safe reference + implementation of the plans-as-proofs paradigm. +
+ +
From 20f077d8ea5191cc8674901435bb6287669eb7df Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:54:49 -0700 Subject: [PATCH 6/9] feat: add BibTeX bibliography (23 sources) and scratch formula/notes files Co-Authored-By: Claude Sonnet 4.6 --- .../scratch/formulas.md | 102 +++++++++ .../scratch/notes.md | 87 ++++++++ .../src/bibliography.bib | 210 ++++++++++++++++++ 3 files changed, 399 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/scratch/formulas.md create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/scratch/notes.md create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/src/bibliography.bib diff --git a/papers/ai_and_agents/principled-agent-architectures-review/scratch/formulas.md b/papers/ai_and_agents/principled-agent-architectures-review/scratch/formulas.md new file mode 100644 index 0000000..cfd40dc --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/scratch/formulas.md @@ -0,0 +1,102 @@ +# Mathematical Formulas and Tables — NSAM Critical Review + +Scratch notes for LaTeX-complex formulas and reference tables. +These are scratch/working notes; canonical source is the DocBook XML files in src/. + +--- + +## Curry-Howard Correspondence Table + +| Logic | Type Theory | Example | +|-------|-------------|---------| +| Proposition | Type | `IsOn(A,B) : Type` | +| Proof | Term (program) | `p : IsOn(A,B)` | +| A → B (implication) | Function type A → B | `stack : Holding(x) → Clear(y) → On(x,y)` | +| A ∧ B (conjunction) | Product type A × B | `(Holding(x), Clear(y))` | +| A ∨ B (disjunction) | Sum type A + B | `Either` | +| ∀x. P(x) (universal) | Π-type (dependent function) | `Π(x:Block). OnTable(x) → Clear(x) → Holding(x)` | +| ∃x. P(x) (existential) | Σ-type (dependent pair) | `Σ(x:Block). On(RedBlock, x)` | +| Proof simplification | Program evaluation (β-reduction) | Plan execution | + +--- + +## NSAM Typing Judgment + +The core formal notation for NSAM plan synthesis: + +``` +Γ ⊢ p : T_goal +``` + +Where: +- **Γ** = set of known facts (formal propositions from semantic parser) +- **p** = plan program (the proof term / sequence of actions) +- **T_goal** = goal type (the proposition to be satisfied) +- **⊢** = "yields" / "proves" + +Reading: "Given context Γ, the program p has type T_goal" = "Given the facts Γ, the plan p achieves the goal T_goal" + +--- + +## Blocks World Action Types + +``` +pickup : Π(x:Block). (OnTable(x) ∧ Clear(x) ∧ HandEmpty) → Holding(x) + +stack : Π(x y:Block). (Holding(x) ∧ Clear(y)) → On(x, y) +``` + +Plan to satisfy `On(RedBlock, BlueBlock)` from initial state `{OnTable(r), Clear(r), OnTable(b), Clear(b), HandEmpty}`: + +``` +p = stack RedBlock BlueBlock (pickup RedBlock (...)) + : On(RedBlock, BlueBlock) +``` + +Type-checks → plan is verified by construction. + +--- + +## Logic-LM Benchmark Context Table + +| Dataset | Standard Prompting | Logic-LM (GPT-3.5) | Δ (pp) | +|---------|-------------------|---------------------|--------| +| ProofWriter | ~70% | ~88% | ~18 | +| PrOntoQA | ~75% | ~92% | ~17 | +| FOLIO | 45.09% | 62.80% | 17.71 | +| LogicalDeduction | ~65% | ~90% | ~25 | +| AR-LSAT | ~30% | ~44% | ~14 | +| **Average** | | | **~39.2% over standard; ~18.4% over CoT** | + +Note: The 39.2% headline is a multi-dataset average. On FOLIO specifically the gain is 17.71 pp. +A 2025 replication (arXiv:2502.17216) found 45.23% or 24.98% depending on methodology. + +--- + +## Kautz NSAI Taxonomy (6 Patterns) + +| Pattern | Neural Role | Symbolic Role | Example | +|---------|-------------|---------------|---------| +| Symbolic→Neural→Symbolic | Transform | I/O | LLMs, seq2seq | +| Symbolic[Neural] | Subroutine | Orchestrator | AlphaGo (MCTS + NN) | +| Neural[Symbolic] | Orchestrator | Tool/subroutine | LLM + calculator | +| Neural\|Symbolic | Coroutine | Coroutine | Iterative refinement | +| Neural:Symbolic→Neural | Training data source | Generator | Math data synthesis | +| Neural:Symbolic (Compiled) | Architecture substrate | Compiled into | LTN, LNN | + +NSAM target pattern: **Neural\|Symbolic** (cooperative coroutines) +with a Neural[Symbolic] fallback for the REST API integration path. + +--- + +## Hypersequent Dependence Logic (verumorphism) + +verumorphism implements HDL over ternary truth values {0, 1, i}: +- **0** = refutation (negative real) +- **1** = proof (positive real) +- **i** = non-closure (zero / indeterminate) + +Key rules: `con_R`, `incon_L`, `dualR`, `dualL`, `dependenceR`, `independenceL` + +This is the symbolic core the NSAM paper motivates connecting to larql-to-sparql's +neural mechanistic interpretability stack. diff --git a/papers/ai_and_agents/principled-agent-architectures-review/scratch/notes.md b/papers/ai_and_agents/principled-agent-architectures-review/scratch/notes.md new file mode 100644 index 0000000..b3aeacb --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/scratch/notes.md @@ -0,0 +1,87 @@ +# Research Session Notes — NSAM Critical Review + +Date: 2026-06-23 +Deep research: 105 agents, 1307 tool uses, 2,247,194 subagent tokens +Workflow output: tasks/wrhx44ghb.output (25KB JSON) + +--- + +## Key Findings Summary + +1. **Logic-LM 39.2%**: Real figure but stripped of context. Per-dataset numbers range 14–25 pp. + Paper should cite EMNLP 2023 Table 2 directly with dataset breakdown. + +2. **Mamba 5x throughput**: Rejected 0-3. Primary paper doesn't state this number. + The linear scaling claim is valid; the specific quantification is not. + +3. **FNet 80% speedup**: Confirmed. But 92–97% GLUE retention is contested (rejected 1-2). + Safe to cite speedup; drop the accuracy retention claim. + +4. **Curry-Howard novelty**: The Proof-Carrying Plans paper (PPDP 2020, ACM 10.1145/3414080.3414094) + explicitly does plans-as-functions, pre/post-conditions as types. Agda implementation predates 2019. + The NSAM paper must cite this. Contribution should be framed as integration architecture. + +5. **PyReason scalability**: Self-reported benchmarks vs. simulators, not vs. peer logic systems. + Excluded from the 2025 comparative study (arXiv:2509.07122). Scallop is better supported. + +6. **Scallop/A-NeSI**: Claims accurate but A-NeSI has provably biased gradient estimators (2024). + +--- + +## Citation Gaps in NSAM Paper + +The paper does not cite: +- Hill, Komendantskaya & Petrick 2020 (PCP) — direct prior art +- Brady & Hammond 2021 — dependent types for AI plans +- Masseron, Tollu & Vauzeilles 1990 — linear logic planning +- Kanovich & Vauzeilles 2001 — linear logic planning +- DeepProbLog (Manhaeve et al., NeurIPS 2018) +- A-NeSI (van Krieken et al., NeurIPS 2023) — only mentions Scallop +- Comparative survey arXiv:2509.07122 that excludes PyReason from empirical tables + +--- + +## Open Questions for Follow-up + +1. What IS the correct Mamba throughput number vs. Transformers? The paper cited 5x; + the primary source didn't say that. What does Figure 8 in arXiv:2312.00752 actually show? + +2. Does the PyReason LAT Logic paper (arXiv:2509.02958) actually benchmark vs. Scallop? + The verified claim says no — only vs. AFSIM and StarCraft II simulators. + +3. Is there a benchmark that covers PyReason, Scallop, DeepProbLog, LTN, and LNN on the + same tasks? The 2025 survey (arXiv:2509.07122) deliberately excluded PyReason. + +4. What would it take to wire verumorphism (HDL REST API) to larql-to-sparql (vindex neural + substrate) as the NSAM integration? larql-probe → vindex → LQL query → HDL propositions → verumorphism? + +--- + +## Portfolio Architecture Insight + +The "NSAM architecture already exists in the portfolio, just not wired" framing: + +``` +[Raw data / Wikidata triples] + ↓ +[larql-to-sparql: vindex + knowledge/ pipeline] ← NSAM neural perceptual layer + - transformer weights decompiled to vindex + - knowledge/ = Wikidata/DBpedia/WordNet → semantic labels + - mechanistic interp hooks (ablation, steering, etc.) + ↓ +[Formal propositions: Is(b1,Block), Color(b1,Red), ...] + ↓ +[verumorphism REST API: HDL calculus] ← NSAM symbolic reasoning layer + - ProverV0.lisp / RefuterV0.lisp threads + - HDL rules: con_R / incon_L / dualR / etc. + - ternary logic {0,1,i} proof/refutation + ↓ +[Plan / proof term output] + ↓ +[drstrangegoo sequoia_engine (PR#4)] ← optional: parameterized proof-search oracle + - cut elimination, identity coherence + - YAML-defined calculi (intuitionistic, linear) +``` + +subclass Proof phantom types = type-safe reference implementation of the plans-as-proofs +paradigm, potentially useful as a Java binding layer. diff --git a/papers/ai_and_agents/principled-agent-architectures-review/src/bibliography.bib b/papers/ai_and_agents/principled-agent-architectures-review/src/bibliography.bib new file mode 100644 index 0000000..27c9538 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/src/bibliography.bib @@ -0,0 +1,210 @@ +% Bibliography for NSAM Critical Review +% 23 sources from deep research workflow (105 agents, 2,247,194 tokens) + +@inproceedings{logic-lm-2023, + author = {Pan, Liangming and Albalak, Alon and Wang, Xinyi and Wang, William Yang}, + title = {Logic-{LM}: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning}, + booktitle = {Findings of the Association for Computational Linguistics: EMNLP 2023}, + year = {2023}, + publisher = {Association for Computational Linguistics}, + pages = {3806--3824}, + url = {https://aclanthology.org/2023.findings-emnlp.248/}, + doi = {10.18653/v1/2023.findings-emnlp.248} +} + +@misc{logic-lm-arxiv-2023, + author = {Pan, Liangming and Albalak, Alon and Wang, Xinyi and Wang, William Yang}, + title = {Logic-{LM}: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning}, + year = {2023}, + eprint = {2305.12295}, + archivePrefix = {arXiv}, + primaryClass = {cs.CL}, + url = {https://arxiv.org/abs/2305.12295} +} + +@inproceedings{mamba-2023, + author = {Gu, Albert and Dao, Tri}, + title = {Mamba: Linear-Time Sequence Modeling with Selective State Spaces}, + year = {2024}, + booktitle = {First Conference on Language Modeling (COLM 2024)}, + eprint = {2312.00752}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/pdf/2312.00752} +} + +@inproceedings{fnet-2022, + author = {Lee-Thorp, James and Ainslie, Joshua and Eckstein, Ilya and Ontanon, Santiago}, + title = {{FNet}: Mixing Tokens with {Fourier} Transforms}, + booktitle = {Proceedings of NAACL 2022}, + year = {2022}, + publisher = {Association for Computational Linguistics}, + eprint = {2105.03824}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/pdf/2105.03824} +} + +@misc{logic-lm-replication-2025, + author = {Anonymous}, + title = {Replication study: {Logic-LM} performance across models and averaging methodologies}, + year = {2025}, + eprint = {2502.17216}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2502.17216} +} + +@misc{logic-lm-pp-2024, + author = {Anonymous}, + title = {Logic-{LM}++: Improved Logical Reasoning with Enhanced Symbolic Integration}, + year = {2024}, + eprint = {2407.02514}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/pdf/2407.02514} +} + +@misc{curry-howard-cot-2025, + title = {Chain-of-Thought as Typed Proof: {Curry-Howard} for {LLM} Reasoning}, + year = {2025}, + eprint = {2510.01069}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2510.01069} +} + +@inproceedings{proof-carrying-plans-2020, + author = {Hill, Ekaterina and Komendantskaya, Ekaterina and Petrick, Ronald P. A.}, + title = {Proof-Carrying Plans}, + booktitle = {Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming (PPDP 2020)}, + year = {2020}, + publisher = {ACM}, + doi = {10.1145/3414080.3414094}, + url = {https://arxiv.org/abs/2008.04165} +} + +@misc{dependent-types-ai-plans-2021, + author = {Brady, Edwin and Hammond, Kevin}, + title = {Actions You Can Handle: Dependent Types for {AI} Plans}, + year = {2021}, + eprint = {2105.11267}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2105.11267} +} + +@misc{constructive-rl-2025, + title = {Constructive Symbolic {RL}: Planning as Theorem Proving under Intuitionistic Logic}, + year = {2025}, + eprint = {2506.05422}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2506.05422} +} + +@inproceedings{scallop-pldi-2023, + author = {Li, Ziyang and Huang, Jiani and Naik, Mayur}, + title = {Scallop: A Language for Neurosymbolic Programming}, + booktitle = {Proceedings of the ACM on Programming Languages (PLDI 2023)}, + year = {2023}, + publisher = {ACM}, + doi = {10.1145/3591280}, + url = {https://dl.acm.org/doi/10.1145/3591280} +} + +@inproceedings{anesi-2022, + author = {van Krieken, Emile and Thanapalasingam, Thiviyan and Tomczak, Jakub M. and van Harmelen, Frank and ten Teije, Annette}, + title = {{A-NeSI}: A Scalable Approximate Method for Probabilistic Neurosymbolic Inference}, + booktitle = {Advances in Neural Information Processing Systems (NeurIPS 2023)}, + year = {2023}, + eprint = {2212.12393}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2212.12393} +} + +@misc{anesi-hardness-2024, + title = {Hardness of Neurosymbolic Approximation: Biased Gradient Estimators and {A-NeSI}}, + year = {2024}, + eprint = {2406.04472}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2406.04472} +} + +@misc{pyreason-2023, + author = {Adithan, Dyuman and others}, + title = {{PyReason}: Software for Open World Temporal Logic}, + year = {2023}, + eprint = {2302.13482}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2302.13482} +} + +@misc{pyreason-lat-2025, + title = {Large-Scale Annotated Logic with {PyReason}: {LAT} Logic}, + year = {2025}, + eprint = {2509.02958}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/pdf/2509.02958} +} + +@misc{nsai-survey-2025, + title = {Comparative Study of Neurosymbolic Frameworks}, + year = {2025}, + eprint = {2509.07122}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2509.07122} +} + +@misc{jamba-2024, + author = {Team, AI21}, + title = {Jamba: A Hybrid Transformer-Mamba Language Model}, + year = {2024}, + eprint = {2403.19887}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2403.19887} +} + +@inproceedings{ltn-2022, + author = {Badreddine, Samy and d'Avila Garcez, Artur and Serafini, Luciano and Spranger, Michael}, + title = {Logic Tensor Networks}, + booktitle = {Artificial Intelligence}, + year = {2022}, + volume = {303}, + publisher = {Elsevier}, + doi = {10.1016/j.artint.2021.103649} +} + +@inproceedings{lnn-2021, + author = {Riegel, Ryan and others}, + title = {Logical Neural Networks}, + year = {2021}, + eprint = {2006.13155}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2006.13155} +} + +@article{linear-logic-planning-1990, + author = {Masseron, Mireille and Tollu, Christophe and Vauzeilles, Josiane}, + title = {Generating Plans in Linear Logic}, + journal = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1990)}, + year = {1990}, + publisher = {Springer} +} + +@article{kahneman-2011, + author = {Kahneman, Daniel}, + title = {Thinking, Fast and Slow}, + year = {2011}, + publisher = {Farrar, Straus and Giroux} +} + +@inproceedings{kautz-nsai-2022, + author = {Kautz, Henry}, + title = {The Third {AI} Summer: {AAAI Robert S. Engelmore Memorial Award} Lecture}, + booktitle = {AI Magazine}, + year = {2022}, + volume = {43}, + number = {1}, + pages = {105--125} +} + +@misc{logic-lm-survey-2025, + title = {Neurosymbolic {AI} Agent Survey: Frameworks and Evaluation}, + year = {2025}, + archivePrefix = {arXiv}, + url = {https://arxiv.org/abs/2509.07122} +} From ab054d24690a35d5ed16cd38be8210e163f101a9 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:58:25 -0700 Subject: [PATCH 7/9] feat: add XSLT 1.0 DocBook-to-HTML5 and DocBook-to-LaTeX transforms Co-Authored-By: Claude Sonnet 4.6 --- .../xsl/html5.xsl | 195 +++++++++++++ .../xsl/latex.xsl | 266 ++++++++++++++++++ 2 files changed, 461 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/xsl/html5.xsl create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/xsl/latex.xsl diff --git a/papers/ai_and_agents/principled-agent-architectures-review/xsl/html5.xsl b/papers/ai_and_agents/principled-agent-architectures-review/xsl/html5.xsl new file mode 100644 index 0000000..cc576ea --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/xsl/html5.xsl @@ -0,0 +1,195 @@ + + + + + + + + + + + + <xsl:value-of select="db:title"/> + + + + + + + + + + + + + + + +
+
+

+
+ +
Author:
+ + +
Date:
+ + +
License:
+ +
+
+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+ + + + + + + +

+

+

+ + + + + +

+ + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + +
+ + +
+ + +
    • +     + + + + + + +
    +     + + + + + + + + + +     diff --git a/papers/ai_and_agents/principled-agent-architectures-review/xsl/latex.xsl b/papers/ai_and_agents/principled-agent-architectures-review/xsl/latex.xsl new file mode 100644 index 0000000..277e2c9 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/xsl/latex.xsl @@ -0,0 +1,266 @@ + + + + + + + + \documentclass[12pt,a4paper]{article} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{lmodern} +\usepackage{hyperref} +\usepackage{booktabs} +\usepackage{longtable} +\usepackage{enumitem} +\usepackage{xcolor} +\definecolor{confirmed}{RGB}{0,140,70} +\definecolor{split}{RGB}{180,100,0} +\definecolor{caveats}{RGB}{40,80,180} + + + + \title{ + + + + + + + + + + + + + } + + + + \author{ + + + + } + + + + + \date{ + + } + + + +\begin{document} +\maketitle +\tableofcontents +\newpage + + + + +\bibliographystyle{plain} +\bibliography{../src/bibliography} + +\end{document} + + + + + + + + + +\noindent{\color{ + + confirmed + split + caveats + + }\rule{\linewidth}{1.5pt}} + + + + + \section{ + + + + } + + + + \subsection{ + + + + } + + + + \subsubsection{ + + + + } + + + + + + + + + + + + + + + + + + + \textbf{ + + + + } + + + \textit{ + + + + } + + + + + \href{ + + }{ + + + + } + + + + + +\begin{longtable}{ + + l + + + + l + + + } +\toprule + + + + \bottomrule +\end{longtable} + + + + + + + \midrule + + + + + + + + + + + + + + + + + & + + + + \\ + + + + + + +\begin{itemize} + + + \end{itemize} + + + + + + +\begin{enumerate} + + + \end{enumerate} + + + + + + \item + + + + + + \texttt{ + + + + } + + + + +\begin{verbatim} + + + +\end{verbatim} + + + + + + + + + + + + + + + + + + + From e278b76bd1c9920a9b41aa57b0ef7714132c8ba2 Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:58:59 -0700 Subject: [PATCH 8/9] feat: add RELAX NG compact schema and DocBook build Makefile Co-Authored-By: Claude Sonnet 4.6 --- .../Makefile | 64 ++++++++ .../schema/critical-review.rnc | 137 ++++++++++++++++++ 2 files changed, 201 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/Makefile create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/schema/critical-review.rnc diff --git a/papers/ai_and_agents/principled-agent-architectures-review/Makefile b/papers/ai_and_agents/principled-agent-architectures-review/Makefile new file mode 100644 index 0000000..51d7814 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/Makefile @@ -0,0 +1,64 @@ +# Build pipeline: DocBook 5.2 XML → HTML5 and LaTeX +# TeX/PDF are derived outputs; XML is the canonical source. +# +# Requirements: +# xsltproc (libxslt) +# xmllint (libxml2) +# pdflatex (texlive) +# jing (RELAX NG validator, optional) + +SRCS := $(wildcard src/0*.xml) +HTML_OUTS := $(patsubst src/%.xml,generated/%.html,$(SRCS)) +TEX_OUTS := $(patsubst src/%.xml,generated/%.tex,$(SRCS)) + +.PHONY: all html latex validate validate-rnc clean + +all: validate html latex + +# --------------------------------------------------------------- +# Validation against DocBook 5.2 RELAX NG + +validate: $(SRCS) + @for f in $(SRCS); do \ + echo "Validating $$f ..."; \ + xmllint --noout --xinclude \ + --relaxng https://docbook.org/xml/5.2/rng/docbook.rng "$$f" && \ + echo " OK: $$f"; \ + done + +# Optional: validate finding sections against custom RNC schema (requires jing) +validate-rnc: src/02-critical-review.xml schema/critical-review.rnc + jing -c schema/critical-review.rnc src/02-critical-review.xml + +# --------------------------------------------------------------- +# HTML5 generation + +html: $(HTML_OUTS) + +generated/%.html: src/%.xml xsl/html5.xsl | generated + xsltproc --xinclude xsl/html5.xsl $< > $@ + +# --------------------------------------------------------------- +# LaTeX generation + +latex: $(TEX_OUTS) + +generated/%.tex: src/%.xml xsl/latex.xsl | generated + xsltproc --xinclude xsl/latex.xsl $< > $@ + +# --------------------------------------------------------------- +# PDF from LaTeX (two-pass for TOC and references) + +generated/%.pdf: generated/%.tex | generated + cd generated && pdflatex -interaction=nonstopmode $(notdir $<) + cd generated && pdflatex -interaction=nonstopmode $(notdir $<) + +# --------------------------------------------------------------- +# Utility + +generated: + mkdir -p generated + +clean: + rm -f generated/*.html generated/*.tex generated/*.pdf + rm -f generated/*.aux generated/*.log generated/*.out generated/*.toc diff --git a/papers/ai_and_agents/principled-agent-architectures-review/schema/critical-review.rnc b/papers/ai_and_agents/principled-agent-architectures-review/schema/critical-review.rnc new file mode 100644 index 0000000..0c979fa --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/schema/critical-review.rnc @@ -0,0 +1,137 @@ +# RELAX NG Compact Schema for NSAM Critical Review Documents +# Extends DocBook 5.2 with custom role/condition attributes +# Used to validate src/02-critical-review.xml finding sections + +namespace db = "http://docbook.org/ns/docbook" +namespace dc = "http://purl.org/dc/terms/" +namespace schema = "https://schema.org/" +namespace xi = "http://www.w3.org/2001/XInclude" +namespace xlink = "http://www.w3.org/1999/xlink" +namespace local = "" + +# --------------------------------------------------------------- +# Custom attribute values + +finding-condition = + "confirmed" | "confirmed-with-caveats" | "split" + +finding-role = + "finding" + +# --------------------------------------------------------------- +# Finding section: a db:section with role="finding" and condition +# These appear inside db:section[@xml:id='cr-findings'] + +finding-section = + element db:section { + attribute xml:id { xsd:NCName }, + attribute role { finding-role }, + attribute condition { finding-condition }, + element db:title { text }, + element db:para { mixed { inline-content* } }+ + } + +# --------------------------------------------------------------- +# Inline content (used inside para) + +inline-content = + element db:emphasis { + attribute role { "bold" }?, + text + } + | element db:link { + attribute xlink:href { xsd:anyURI }, + text + } + | element db:code { text } + | text + +# --------------------------------------------------------------- +# Ordered and unordered lists + +list-item = + element db:listitem { + element db:para { mixed { inline-content* } } + } + +ordered-list = + element db:orderedlist { + list-item+ + } + +unordered-list = + element db:itemizedlist { + list-item+ + } + +# --------------------------------------------------------------- +# Table structures + +table-entry = element db:entry { mixed { inline-content* } } +table-row = element db:row { table-entry+ } +table-head = element db:thead { table-row+ } +table-body = element db:tbody { table-row+ } +table-group = element db:tgroup { + attribute cols { xsd:positiveInteger }, + element db:colspec { + attribute colname { text }?, + attribute colwidth { text }? + }*, + table-head?, + table-body +} +informal-table = element db:informaltable { table-group } + +# --------------------------------------------------------------- +# Section content: paragraphs, lists, tables, subsections + +section-content = + element db:para { mixed { inline-content* } } + | ordered-list + | unordered-list + | informal-table + | finding-section + | element db:section { + attribute xml:id { xsd:NCName }?, + element db:title { text }, + section-content* + } + +# --------------------------------------------------------------- +# Metadata block (from XInclude of 00-metadata.xml) + +dc-info = + element db:info { + element dc:title { text }, + element dc:creator { text }, + element dc:subject { text }?, + element dc:description { text }?, + element dc:publisher { text }?, + element dc:date { text }, + element dc:type { text }?, + element dc:format { text }?, + element dc:language { text }?, + element dc:rights { text }?, + element dc:source { text }?, + element db:bibliomisc { + attribute role { "schema-org-jsonld" }, + text + }? + } + +# --------------------------------------------------------------- +# Top-level article + +start = + element db:article { + attribute version { "5.2" }, + attribute xml:id { xsd:NCName }, + attribute xml:lang { "en" }, + dc-info, + element db:title { text }, + element db:section { + attribute xml:id { xsd:NCName }, + element db:title { text }, + section-content* + }+ + } From 33c737c76d3fa3a34fcfed65c12449776ab01e2c Mon Sep 17 00:00:00 2001 From: metavacua Date: Tue, 23 Jun 2026 21:59:32 -0700 Subject: [PATCH 9/9] feat: add README with build instructions and findings summary Co-Authored-By: Claude Sonnet 4.6 --- .../README.md | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 papers/ai_and_agents/principled-agent-architectures-review/README.md diff --git a/papers/ai_and_agents/principled-agent-architectures-review/README.md b/papers/ai_and_agents/principled-agent-architectures-review/README.md new file mode 100644 index 0000000..339c6b0 --- /dev/null +++ b/papers/ai_and_agents/principled-agent-architectures-review/README.md @@ -0,0 +1,87 @@ +# Principled Agent Architectures: Critical Review and Repository Audit + +Adversarially verified critical review of "Principled Agent Architectures: A Neuro-Symbolic +Blueprint Beyond Large Language Models," with a 7-repository relevance audit across the +metavacua GitHub portfolio. + +**Deep research provenance:** 105 agents · 1,307 tool uses · 2,247,194 subagent tokens · 2026-06-23 + +## Contents + +``` +src/ + 00-metadata.xml Dublin Core + Schema.org metadata (XIncluded by articles) + 01-original-paper.xml Full NSAM paper encoded as DocBook 5.2 XML + 02-critical-review.xml 6 verified findings, 11 refuted claims, 4 open questions + 03-repository-audit.xml 7-repo relevance audit with cross-repo synthesis + bibliography.bib 23 BibTeX sources + +xsl/ + html5.xsl DocBook → HTML5 with DC meta tags + Schema.org JSON-LD + latex.xsl DocBook → LaTeX (article class, longtable, booktabs) + +schema/ + critical-review.rnc RELAX NG Compact schema extending DocBook 5.2 + +scratch/ + formulas.md Curry-Howard table, NSAM typing judgments, benchmark tables + notes.md Session notes, citation gaps, open questions, portfolio diagram + +generated/ (git-ignored) HTML5 and LaTeX outputs +``` + +## Building + +```bash +# Validate XML against DocBook 5.2 RELAX NG +make validate + +# Generate HTML5 +make html + +# Generate LaTeX +make latex + +# Both +make all +``` + +Requirements: `xsltproc` (libxslt), `xmllint` (libxml2), `pdflatex` (optional, for PDF). + +## Key Findings + +| Finding | Verdict | +|---------|---------| +| Logic-LM 39.2% figure lacks dataset/model context | Confirmed with caveats | +| Mamba linear scaling valid; 5x throughput unsupported | Split | +| FNet 80% speedup accurate; 92–97% GLUE retention contested | Split | +| Curry-Howard for agent planning anticipated by Proof-Carrying Plans (PPDP 2020) | Confirmed | +| Scallop/A-NeSI claims accurate but require qualification | Confirmed with caveats | +| PyReason features confirmed; "exact yet scalable" vs. peers unsupported | Split | + +## Repository Audit Summary + +| Repository | Relevance | Role in NSAM Architecture | +|------------|-----------|--------------------------| +| metavacua/Theory | HIGH | Primary placement | +| metavacua/verumorphism | HIGH | **Symbolic reasoning core** (HDL calculus + REST API) | +| metavacua/CategoricalReasoner | MEDIUM-HIGH | Curry-Howard theory chapters | +| metavacua/drstrangegoo | MEDIUM-HIGH | Proof-search oracle candidate (sequoia_engine PR#4) | +| metavacua/subclass | MEDIUM-HIGH | Live Curry-Howard implementation (Proof\ phantom types) | +| metavacua/larql-to-sparql | MEDIUM | **Neural substrate** (vindex + knowledge/ semantic grounding) | +| metavacua/GeodesicLangModel | LOW | Adjacent framework (footnote only) | + +**Key insight:** verumorphism (symbolic half) + larql-to-sparql (neural half) already implement +both sides of the NSAM architecture — they simply are not yet wired together. The NSAM blueprint +motivates building that integration. + +## License + +AGPL-3.0-or-later + +## Standards + +- [DocBook 5.2](https://docbook.org/specs/docbook-v5.2-csprd01.html) — canonical XML source +- [Dublin Core Terms](https://www.dublincore.org/specifications/dublin-core/dcmi-terms/) — metadata +- [Schema.org ScholarlyArticle](https://schema.org/ScholarlyArticle) — JSON-LD structured data +- [RELAX NG Compact](https://relaxng.org/compact-tutorial-20030326.html) — schema validation