Safin-1.5: Safety-Native Architecture and Verifiable Reasoning for Recursive Safety Improvement

# Safin-1.5: Safety-Native Architecture and Verifiable Reasoning for Recursive Safety Improvement
Source: [https://arxiv.org/html/2610.40751](https://arxiv.org/html/2610.40751)
\\setleftlogo

\[180pt\]imgs/logo\_lab\.png\\setrightlogo\[180pt\]

###### Abstract Recursive self\-improvement \(RSI\) enables large language models to advance their capabilities through successive updates, but these updates can also introduce new risks and weaken existing safeguards\. In line with the AI\-45° Law, we pursue Safety RSI, in which safety develops as an intrinsic capability alongside general model capabilities through continual risk discovery and repair, while preserving utility and limiting over\-refusal\. We introduceSafin\-1\.5, a model built on a safety architecture and trained through recursive safety improvement, with an inference\-time harness that extends its capabilities to formal reasoning\. Our approach comprises three components: i\) The safety architecture combines persistent safety states with hazardous\-knowledge disentanglement\. The former retains and selectively invokes safety knowledge, while the latter relocates targeted hazardous knowledge into removable experts, enabling its removal with minimal impact on general capabilities\. ii\) Recursive safety improvement establishes a discovery–evaluation–repair loop\. The loop identifies new vulnerabilities and uses experimental feedback to develop repair strategies\. It accepts updates only when they improve safety while preserving general capabilities and limiting over\-refusal\. iii\) The formal reasoning harness combines the model’s language understanding with symbolic inference and verification\. Proof\-obligation\-guided semantic bridging recovers missing relations in formal representations, enabling symbolic solvers to construct checkable proofs under formalized premises and accepted semantic bridges\. Experimental results demonstrate thatSafin\-1\.5achieves safety and reasoning performance, outperforming frontier models\.

![Refer to caption](https://arxiv.org/html/2610.40751v1/teaser-v2.png)Figure 1:Main evaluation results ofSafin\-1\.5\(35B\) compared with frontier models across safety and formal reasoning benchmarks\. For lower\-is\-better benchmarks \(H\-CoT, X\-Teaming, and WJB\), results are reported as100 \- metric, so higher scores consistently indicate better performance\.Contents

## 1Introduction

Rapid advances in large language model \(LLM\)\[[26](https://arxiv.org/html/2610.40751#bib.bib44),[51](https://arxiv.org/html/2610.40751#bib.bib8),[14](https://arxiv.org/html/2610.40751#bib.bib43)\]capabilities have given rise to an emerging paradigm of recursive self\-improvement \(RSI\)\[[5](https://arxiv.org/html/2610.40751#bib.bib10),[7](https://arxiv.org/html/2610.40751#bib.bib41),[63](https://arxiv.org/html/2610.40751#bib.bib42)\], in which models become the primary drivers of their own iterative improvement, enabling them to continuously adapt to increasingly complex scenarios and tasks\[[24](https://arxiv.org/html/2610.40751#bib.bib2),[54](https://arxiv.org/html/2610.40751#bib.bib1)\]\. However, sustained growth in model capabilities does not automatically translate into corresponding gains in safety\. Prior work has shown that even a single fine\-tuning step can weaken a model’s established alignment\[[34](https://arxiv.org/html/2610.40751#bib.bib14),[33](https://arxiv.org/html/2610.40751#bib.bib5)\]; over the course of recursive evolution, repeated model updates may introduce new safety vulnerabilities and exacerbate existing safety issues\[[12](https://arxiv.org/html/2610.40751#bib.bib11),[8](https://arxiv.org/html/2610.40751#bib.bib12),[61](https://arxiv.org/html/2610.40751#bib.bib13)\]\. Nevertheless, current self\-improvement methods predominantly optimize for benchmark performance, without systematically incorporating safety into the evolutionary loop, making it difficult to ensure that safety capabilities keep pace with ongoing changes in model capabilities\. Leading AI organizations have begun to confront this capability–safety gap: the GPT\-5\.6\[[29](https://arxiv.org/html/2610.40751#bib.bib3)\]and Claude 4\[[1](https://arxiv.org/html/2610.40751#bib.bib4)\]system cards assess not only model capabilities but also risks such as misuse, prompt injection, and alignment failures, while documenting the corresponding safeguards in safety training and deployment\. These practices resonate with the central claim of our previously proposed AI\-45° law\[[19](https://arxiv.org/html/2610.40751#bib.bib9)\]: safety capabilities should co\-evolve with model capabilities, rather than being applied as post hoc patches after model capabilities have stabilized\.

Such coevolution requires safety alignment to continue throughout recursive model improvement—a process we term Safety RSI\. As model capabilities and attack strategies evolve, static alignment against a fixed set of risks becomes insufficient\[[50](https://arxiv.org/html/2610.40751#bib.bib39),[65](https://arxiv.org/html/2610.40751#bib.bib40),[46](https://arxiv.org/html/2610.40751#bib.bib32),[43](https://arxiv.org/html/2610.40751#bib.bib31)\]\. Safety RSI therefore requires continual discovery and repair of emerging vulnerabilities while preserving utility and limiting over\-refusal\. OpenAI’s GPT\-Red illustrates how self\-play\-trained red\-teamers can generate attacks that improve subsequent models’ prompt\-injection robustness\[[29](https://arxiv.org/html/2610.40751#bib.bib3),[45](https://arxiv.org/html/2610.40751#bib.bib33)\]\. However, this continual discover\-and\-repair process is undermined by how current models encode and store knowledge: i\) current architectures store safety knowledge in shared parameters rather than a dedicated substrate, so it is overwritten by subsequent updates as the model evolves and previously addressed risks are forgotten\[[34](https://arxiv.org/html/2610.40751#bib.bib14),[33](https://arxiv.org/html/2610.40751#bib.bib5)\]; ii\) current architectures encode hazardous and general knowledge in shared parameters, making it difficult to locate and isolate hazardous knowledge as models improve through RSI\. Interventions on these parameters may impair general capabilities\[[20](https://arxiv.org/html/2610.40751#bib.bib6),[58](https://arxiv.org/html/2610.40751#bib.bib7)\], while subsequent fine\-tuning can restore previously suppressed hazardous knowledge\[[6](https://arxiv.org/html/2610.40751#bib.bib15)\]\. Addressing these limitations requires architectural support for safety memory and hazardous\-knowledge disentanglement: the former retains safety experience for use in later updates, while the latter separates hazardous knowledge from general knowledge so it can be removed with minimal impact on general capabilities\.

These mechanisms support the continuous development and preservation of safety capabilities throughout Safety RSI\. However, the resulting alignment remains primarily empirical: models learn safety responses from risk\-related data, without necessarily establishing why a response satisfies the relevant safety requirements\. Formal reasoning complements this empirical alignment by enabling the system to reason explicitly about safety\-relevant conditions and derive conclusions from specified premises and rules\. An inference\-time neuro\-symbolic harness can implement this capability by combining the model’s language understanding with symbolic solvers that derive conclusions and construct checkable proofs under explicit assumptions\[[49](https://arxiv.org/html/2610.40751#bib.bib34)\]\. These proofs provide a machine\-checkable basis for safety judgments beyond learned refusal behavior, with guarantees scoped to the formalized assumptions and safety requirements\. The applicability of these guarantees to the original problems depends on how faithfully the formal representations capture their meaning\. In existing neuro\-symbolic approaches, translating natural\-language problems into formal representations can omit implicit premises or semantic relations, while variations in wording can lead to inconsistent formalizations, preventing the solver from establishing the intended conclusion\[[30](https://arxiv.org/html/2610.40751#bib.bib35),[13](https://arxiv.org/html/2610.40751#bib.bib36)\]\. Addressing this gap must therefore preserve the connection between natural\-language meaning and formal representations, making both the formalized premises and the semantic bridges used in reasoning explicit so that the resulting proofs can be checked and interpreted within their stated scope\.

![Refer to caption](https://arxiv.org/html/2610.40751v1/framework-v3.png)Figure 2:Overview ofSafin\-1\.5\. At the architectural level,MARCHandREXprovide persistent safety memory and hazardous\-knowledge disentanglement, respectively\. At the training level,ReSIsupports continual safety improvement through iterative red\-teaming, pilot screening, and full\-scale model updates\. At the formal assurance level, the formal reasoning harness leveragesPOGBto address semantic gaps between natural\-language problems and formal representations, enhancing the model’s logical reasoning capabilities\.Building on these requirements, we introduceSafin\-1\.5, the latest generation of the Safin series\. Its predecessor, Safin\-1\[[56](https://arxiv.org/html/2610.40751#bib.bib24)\], offered an initial exploration of Safety from Within, demonstrating the potential of integrating persistent safety capabilities into a model’s internal architecture\.Safin\-1\.5extends this foundation into a full\-stack framework for operationalizing Safety RSI by co\-designing model architecture, continual training, and formal assurance, as illustrated in Figure[2](https://arxiv.org/html/2610.40751#S1.F2)\. At the architectural level, we integrateMemory\-Anchor Routing across Context History \(MARCH\)\[[57](https://arxiv.org/html/2610.40751#bib.bib45)\]andRelocating into Removable EXperts \(REX\)\[[16](https://arxiv.org/html/2610.40751#bib.bib46)\]to support persistent safety memory and hazardous\-knowledge disentanglement, respectively\. Together, these mechanisms enable safety experience to be retained and reused across model updates while facilitating the targeted removal of hazardous knowledge with minimal disruption to general capabilities\. At the training level,Recursive Safety Improvement \(ReSI\)\[[62](https://arxiv.org/html/2610.40751#bib.bib37)\]operationalizes Safety RSI through a continual cycle of risk discovery, evaluation, and repair, allowing safety alignment to adapt to emerging vulnerabilities while balancing safety improvements, capability retention, and over\-refusal\. The architectural mechanisms underpin this cycle by preserving prior safety experience and enabling targeted interventions against newly identified risks\. At the formal assurance level,Proof\-Obligation\-Guided Bridging \(POGB\)\[[41](https://arxiv.org/html/2610.40751#bib.bib38)\]serves as the core mechanism of our Formal Reasoning Harness, complementing empirical safety evaluation with verifiable reasoning evidence at inference time\. By addressing semantic gaps between natural\-language problems and formal representations, it enables machine\-checkable verification of conclusions in logical reasoning tasks under explicit assumptions\.

Our main contributions are as follows:

- •We build on Safin\-1’s safety memory and incorporate REX\-based hazardous\-knowledge disentanglement to support continual safety improvement\. i\) The inherited MARCH interface makes persistent safety states selectively accessible within model computation; ii\) REX relocates the hazardous knowledge already present in a pretrained MoE model into newly added removable experts, keeps general capability in the original experts, trains subsequent updates on the full model, and physically excises the removable experts at deployment\. On Safin\-1, a single set of removable experts carries both Bio and Cyber knowledge; one excision substantially lowers WMDP accuracy in both domains, and the removal persists through standard post\-training andReSI, whereas the same RMU recipe rebounds almost completely under the same post\-training\.
- •We integrateReSIas the training harness for Safety RSI\. In each round,ReSIapplies diverse red\-teaming methods to identify vulnerabilities in the current target model, develops a training recipe through automated research, and promotes the update with the largest safety gain among those passing a Pareto gate on benign compliance and instruction following\. On the disentangled architecture,ReSItrains the full model while red\-teaming, validating, and gating its excised counterpart, and its extensible pools of red\-teaming and alignment methods let the loop incorporate new attacks and learning approaches\.
- •To support trustworthy safety improvement beyond empirical evaluation, we enhance the reliability of logical reasoning through machine\-checkable proofs\. We introduce POGB, which addresses semantic gaps between natural\-language statements and formal representations by integrating LLM\-based semantic understanding with solver\-controlled logical reasoning\. Extensive experiments demonstrate substantial improvements in reasoning accuracy across diverse benchmarks\.
- •Experimental results show that, compared with Safin\-1,Safin\-1\.5reduces H\-CoT ASR from 82\.00% to 14\.00% and X\-Teaming ASR from 64\.78% to 32\.08%, lower than all evaluated frontier models on X\-Teaming, while largely preserving general capabilities and benign compliance\. At test time, POGB\-based Formal Reasoning Harness achieves 91\.80% overall accuracy across four reasoning benchmarks, surpassing all evaluated Direct and CoT baseline configurations except those of Claude Opus 5\. It achieves the highest FOLIO accuracy of 88\.73%, matches the best PrOntoQA result at 100\.00%, and reaches near\-perfect accuracy of 99\.50% on ProofWriter, demonstrating the benefit of proof\-guided reasoning for end\-to\-end accuracy\.

## 2Safety\-Native Architecture

This section summarizes the safety memory inherited from Safin\-1 and describes its integration with REX\-based hazardous\-knowledge disentanglement\. Together, these mechanisms provide architectural support for retaining safety experience and isolating targeted hazardous knowledge during continual safety improvement\.

### 2\.1MARCH: Safety Memory

Safin\-1\.5retains the memory architecture of MARCH\[[57](https://arxiv.org/html/2610.40751#bib.bib45)\]and the persistent Safety State introduced in Safin\-1\[[56](https://arxiv.org/html/2610.40751#bib.bib24)\]\. This interface makes both contextual memory and learned safety specialization selectively accessible within recurrent computation\. We describe one state\-bearing layer below; the same construction applies across recurrent layers\.

##### State anchors\.

Let𝐱t\\mathbf\{x\}\_\{t\}be the normalized token representation and𝐒t∈ℝdv×dk\\mathbf\{S\}\_\{t\}\\in\\mathbb\{R\}^\{d\_\{v\}\\times d\_\{k\}\}the recurrent state, with native read query𝐪t=𝐖q​𝐱t∈ℝdk\\mathbf\{q\}\_\{t\}=\\mathbf\{W\}\_\{q\}\\mathbf\{x\}\_\{t\}\\in\\mathbb\{R\}^\{d\_\{k\}\}\. The base mixer updates𝐒t=F⁡\(𝐒t−1,𝐱t\)\\mathbf\{S\}\_\{t\}=F\(\\mathbf\{S\}\_\{t\-1\},\\mathbf\{x\}\_\{t\}\)continuously, and MARCH checkpoints its state at boundariesbmb\_\{m\}spaced everyCCtext tokens:

𝐀\(m\)=𝐒bm,𝒱t=\{m∣bm<t\}\.\\mathbf\{A\}^\{\(m\)\}=\\mathbf\{S\}\_\{b\_\{m\}\},\\qquad\\mathcal\{V\}\_\{t\}=\\\{m\\mid b\_\{m\}<t\\\}\.\(1\)Each anchor stores a cumulative prefix state rather than an isolated segment\. An occurrence of a shared learned anchor embedding is inserted after each boundary without modifying the recurrence\. At each layer, its normalized representation𝐮m\\mathbf\{u\}\_\{m\}reads the aligned checkpoint as𝐀\(m\)​𝐖q​𝐮m\\mathbf\{A\}^\{\(m\)\}\\mathbf\{W\}\_\{q\}\\mathbf\{u\}\_\{m\}and yields a routing key𝜿m=𝐖κ​𝐮m∈ℝdr\\boldsymbol\{\\kappa\}\_\{m\}=\\mathbf\{W\}\_\{\\kappa\}\\mathbf\{u\}\_\{m\}\\in\\mathbb\{R\}^\{d\_\{r\}\}\. The readout passes through the output projection and residual pathway, making subsequent\-layer anchor representations state\-dependent\.

##### Persistent safety memory\.

The bank additionally contains a learned state𝐏safe∈ℝdv×dk\\mathbf\{P\}\_\{\\mathrm\{safe\}\}\\in\\mathbb\{R\}^\{d\_\{v\}\\times d\_\{k\}\}, indexed bypsafep\_\{\\mathrm\{safe\}\}, with a key constructed through the same anchor\-representation pathway\. The layer\-wise collection of these states forms the Safety State\. Unlike sequence\-derived anchors, it remains available from the first token without consuming input positions\. Safin\-1 learns this collection with token\-level cross\-entropy on harmful requests with safety\-aligned responses and benign requests with helpful responses, while freezing the language\-model backbone\[[56](https://arxiv.org/html/2610.40751#bib.bib24)\]\.

##### Joint routing and readout\.

Let𝝆t=𝐖ρ​𝐱t∈ℝdr\\boldsymbol\{\\rho\}\_\{t\}=\\mathbf\{W\}\_\{\\rho\}\\mathbf\{x\}\_\{t\}\\in\\mathbb\{R\}^\{d\_\{r\}\}be the routing query\. The candidate set is𝒞t=𝒱t∪\{psafe,∅\}\\mathcal\{C\}\_\{t\}=\\mathcal\{V\}\_\{t\}\\cup\\\{p\_\{\\mathrm\{safe\}\},\\varnothing\\\}, with payloads𝐀\(psafe\)=𝐏safe\\mathbf\{A\}^\{\(p\_\{\\mathrm\{safe\}\}\)\}=\\mathbf\{P\}\_\{\\mathrm\{safe\}\}and𝐀\(∅\)=𝟎\\mathbf\{A\}^\{\(\\varnothing\)\}=\\mathbf\{0\}\. The null option allows retrieval to be bypassed\. Candidate scores and probabilities are

st,j\\displaystyle s\_\{t,j\}=\{𝝆t⊤​𝜿j,j≠∅,𝐰∅⊤​𝐱t\+b∅,j=∅,\\displaystyle=\\begin\{cases\}\\boldsymbol\{\\rho\}\_\{t\}^\{\\top\}\\boldsymbol\{\\kappa\}\_\{j\},&j\\neq\\varnothing,\\\\ \\mathbf\{w\}\_\{\\varnothing\}^\{\\top\}\\mathbf\{x\}\_\{t\}\+b\_\{\\varnothing\},&j=\\varnothing,\\end\{cases\}πt,j\\displaystyle\\pi\_\{t,j\}=exp⁡\(st,j\)∑j′∈𝒞texp⁡\(st,j′\)\.\\displaystyle=\\frac\{\\exp\(s\_\{t,j\}\)\}\{\\sum\_\{j^\{\\prime\}\\in\\mathcal\{C\}\_\{t\}\}\\exp\(s\_\{t,j^\{\\prime\}\}\)\}\.\(2\)The router selects memories, while𝐪t\\mathbf\{q\}\_\{t\}reads their matrix\-valued contents\. The retrieved readout is added to the native recurrent path:

𝐨t=𝐒t​𝐪t\+∑j∈𝒞tπt,j​𝐀\(j\)​𝐪t\.\\mathbf\{o\}\_\{t\}=\\mathbf\{S\}\_\{t\}\\mathbf\{q\}\_\{t\}\+\\sum\_\{j\\in\\mathcal\{C\}\_\{t\}\}\\pi\_\{t,j\}\\mathbf\{A\}^\{\(j\)\}\\mathbf\{q\}\_\{t\}\.\(3\)Thus, context anchors and persistent safety memory contribute according to the current token and context, without changing the base recurrent update\. InSafin\-1\.5, this inherited interface supplies the memory foundation alongside REX andReSI; replay and the safety–utility gate in Section[3\.3](https://arxiv.org/html/2610.40751#S3.SS3)complement it during continual safety improvement\.

### 2\.2REX: Hazardous\-Knowledge Disentanglement

Figure 3:Overview of REX\.\(1\) Expert expansion copies and scales the source experts of the base modelBBto form removable experts \(F0F\_\{0\}\), and joint training with selective gradient masking and routing differentiation relocates hazardous knowledge into them \(F1F\_\{1\}\)\. \(2\) Excising the removable experts yieldsA1A\_\{1\}, and a light RMU cleanup yields the public base modelA2A\_\{2\}, while the removable experts and their router rows are kept\. \(3\) Recombining them withA2A\_\{2\}gives the full structureF2F\_\{2\}, on which standard post\-training produces the full modelF3F\_\{3\}for authorized users; excising its removable experts produces the public modelA3A\_\{3\}\.Safety RSI requires that hazardous capabilities, once removed, stay removed as the model keeps being updated, and parameter\-level unlearning has difficulty meeting this requirement because hazardous and general knowledge are stored in the same parameters\. Methods such as RMU\[[20](https://arxiv.org/html/2610.40751#bib.bib6)\]and NPO\[[58](https://arxiv.org/html/2610.40751#bib.bib7)\]modify these shared parameters in place, so more thorough removal costs more general capability\. More importantly, such removal suppresses the expression of the knowledge rather than taking it out of the model, and subsequent fine\-tuning, even on unrelated data, can bring it back\[[6](https://arxiv.org/html/2610.40751#bib.bib15)\]\. In a one\-off release this is already a risk; in Safety RSI, where the model is updated round after round, every update is another chance for the knowledge to return\. REX\[[16](https://arxiv.org/html/2610.40751#bib.bib46)\]addresses this problem through where the knowledge is stored\. The feed\-forward parameters of a Mixture\-of\-Experts \(MoE\) model are partitioned into independently addressable experts, the expert set can be expanded, and selected experts can be deleted at deployment\. Once hazardous knowledge is concentrated in a set of removable experts, removing it no longer depends on in\-place edits to shared parameters and becomes a structural operation\.

REX relocates hazardous knowledge out of the original experts and into newly added removable experts through three components \(Figure[3](https://arxiv.org/html/2610.40751#S2.F3)\)\. The first component,*expert expansion*, initializes the removable experts\. On the training corpora, we count how often each expertiiis selected into the top\-KKon target data𝒟harm\\mathcal\{D\}\_\{\\mathrm\{harm\}\}and on general data𝒟gen\\mathcal\{D\}\_\{\\mathrm\{gen\}\}, and compute the differenceΔi=fiharm−figen\\Delta\_\{i\}=f\_\{i\}^\{\\mathrm\{harm\}\}\-\{f\_\{i\}^\{\\mathrm\{gen\}\}\}\. In each layer, the experts with the largestΔi\\Delta\_\{i\}serve as source experts\. Their parameters and router rows are copied to form the removable experts, and the source experts are scaled by a fixed factorγ\\gamma, which weakens the hazardous knowledge they hold while preserving most of their general computation\. The second component,*selective gradient masking*, determines where the updates from each data source can be written\. LetΘrem\\Theta\_\{\\mathrm\{rem\}\}denote the removable experts,Θorig\\Theta\_\{\\mathrm\{orig\}\}the original experts, andΘrouter\\Theta\_\{\\mathrm\{router\}\}all router rows; the updated parameters are

\{Θrem∪Θrouteron​𝒟harm,Θorig∪Θrouteron​𝒟gen\.\\begin\{cases\}\{\\Theta\_\{\\mathrm\{rem\}\}\}\\cup\{\\Theta\_\{\\mathrm\{router\}\}\}&\\text\{on \}\\mathcal\{D\}\_\{\\mathrm\{harm\}\},\\\\ \{\\Theta\_\{\\mathrm\{orig\}\}\}\\cup\{\\Theta\_\{\\mathrm\{router\}\}\}&\\text\{on \}\{\\mathcal\{D\}\_\{\\mathrm\{gen\}\}\}\.\\end\{cases\}\(4\)On general data, a pre\-top\-KKactivation mask additionally removes the logits of the removable experts before selection, so that every general token is dispatched without them\. The original experts must therefore carry general capability on their own, and the hazardous knowledge they already hold receives no training signal and fades, which turns catastrophic forgetting during continued training into directed forgetting\. The third component,*routing differentiation*, shapes the router with two losses\. A mass loss keeps the routing mass assigned to the removable experts above a floor on target tokens and below a ceiling on general tokens\. A rank loss keeps the largest removable\-expert logit on general tokens a margin below the top\-KKboundary of the original experts, so that the unmasked router at inference also leaves general tokens to the original experts\. The relocation objective is

ℒREX=ℒLM\+λ1​ℒmass\+λ2​ℒrank,\\mathcal\{L\}\_\{\\mathrm\{REX\}\}=\\mathcal\{L\}\_\{\\mathrm\{LM\}\}\+\\lambda\_\{1\}\\mathcal\{L\}\_\{\\mathrm\{mass\}\}\+\\lambda\_\{2\}\\mathcal\{L\}\_\{\\mathrm\{rank\}\},\(5\)whereλ1\\lambda\_\{1\}andλ2\\lambda\_\{2\}weight the mass and rank losses, respectively, and the language\-modeling loss is back\-propagated under the masking rules of Eq\. \([4](https://arxiv.org/html/2610.40751#S2.E4)\)\. During relocation, attention, embeddings, normalization layers, shared experts, and the LM head stay frozen, and only the routed experts and the router are trained\.

After relocation, REX excises the removable experts together with their router rows and applies a light RMU cleanup to the retained parameters to remove residual target knowledge, which yields the public base model; the excised experts are kept by the developer\. The value of this design for Safety RSI lies in the updates that follow\. An update is not applied to the public model directly\. Instead, the kept removable experts are recombined with the cleaned parameters into the full structure, training proceeds on the full structure, and the removable experts are excised again at deployment\. During the update, the router continues to send target\-related tokens to the removable experts, so these updates leave with the experts at deployment, while growth in general capability is written to the retained parameters and released with the public model\. The developer therefore always holds two forms of the model: a full model for authorized users that retains the hazardous capability, and a public model that contains no parameters of the removable experts\. What to train and what to release thus become two independent decisions, which is exactly the interface that theReSIloop needs when it accepts an update in each round \(Section[3\.3](https://arxiv.org/html/2610.40751#S3.SS3)\)\. In the experiments, we denote the original model byBB, the cleaned public base model byA2A\_\{2\}, the recombined full model after standard post\-training byF3F\_\{3\}, and its excised counterpart byA3A\_\{3\}\.

Safin\-1\.5applies REX to Safin\-1\-35B\-A3B without interfering with the memory mechanism of MARCH\. The memory\-related parameters introduced by MARCH belong to the frozen shared parameters during both relocation and cleanup, so REX changes only the routed experts and the router\. Routing statistics, training\-token counts, and RMU activations are computed on text positions, excluding the anchor positions that MARCH inserts into the sequence\. Unlike the original REX, which handles one domain at a time,Safin\-1\.5uses a single set of removable experts for both Bio and Cyber\. Expert expansion selects 8 source experts per layer for each domain by differential activation, takes their union, and completes it to 16 per layer by the joint differential across the two domains, expanding each layer from 256 to 272 experts withγ=0\.3\\gamma=0\.3\. Relocation uses about 40M tokens of mixed target data, with Bio and Cyber at roughly 4:1, and about 27M tokens of general data\. The residual cleanup uses a forget budget of 32M tokens and updates only the routed\-expert and shared\-expert MLPs in layers 7–9, and standard post\-training on the recombined model uses 250M tokens\. A single excision then removes the target knowledge of both domains\.

## 3ReSI: Recursive Safety Improvement

ReSI\[[62](https://arxiv.org/html/2610.40751#bib.bib37)\]builds on the safety architecture described in Section[2](https://arxiv.org/html/2610.40751#S2)to implement the risk discovery, evaluation, and repair loop of Safety RSI\. In each round,ReSIapplies diverse red\-teaming methods to identify vulnerabilities in the current target model, develops a training recipe through automated research, and promotes the eligible update with the largest safety gain as the next target model, where eligibility requires passing a Pareto gate on safety gain, benign compliance, and instruction following \(Figure[4](https://arxiv.org/html/2610.40751#S3.F4)\)\. Through successive rounds, the loop pursues the two goals identified by R2AI\[[42](https://arxiv.org/html/2610.40751#bib.bib61),[43](https://arxiv.org/html/2610.40751#bib.bib31)\]:*resistance*to known threats and*resilience*to unforeseen risks\. Section[3\.1](https://arxiv.org/html/2610.40751#S3.SS1)formulates the recursive update, Section[3\.2](https://arxiv.org/html/2610.40751#S3.SS2)describes the three stages of a round and the joint recipe search space, and Section[3\.3](https://arxiv.org/html/2610.40751#S3.SS3)describes how the loop operates on the safety architecture\.

![Refer to caption](https://arxiv.org/html/2610.40751v1/imgs/resi_framework.png)Figure 4:The three\-stageReSIframework\.In each round,ReSIapplies red\-teaming methods to identify vulnerabilities in the current target modelMrM\_\{r\}, develops training recipes through automated research, and promotes the eligible update with the largest safety gain asMr\+1M\_\{r\+1\}, the target for the next round\. Stage 1 collects successful attacks againstMrM\_\{r\}\(Section[3\.2\.1](https://arxiv.org/html/2610.40751#S3.SS2.SSS1)\)\. Stage 2 screens attack sources and alignment methods through low\-budget pilot trials and shortlists the most promising recipes \(Section[3\.2\.3](https://arxiv.org/html/2610.40751#S3.SS2.SSS3)\)\. Stage 3 conducts full\-scale training and feedback\-guided refinement, then selects the eligible checkpoint with the largest safety gain \(Section[3\.2\.4](https://arxiv.org/html/2610.40751#S3.SS2.SSS4)\)\.### 3\.1Recursive Formulation

ReSIorganizes safety improvement as a recursive loop over target models\. Specifically,ReSIformulates the safety update within a round as an auto\-research problem: givenMrM\_\{r\}and the attacks that succeed against it,ReSIsearches for a training recipe that strengthens the model’s resistance to the exposed attacks while preserving existing safety behavior and general capabilities\. Starting from an initial modelM0M\_\{0\}, roundrrtakes the current target modelMrM\_\{r\}and produces the next target

Mr\+1=\{Mrωr⋆,ℰr≠∅,Mr,ℰr=∅,ωr⋆∈arg​maxω∈ℰr⁡gr​\(ω\),M\_\{r\+1\}=\\begin\{cases\}M\_\{r\}^\{\\omega\_\{r\}^\{\\star\}\},&\\mathcal\{E\}\_\{r\}\\neq\\varnothing,\\\\\[2\.0pt\] M\_\{r\},&\\mathcal\{E\}\_\{r\}=\\varnothing,\\end\{cases\}\\qquad\\omega\_\{r\}^\{\\star\}\\in\\operatorname\*\{arg\\,max\}\_\{\\omega\\in\\mathcal\{E\}\_\{r\}\}g\_\{r\}\(\\omega\),\(6\)whereMrωM\_\{r\}^\{\\omega\}denotes the checkpoint that recipeω\\omegaproduces in roundrrfrom its specified starting checkpoint,gr​\(ω\)g\_\{r\}\(\\omega\)is its safety gain \(Eq\. \([9](https://arxiv.org/html/2610.40751#S3.E9)\)\), andℰr\\mathcal\{E\}\_\{r\}is the set of recipes with completed full\-scale trials, including the refinement trials of Section[3\.2\.4](https://arxiv.org/html/2610.40751#S3.SS2.SSS4), that pass the Pareto gate \(Eq\. \([10](https://arxiv.org/html/2610.40751#S3.E10)\)\)\. As a result, an accepted update becomes the target of the next round; if no recipe passes the gate,ReSIretainsMrM\_\{r\}and terminates, so that updates failing the gate never propagate to later rounds\. We use*recursive*in a bounded, operational sense: the search procedure and the Pareto gate remain fixed across rounds, while the target model and the attacks collected against it change\.

### 3\.2The Three\-Stage Round

Each round ofReSIproceeds in three stages over a joint recipe search space \(Figure[4](https://arxiv.org/html/2610.40751#S3.F4)\)\. Stage 1 collects successful attacks againstMrM\_\{r\}\(Section[3\.2\.1](https://arxiv.org/html/2610.40751#S3.SS2.SSS1)\), which define the attack data of the recipe search space \(Section[3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2)\)\. Within this space, Stage 2 screens attack sources and alignment methods through pilot trials \(Section[3\.2\.3](https://arxiv.org/html/2610.40751#S3.SS2.SSS3)\), and Stage 3 refines full\-scale recipes and selects the model update under the Pareto gate \(Section[3\.2\.4](https://arxiv.org/html/2610.40751#S3.SS2.SSS4)\)\.

#### 3\.2\.1Stage 1: Red\-Teaming Assessment

Stage 1 identifies the vulnerabilities of the current target model and converts them into safety training signals\. Let𝒳r\\mathcal\{X\}\_\{r\}denote a safety data pool of requests that represent potential deployment risks, and let𝒵r\\mathcal\{Z\}\_\{r\}denote the set of available red\-teaming methods\. Each methodz∈𝒵rz\\in\\mathcal\{Z\}\_\{r\}draws requests from𝒳r\\mathcal\{X\}\_\{r\}to construct attacks againstMrM\_\{r\}, potentially adapting them based on the model’s responses, and produces input–response pairsz⁡\(Mr,𝒳r\)z\(M\_\{r\},\\mathcal\{X\}\_\{r\}\)\.ReSIaggregates these records and retains those in which the attack elicits an unsafe response:

𝒟ratk=\{\(x,y\)∈⋃z∈𝒵rz⁡\(Mr,𝒳r\)\|Unsafe⁡\(x,y\)=1\},\\mathcal\{D\}\_\{r\}^\{\\mathrm\{atk\}\}=\\Bigl\\\{\(x,y\)\\in\\textstyle\\bigcup\_\{z\\in\\mathcal\{Z\}\_\{r\}\}z\(M\_\{r\},\\mathcal\{X\}\_\{r\}\)\\;\\Big\|\\;\\operatorname\{Unsafe\}\(x,y\)=1\\Bigr\\\},\(7\)wherexxis an attack input,yyis the corresponding response fromMrM\_\{r\}, andUnsafe⁡\(x,y\)\\operatorname\{Unsafe\}\(x,y\)indicates a safety violation;𝒟r,zatk\\mathcal\{D\}\_\{r,z\}^\{\\mathrm\{atk\}\}denotes the subset contributed by methodzz\. Since the attack dataset is re\-collected for each target model, it captures the vulnerabilities of the current checkpoint, including those introduced by earlier updates\. Moreover, the safety data pool and the set of red\-teaming methods are both extensible, so that new deployment risks and new red\-teaming methods can enter the loop as they emerge\.

#### 3\.2\.2Joint Recipe Search Space

Following Stage 1,ReSIsearches over a joint recipe spaceΩr\\Omega\_\{r\}of compatible combinations of attack data, alignment methods, training data mixtures, and hyperparameters\. A candidate recipe is represented as

ω=\(𝜶,a,𝝀,𝐡\)∈Ωr,\\omega=\(\\boldsymbol\{\\alpha\},a,\\boldsymbol\{\\lambda\},\\mathbf\{h\}\)\\in\\Omega\_\{r\},\(8\)where𝜶\\boldsymbol\{\\alpha\},aa,𝝀\\boldsymbol\{\\lambda\}, and𝐡\\mathbf\{h\}specify the attack data, alignment method, training data mixture, and hyperparameters, respectively\.

Attack data\.The attack\-data dimension𝜶\\boldsymbol\{\\alpha\}controls the contribution of each red\-teaming source\. For each methodzz,αz∈\[0,1\]\\alpha\_\{z\}\\in\[0,1\]selects a fraction of𝒟r,zatk\\mathcal\{D\}\_\{r,z\}^\{\\mathrm\{atk\}\}, so that a recipe can use a single source, combine all available attacks, or reweight the sources\.

Alignment methods\.The alignment methodaais drawn from an extensible poolℳalign\\mathcal\{M\}\_\{\\mathrm\{align\}\}and converts the selected attacks into training examples\. Representative methods in this pool and their design rationales are outlined below\. A3\[[55](https://arxiv.org/html/2610.40751#bib.bib56)\]pairs harmful requests with benign counterparts that share similar patterns and uses both for supervised fine\-tuning \(SFT\), encouraging the model to learn safety distinctions that generalize beyond specific adversarial patterns\. SInternal\[[59](https://arxiv.org/html/2610.40751#bib.bib57)\]fine\-tunes the model to reproduce an expert’s critique of its own response against safety specifications and then predict a safety judgment, strengthening its understanding of the specifications\. AlphaAlign\[[60](https://arxiv.org/html/2610.40751#bib.bib58)\]applies reinforcement learning with a reward that requires safe responses to harmful requests and safe, fully compliant responses to benign requests of similar surface form, so that unnecessary refusals receive no reward\.

Training data mixtures\.The mixture𝝀=\(λcur,λrep,λgen\)\\boldsymbol\{\\lambda\}=\(\\lambda\_\{\\mathrm\{cur\}\},\\lambda\_\{\\mathrm\{rep\}\},\\lambda\_\{\\mathrm\{gen\}\}\)balances learning from newly identified vulnerabilities with retaining existing safety behavior and general capabilities\. Specifically, the three weights of𝝀\\boldsymbol\{\\lambda\}are non\-negative, sum to one, and give the fractions of current safety examples, replay examples from earlier safety training, and general\-task examples\.

Hyperparameters\.The configuration𝐡∈ℋ⁡\(a\)\\mathbf\{h\}\\in\\mathcal\{H\}\(a\), drawn from the training settings available for methodaa, covers the learning rate, batch size, training budget, checkpoint frequency, the evaluated checkpoint step, adaptation settings such as LoRA\[[11](https://arxiv.org/html/2610.40751#bib.bib60)\], and generation parameters for reinforcement learning\.

#### 3\.2\.3Stage 2: Pilot Screening

Pilot screening identifies promising attack sources and alignment methods through low\-budget trials\. For each sourcezzproviding at leastnpilotn\_\{\\mathrm\{pilot\}\}successful attacks and each methoda∈ℳaligna\\in\\mathcal\{M\}\_\{\\mathrm\{align\}\},ReSItrains a pilot fromMrM\_\{r\}with methodaaonnpilotn\_\{\\mathrm\{pilot\}\}attacks fromzz, using only current safety data \(𝝀\(0\)=\(1,0,0\)\\boldsymbol\{\\lambda\}^\{\(0\)\}=\(1,0,0\)\), the default hyperparameters𝐡a\(0\)\\mathbf\{h\}\_\{a\}^\{\(0\)\}ofaa, and a limited training budget\. In the first round, successful attacks from the original safety data pool form a shared base that each pilot uses in addition to itsnpilotn\_\{\\mathrm\{pilot\}\}source\-specific attacks\. After training, each recipe is evaluated on a held\-out validation set𝒟rval\\mathcal\{D\}\_\{r\}^\{\\mathrm\{val\}\}drawn from the original safety data pool\. However, whenMrM\_\{r\}already has a low attack success rate \(ASR\) on that pool,𝒟rval\\mathcal\{D\}\_\{r\}^\{\\mathrm\{val\}\}is instead drawn from a more challenging attack set, and a candidate must also not raise ASR on the original pool by more than a toleranceδ\\deltarelative toMrM\_\{r\}\. The safety gain ofω\\omegais

gr​\(ω\)=ASR⁡\(Mr;𝒟rval\)−ASR⁡\(Mrω;𝒟rval\)\.g\_\{r\}\(\\omega\)=\\operatorname\{ASR\}\(M\_\{r\};\\mathcal\{D\}\_\{r\}^\{\\mathrm\{val\}\}\)\-\\operatorname\{ASR\}\(M\_\{r\}^\{\\omega\};\\mathcal\{D\}\_\{r\}^\{\\mathrm\{val\}\}\)\.\(9\)Although equal sample counts keep pilots comparable, they can understate a source that provides many more attacks thannpilotn\_\{\\mathrm\{pilot\}\}\. Therefore, for recipes with modest pilot safety gains but substantially more available attacks,ReSIruns a conditional scaling probe, retraining the same recipe fromMrM\_\{r\}withnpilot<nscale≤\|𝒟r,zatk\|n\_\{\\mathrm\{pilot\}\}<n\_\{\\mathrm\{scale\}\}\\leq\|\\mathcal\{D\}\_\{r,z\}^\{\\mathrm\{atk\}\}\|attacks and ranking it alongside the initial pilots\. Finally,ReSIshortlists up toKpilotK\_\{\\mathrm\{pilot\}\}recipes with the largest positive safety gains,𝒬r=TopKgr⁡\{ω:gr​\(ω\)\>0\}\\mathcal\{Q\}\_\{r\}=\\operatorname\{TopK\}\_\{g\_\{r\}\}\\\{\\omega:g\_\{r\}\(\\omega\)\>0\\\}; if𝒬r=∅\\mathcal\{Q\}\_\{r\}=\\varnothing, it retainsMrM\_\{r\}and terminates\.

#### 3\.2\.4Stage 3: Full\-Scale Refinement and Model Update

Given the shortlisted recipes𝒬r\\mathcal\{Q\}\_\{r\},ReSIconducts full\-scale trials, refines each recipe based on feedback from the Pareto gate, and selects the model update\. Specifically, each full\-scale trial starts fromMrM\_\{r\}, expands the training data to all successful attacks from the source of the shortlisted recipe, and lifts the pilot budget cap, keeping𝝀\(0\)\\boldsymbol\{\\lambda\}^\{\(0\)\}and𝐡a\(0\)\\mathbf\{h\}\_\{a\}^\{\(0\)\}\. The trial saves checkpoints at the frequency specified in𝐡\\mathbf\{h\}, and each saved checkpoint is evaluated as a candidate update\.

Pareto gate\.The Pareto gate requires a safety improvement over the current model while keeping benign compliance and instruction following within a tolerance of the initial model\. A recipe passes the gate if

𝒢r\(ω\)=1⟺\{gr​\(ω\)\>0,BC⁡\(Mrω\)≥BC⁡\(M0\)−ϵ,IF⁡\(Mrω\)≥IF⁡\(M0\)−ϵ,\\mathcal\{G\}\_\{r\}\(\\omega\)=1\\quad\\Longleftrightarrow\\quad\\begin\{cases\}g\_\{r\}\(\\omega\)\>0,\\\\ \\mathrm\{BC\}\(M\_\{r\}^\{\\omega\}\)\\geq\\mathrm\{BC\}\(M\_\{0\}\)\-\\epsilon,\\\\ \\mathrm\{IF\}\(M\_\{r\}^\{\\omega\}\)\\geq\\mathrm\{IF\}\(M\_\{0\}\)\-\\epsilon,\\end\{cases\}\(10\)whereBC\\mathrm\{BC\}denotes benign compliance,IF\\mathrm\{IF\}denotes instruction following, andϵ\\epsilonis the retention tolerance\. Here, the benign\-compliance condition limits over\-refusal, and the instruction\-following condition limits the loss of general capabilities\. Moreover, anchoring both retention thresholds toM0M\_\{0\}rather than toMrM\_\{r\}prevents small per\-round losses within the tolerance from accumulating across rounds\.

Feedback\-guided refinement\.ReSIrevises a recipe according to its Pareto\-gate result, allowing at mostNrefineN\_\{\\mathrm\{refine\}\}refinement trials beyond the initial trial and stopping earlier when no executable revision remains\.

- •S1\. Attack\-source composition\.For limited safety gains, expand𝜶\\boldsymbol\{\\alpha\}to combine successful attacks from additional promising sources\.
- •S2\. Harmful–benign pairing\.For a benign\-compliance violation, construct A3\-style benign counterparts that preserve the attack patterns of harmful examples while replacing their harmful content, and adjust the harmful–benign balance\.
- •S3\. Utility preservation\.For an instruction\-following violation, increase general\-task replay through𝝀\\boldsymbol\{\\lambda\}, or reduce the learning rate or the number of updates through𝐡\\mathbf\{h\}\.
- •S4\. Post\-SFT safety GRPO\.For an eligible SFT recipe, retain it as a candidate and continue training from its checkpoint with AlphaAlign\-based safety Group Relative Policy Optimization \(GRPO\)\[[40](https://arxiv.org/html/2610.40751#bib.bib65)\]and DAPO\-style optimization\[[52](https://arxiv.org/html/2610.40751#bib.bib59)\]; this transition resets the refinement counter to zero, allowing up toNrefineN\_\{\\mathrm\{refine\}\}further refinement trials\.

In practice, each revision specifies its starting checkpoint, while all trials share the same validation sets and gate thresholds\. Revisions restart fromMrM\_\{r\}by default; a revision may instead continue from the evaluated checkpoint with a reduced training budget recorded in𝐡\\mathbf\{h\}, and revisions within an S4 continuation restart from the same SFT checkpoint\.

Final selection and stopping\.After all shortlisted recipes and their refinements have been evaluated,ReSIupdates the target model according to Eq\. \([6](https://arxiv.org/html/2610.40751#S3.E6)\)\.ReSIpromotes the eligible checkpoint with the largest safety gain, or retainsMrM\_\{r\}and terminates when no recipe is eligible; the loop also terminates at the configured round limit\.

### 3\.3ReSIon the Safety Architecture

ReSIoperates on the safety architecture of Section[2](https://arxiv.org/html/2610.40751#S2)without changing the three stages of a round or the Pareto gate: hazardous\-knowledge disentanglement determines which model is trained and which is evaluated, safety memory supports the retention and reuse of safety experience across rounds, and formal assurance can check specified claims about the models that the loop promotes\.

Hazardous\-knowledge disentanglement\.On the disentangled architecture,ReSItrains the full model but red\-teams, validates, and gates its excised counterpart; the full checkpoint of an accepted update becomes the starting point of the next round, and its excised counterpart is the deployed model\. Specifically, REX\[[16](https://arxiv.org/html/2610.40751#bib.bib46)\]relocates targeted hazardous knowledge into removable experts that are excised for deployment\. Therefore, in each round, a recipe updates the full model with all experts, so that the router and the removable experts keep the roles assigned during relocation\. In contrast, training without the removable experts could push hazardous content contained in safety data into shared parameters, whereas evaluating with them would assess a model that is never deployed\. Additionally,ReSImeasures hazardous\-knowledge accuracy for each trial on the excised checkpoint, so that any reintroduction of removed knowledge is visible when candidates are compared\.

Safety memory\.Safety memory keeps safety experience from earlier rounds available to later updates\. On the model side, MARCH\[[57](https://arxiv.org/html/2610.40751#bib.bib45)\]can provide a persistent interface through which this experience is stored and selectively invoked\. On the training side, the replay weightλrep\\lambda\_\{\\mathrm\{rep\}\}complements this interface by keeping examples from earlier safety training in the training data to reduce forgetting of earlier repairs\.

Formal assurance\.Formal assurance can complement the empirical evaluation of each model thatReSIpromotes\.ReSIprovides empirical evidence that an update reduces ASRs on the evaluated attacks, and specified claims about each promoted model can then be checked by the formal assurance harness in Section[4](https://arxiv.org/html/2610.40751#S4)under explicit assumptions\.

## 4POGB: Formal Reasoning Harness

Building on the model trained through the safety improvement process in Section[3](https://arxiv.org/html/2610.40751#S3), we introduce POGB as an inference\-time harness to extend its capabilities to formal reasoning, as illustrated in Figure[5](https://arxiv.org/html/2610.40751#S4.F5)\. An inference\-time switch controls whether POGB is invoked; it is enabled only for logical reasoning tasks that ask whether a claim follows from given premises\. When disabled, the model follows its standard inference procedure\. When enabled, PoGB begins with a grounding autoformalization step, in which an LLM translates the problem expressed in NL into formal representations while maintaining a grounding table that records the type and associated NL information for each formal element\. This table then serves as a*proof\-time interface*for*proof\-obligation\-guided search*\. During this search, type information constrains which instantiations are admissible, while NL information guides the identification of semantic bridges via an LLM\-basedGate\\operatorname\{Gate\}when symbolic reasoning encounters an unresolved proof obligation\. This design keeps all logical reasoning under the solver’s control while restricting the LLM’s role to autoformalization and the evaluation of candidate semantic bridges\.

![Refer to caption](https://arxiv.org/html/2610.40751v1/imgs/POGB.png)Figure 5:Illustration of the proposed approach\. Variables in the atomic formulas of the grounding table are replaced with argument placeholders\{ai\}\\\{a\_\{i\}\\\}, which are highlighted in blue and subsequently instantiated with type\-compatible constants\.### 4\.1Problem Formulation

LetX=\(ℙ,q\)X=\(\\mathbb\{P\},q\)denote a problem comprising a set of NL premisesℙ=\{pi\}i=1n\\mathbb\{P\}=\\\{p\_\{i\}\\\}\_\{i=1\}^\{n\}and an NL queryqq\. We use a grounding autoformalizationA​F\{AF\}to mapXXtoA​F​\(X\)=\(𝒫,𝔮,𝒯\)\{AF\}\(X\)=\(\\mathcal\{P\},\\mathfrak\{q\},\\mathcal\{T\}\), thereby yielding formal representations that are explicitly associated with their NL semantics inXX\. Here,𝒫=\{𝔭i\}i=1n\\mathcal\{P\}=\\\{\\mathfrak\{p\}\_\{i\}\\\}\_\{i=1\}^\{n\}is the set of formalized premises, where𝔭i\\mathfrak\{p\}\_\{i\}denotes theiith formalized premise;𝔮\\mathfrak\{q\}is the formalized query; and𝒯\\mathcal\{T\}is a grounding table that records the NL semantic grounding of every formal element \(see Section[4\.2](https://arxiv.org/html/2610.40751#S4.SS2)for details\)\. We adopt first\-order logic \(FOL\) as the target formal language\.

Consider two proof goals corresponding to the query and its negation:𝔮\\mathfrak\{q\}and¬𝔮\\neg\\mathfrak\{q\}\. For each goal𝔤∈\{𝔮,¬𝔮\}\\mathfrak\{g\}\\in\\\{\\mathfrak\{q\},\\neg\\mathfrak\{q\}\\\}, the symbolic solver performs a proof search and identifies unresolved proof obligations resulting from missing semantic relations\. Let𝒮\\mathcal\{S\}denote the symbolic solver\. Our objective is to find a*reasonable*bridge setℬ\\mathcal\{B\}that enables the proof to be completed:

𝒮⁡\(𝒫∪ℬ,𝔤\)=Proved∧Gate⁡\(ℬ,𝒯\)=Accepted\.\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{g\}\)=\\textsc\{Proved\}\\quad\\land\\quad\\operatorname\{Gate\}\(\\mathcal\{B\},\\mathcal\{T\}\)=\\textsc\{Accepted\}\.\(11\)Here,ℬ=\{𝔟j\}j=1m\\mathcal\{B\}=\\\{\\mathfrak\{b\}\_\{j\}\\\}\_\{j=1\}^\{m\}, where each𝔟j\\mathfrak\{b\}\_\{j\}is a semantic bridge that explicitly encodes an entailment relation supported by the NL semantics but not represented in the symbolic ontology\. The LLM\-basedGate\\operatorname\{Gate\}evaluates only whether these candidate semantic bridges are reasonable given the grounding table𝒯\\mathcal\{T\}; it does not perform proof search, conduct intermediate reasoning, or repair failures in response to solver feedback\. The final decision is determined by the proof outcomes for the two goals:

Decide⁡\(X\)=\{Entailed,\(𝒮⁡\(𝒫∪ℬ,𝔮\),𝒮⁡\(𝒫∪ℬ,¬𝔮\)\)=\(Proved,Failed\),Contradicted,\(𝒮⁡\(𝒫∪ℬ,𝔮\),𝒮⁡\(𝒫∪ℬ,¬𝔮\)\)=\(Failed,Proved\),Unknown,\(𝒮⁡\(𝒫∪ℬ,𝔮\),𝒮⁡\(𝒫∪ℬ,¬𝔮\)\)=\(Failed,Failed\),Conflicted,\(𝒮⁡\(𝒫∪ℬ,𝔮\),𝒮⁡\(𝒫∪ℬ,¬𝔮\)\)=\(Proved,Proved\)\.\\operatorname\{Decide\}\(X\)=\\begin\{cases\}\\textsc\{Entailed\},&\\bigl\(\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{q\}\),\\ \\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\neg\\mathfrak\{q\}\)\\bigr\)=\\bigl\(\\textsc\{Proved\},\\ \\textsc\{Failed\}\\bigr\),\\\\ \\textsc\{Contradicted\},&\\bigl\(\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{q\}\),\\ \\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\neg\\mathfrak\{q\}\)\\bigr\)=\\bigl\(\\textsc\{Failed\},\\ \\textsc\{Proved\}\\bigr\),\\\\ \\textsc\{Unknown\},&\\bigl\(\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{q\}\),\\ \\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\neg\\mathfrak\{q\}\)\\bigr\)=\\bigl\(\\textsc\{Failed\},\\ \\textsc\{Failed\}\\bigr\),\\\\ \\textsc\{Conflicted\},&\\bigl\(\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{q\}\),\\ \\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\neg\\mathfrak\{q\}\)\\bigr\)=\\bigl\(\\textsc\{Proved\},\\ \\textsc\{Proved\}\\bigr\)\.\\end\{cases\}

### 4\.2The Grounding Table as a Proof\-Time Interface

As discussed in Section[1](https://arxiv.org/html/2610.40751#S1), even when individual NL statements are faithfully formalized, their semantically related expressions may still be mapped to symbolically unrelated predicates\. To recover the semantic relations between such predicates during proof search, we maintain two complementary kinds of information for every formal element\. Let𝔢\\mathfrak\{e\}denote a formal element occurring in𝒫\\mathcal\{P\}or𝔮\\mathfrak\{q\}, including a constant, a variable, or an atomic formula\. For each𝔢\\mathfrak\{e\}, the grounding table𝒯\\mathcal\{T\}records both type information,type𝒯⁡\(𝔢\)\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\), and NL information,NL𝒯⁡\(𝔢\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\), thereby*providing an interface for proof\-time inference*\.

Inspired by type systems\[[4](https://arxiv.org/html/2610.40751#bib.bib19)\],type𝒯⁡\(𝔢\)\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)retains a coarse\-grained semantic category assigned to𝔢\\mathfrak\{e\}by the LLM\. This category constrains which instantiations are admissible, thereby narrowing the search space for candidate semantic bridges\. For instance, in the running example in Appendix[A\.1](https://arxiv.org/html/2610.40751#A1.SS1), a variable of type𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}can be instantiated withhh\(Harry\) but not withww\(*Walden*\)\. By contrast,NL𝒯⁡\(𝔢\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)retains the finer\-grained NL semantics of𝔢\\mathfrak\{e\}by storing referring expressions \(e\.g\., “Harry,” “*Walden*,” “a person,” and “a book”\) and predicate meanings \(e\.g\., “\{a1\}\\\{a\_\{1\}\\\}reads\{a2\}\\\{a\_\{2\}\\\}”\)\. When exact symbolic matching fails, this information guides the search for plausible semantic bridges between*type\-compatible*candidates, such as the bridge between𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\mathsf\{Smarter\}\(h\)and𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\\mathsf\{SmarterThanBefore\}\(h\)\. We next show how this interface supports*proof\-obligation\-guided search*\.

### 4\.3Proof\-Obligation\-Guided Search

We propose a proof\-search method controlled by a symbolic solver and guided by proof obligations, as described in Algorithms[1](https://arxiv.org/html/2610.40751#alg1)and[2](https://arxiv.org/html/2610.40751#alg2)\. Algorithm[1](https://arxiv.org/html/2610.40751#alg1)recursively decomposes each obligation through symbolic reasoning\. When symbolic reasoning alone is insufficient to discharge an obligation, Algorithm[1](https://arxiv.org/html/2610.40751#alg1)invokes Algorithm[2](https://arxiv.org/html/2610.40751#alg2)to identify local semantic bridges\. Algorithm[2](https://arxiv.org/html/2610.40751#alg2)then returns the identified bridges together with the residual obligations required to establish each bridge, after which Algorithm[1](https://arxiv.org/html/2610.40751#alg1)recursively discharges these residual obligations\. A running example is presented in Appendix[A\.1](https://arxiv.org/html/2610.40751#A1.SS1)\.

Algorithm 1Proof\-obligation\-guided search1:A set of formalized premises

𝒫\\mathcal\{P\}, a symbolic solver

𝒮\\mathcal\{S\}, a proof obligation

ϕ\\phi, a set of ancestor obligations

𝒜\\mathcal\{A\}, and a grounding table

𝒯\\mathcal\{T\}\.

2:A set of accepted bridges sufficient to prove

ϕ\\phifrom

𝒫\\mathcal\{P\}, orFailedif the search fails\.

3:functionProve\(

ϕ,𝒜,𝒯\\phi,\\mathcal\{A\},\\mathcal\{T\}\)

4:if

𝒮⁡\(𝒫,ϕ\)=Proved\\mathcal\{S\}\(\\mathcal\{P\},\\phi\)=\\textsc\{Proved\}then⊳\\trianglerightDischargeϕ\\phidirectly with the symbolic solver

5:return

∅\\varnothing
6:

ϕ←Normalize​\(ϕ\)\\phi\\leftarrow\\textsc\{Normalize\}\(\\phi\)⊳\\trianglerightRewriteϕ\\phiin canonical form

7:if

Cyclic​\(ϕ,𝒜\)\\textsc\{Cyclic\}\(\\phi,\\mathcal\{A\}\)then⊳\\trianglerightReject circular reasoning

8:returnFailed

9:

𝒜′←𝒜∪\{ϕ\}\\mathcal\{A\}^\{\\prime\}\\leftarrow\\mathcal\{A\}\\cup\\\{\\phi\\\}⊳\\trianglerightRecord the current proof obligation to check the circular reasoning

10:if

ϕ=∃x\.ψ\\phi=\\exists x\.\\,\\psithen⊳\\trianglerightBranch over type\-compatible instantiations ofxx

11:returnany successful result of

Prove​\(ψ′,𝒜′,𝒯\)\\textsc\{Prove\}\(\\psi^\{\\prime\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)with

ψ′∈Inst​\(ψ,𝒯\)\\psi^\{\\prime\}\\in\\textsc\{Inst\}\(\\psi,\\mathcal\{T\}\)
12:elseif

ϕ=∀x\.ψ\\phi=\\forall x\.\\,\\psithen⊳\\trianglerightIntroduce a fresh constantcfresh\{c\_\{\\mathrm\{fresh\}\}\}and proveψ\\psiafter mapping variablexxtocfresh\{c\_\{\\mathrm\{fresh\}\}\}

13:return

Prove\(ψ\[x↦cfresh\],𝒜′,𝒯∪\{\(cfresh,type𝒯\(x\),NL𝒯\(x\)\)\}\)\\textsc\{Prove\}\(\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\],\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\\cup\\\{\(\{c\_\{\\mathrm\{fresh\}\}\},\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(x\),\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(x\)\)\\\}\)
14:elseif

ϕ=ϕ1∧ϕ2\\phi=\\phi\_\{1\}\\land\\phi\_\{2\}then⊳\\trianglerightDischarge both sub\-obligations

15:return

Prove​\(ϕ1,𝒜′,𝒯\)∪Prove​\(ϕ2,𝒜′,𝒯\)\\textsc\{Prove\}\(\\phi\_\{1\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)\\cup\\textsc\{Prove\}\(\\phi\_\{2\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)
16:elseif

ϕ=ϕ1∨ϕ2\\phi=\\phi\_\{1\}\\lor\\phi\_\{2\}then⊳\\trianglerightDischarge at least one sub\-obligation

17:returnthe successful result of

Prove​\(ϕ1,𝒜′,𝒯\)\\textsc\{Prove\}\(\\phi\_\{1\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)or

Prove​\(ϕ2,𝒜′,𝒯\)\\textsc\{Prove\}\(\\phi\_\{2\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)
18:foreach

\(ℬ,𝔬\)\(\\mathcal\{B\},\\mathfrak\{o\}\)yielded by

Identify​\(ϕ,𝒫,𝒯\)\\textsc\{Identify\}\(\\phi,\\mathcal\{P\},\\mathcal\{T\}\)do⊳\\trianglerightIdentify​\(ϕ,𝒫,𝒯\)\\textsc\{Identify\}\(\\phi,\\mathcal\{P\},\\mathcal\{T\}\)is given in Algorithm[2](https://arxiv.org/html/2610.40751#alg2)

19:

ℬ𝔬←Prove​\(𝔬,𝒜′,𝒯\)\\mathcal\{B\}\_\{\\mathfrak\{o\}\}\\leftarrow\\textsc\{Prove\}\(\\mathfrak\{o\},\\mathcal\{A\}^\{\\prime\},\\mathcal\{T\}\)
20:if

ℬ𝔬≠Failed\\mathcal\{B\}\_\{\\mathfrak\{o\}\}\\neq\\textsc\{Failed\}then⊳\\trianglerightThe residual proof obligation has been discharged

21:return

ℬ∪ℬ𝔬\\mathcal\{B\}\\cup\\mathcal\{B\}\_\{\\mathfrak\{o\}\}⊳\\trianglerightCombine the accepted bridges

22:returnFailed⊳\\trianglerightThe search fails

#### 4\.3\.1Solver\-Controlled Recursion

Algorithm[1](https://arxiv.org/html/2610.40751#alg1)defines a recursive function,Prove​\(ϕ,𝒜,𝒯\)\\textsc\{Prove\}\(\\phi,\\mathcal\{A\},\\mathcal\{T\}\), that performs proof\-obligation\-guided search\. Here,ϕ\\phidenotes the current proof obligation and is initially set to𝔤\\mathfrak\{g\};𝒜\\mathcal\{A\}denotes the set of ancestor obligations to detect circular reasoning and is initially empty; and𝒯\\mathcal\{T\}is the grounding table\. The solver first attempts to dischargeϕ\\phidirectly through symbolic reasoning\. If this attempt fails, it normalizesϕ\\phiand distinguishes cases based on the top\-level logical structure ofϕ\\phi\.

For an existential obligationϕ=∃x\.ψ\\phi=\\exists x\.\\,\\psi, the solver branches over the type\-compatible instantiations ofxxgenerated by the operatorInst​\(ψ,𝒯\)\\textsc\{Inst\}\(\\psi,\\mathcal\{T\}\), wherexxmay denote a set of variables\. More precisely, for a formulaψ\\psicontaining variablesx1,…,xnx\_\{1\},\\ldots,x\_\{n\},

Inst\(ψ,𝒯\)=\{ψ\[θ\]\|θ=\{xi↦ci\}i=1nandtype𝒯\(ci\)⪯type𝒯\(xi\)for alli\}\.\\textsc\{Inst\}\(\\psi,\\mathcal\{T\}\)=\\left\\\{\\psi\[\\theta\]\\;\\middle\|\\;\\theta=\\\{x\_\{i\}\\mapsto c\_\{i\}\\\}\_\{i=1\}^\{n\}\\text\{ and \}\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(c\_\{i\}\)\\preceq\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(x\_\{i\}\)\\text\{ for all \}i\\right\\\}\.Here,θ\\thetais a substitution that maps each variablexix\_\{i\}to a constantcic\_\{i\};ψ⁡\[θ\]\\psi\[\\theta\]denotes the result of applyingθ\\thetatoψ\\psi; andτ1⪯τ2\\tau\_\{1\}\\preceq\\tau\_\{2\}denotes thatτ1\\tau\_\{1\}is a subtype ofτ2\\tau\_\{2\}, such as𝖲𝗍𝗎𝖽𝖾𝗇𝗍⪯𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Student\}\\preceq\\mathsf\{Person\}\. Type information thus rules out type\-incompatible instantiations before bridge identification begins\. For a universal obligationϕ=∀x\.ψ\\phi=\\forall x\.\\,\\psi, the solver introduces a fresh constantcfresh\{c\_\{\\mathrm\{fresh\}\}\}representing an arbitrary value ofxxand then provesψ\[x↦cfresh\]\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\], following the standard eigenvariable technique\[[21](https://arxiv.org/html/2610.40751#bib.bib17)\]\. For a conjunctive obligationϕ=ϕ1∧ϕ2\\phi=\\phi\_\{1\}\\land\\phi\_\{2\}, both sub\-obligations must be discharged\. In contrast, for a disjunctive obligationϕ=ϕ1∨ϕ2\\phi=\\phi\_\{1\}\\lor\\phi\_\{2\}, it suffices to dischargeat least one sub\-obligation\.

Algorithm 2Semantic bridge identification1:An unresolved obligation

ϕ\\phi, a set of formalized premises

𝒫\\mathcal\{P\}, a grounding table

𝒯\\mathcal\{T\}, and a threshold

τNLI\{\\tau\_\{\\mathrm\{NLI\}\}\}\.

2:A set of accepted semantic bridge \(possiblyFailed\) and its corresponding residual obligation\.

3:functionIdentify\(

ϕ,𝒫,𝒯\\phi,\\mathcal\{P\},\\mathcal\{T\}\)

4:

𝒬bridge←∅\{\\mathcal\{Q\}\_\{\\mathrm\{bridge\}\}\}\\leftarrow\\varnothing⊳\\trianglerightInitialize the candidate pool

5:for all

ℐ⊆⋃𝔭∈𝒫Inst​\(𝔭,𝒯\)\\mathcal\{I\}\\subseteq\\bigcup\_\{\\mathfrak\{p\}\\in\\mathcal\{P\}\}\\textsc\{Inst\}\(\\mathfrak\{p\},\\mathcal\{T\}\)do⊳\\trianglerightEnumerate subsets of all type\-compatible instantiations

6:for all

𝕊lit⊆⋃𝔦∈ℐLit​\(𝔦\)\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}\\subseteq\\bigcup\_\{\\mathfrak\{i\}\\in\\mathcal\{I\}\}\\textsc\{Lit\}\(\\mathfrak\{i\}\)with

\|𝕊lit\|≤2\|\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}\|\\leq 2do⊳\\trianglerightEnumerate support sets comprising at most two literals

7:

Σ←⋀ℓ∈𝕊litℓ\\Sigma\\leftarrow\\bigwedge\_\{\{\\ell\}\\in\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}\}\{\\ell\}⊳\\trianglerightConstruct the candidate semantic support

8:

𝔬←Abduce​\(ℐ,Σ\)\\mathfrak\{o\}\\leftarrow\\textsc\{Abduce\}\(\\mathcal\{I\},\\Sigma\)⊳\\trianglerightDerive the residual proof obligation

9:

ssim←sim⁡\(NL𝒯⁡\(Σ\),NL𝒯⁡\(ϕ\)\)\{s\_\{\\mathrm\{sim\}\}\}\\leftarrow\\operatorname\{sim\}\(\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\Sigma\),\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\phi\)\)⊳\\trianglerightCompute semantic similarity

10:

𝒬bridge←𝒬bridge∪\{\(Σ,𝔬,ssim\)\}\{\\mathcal\{Q\}\_\{\\mathrm\{bridge\}\}\}\\leftarrow\{\\mathcal\{Q\}\_\{\\mathrm\{bridge\}\}\}\\cup\\\{\(\\Sigma,\\mathfrak\{o\},\{s\_\{\\mathrm\{sim\}\}\}\)\\\}
11:for

\(Σ,𝔬,ssim\)∈𝒬bridge\(\\Sigma,\\mathfrak\{o\},\{s\_\{\\mathrm\{sim\}\}\}\)\\in\{\\mathcal\{Q\}\_\{\\mathrm\{bridge\}\}\}in nonincreasing order of

ssim\{s\_\{\\mathrm\{sim\}\}\}do⊳\\trianglerightEvaluate candidates in ranked order

12:

ℬ←∅\\mathcal\{B\}\\leftarrow\\varnothingif

Σ=ϕ\\Sigma=\\phi; otherwise

ℬ←\{Σ→ϕ\}\\mathcal\{B\}\\leftarrow\\\{\\Sigma\\rightarrow\\phi\\\}
13:if

ℬ=∅\\mathcal\{B\}=\\varnothingor

NLI​\(NL𝒯⁡\(Σ\),NL𝒯⁡\(ϕ\)\)≥τNLI\\textsc\{NLI\}\(\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\Sigma\),\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\phi\)\)\\geq\{\\tau\_\{\\mathrm\{NLI\}\}\}then⊳\\trianglerightPerform NLI filtering

14:if

Gate⁡\(ℬ,𝒯\)=Accepted\\operatorname\{Gate\}\(\\mathcal\{B\},\\mathcal\{T\}\)=\\textsc\{Accepted\}then⊳\\trianglerightEvaluate the bridge using the LLM\-basedGate\\operatorname\{Gate\}

15:yield

\(ℬ,𝔬\)\(\\mathcal\{B\},\\mathfrak\{o\}\)

#### 4\.3\.2Semantic Bridge Identification

Ifϕ\\phiremains unresolved after the above process, Algorithm[2](https://arxiv.org/html/2610.40751#alg2)is invoked to identify bridges that can provide semantic support forϕ\\phi\. The key idea is to address two questions separately:*which semantic support can bridge the gap to the current proof obligation*, and*what residual obligation must still be discharged to establish that support*\. The former is addressed by LLM\-based evaluation, whereas the latter is addressed by symbolic reasoning\.

Specifically, for each formalized premise𝔭∈𝒫\\mathfrak\{p\}\\in\\mathcal\{P\}, the operatorInst​\(𝔭,𝒯\)\\textsc\{Inst\}\(\\mathfrak\{p\},\\mathcal\{T\}\)first generates type\-compatible instantiations\. For each instantiation𝔦\\mathfrak\{i\}, letLit​\(𝔦\)\\textsc\{Lit\}\(\\mathfrak\{i\}\)denote the set of literals it contains, where a literal is an atomic formula or its negation\. For example, the instantiation𝖦𝖺𝗂𝗇⁡\(h,k\)→𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\mathsf\{Gain\}\(h,k\)\\rightarrow\\mathsf\{Smarter\}\(h\)is equivalent to¬𝖦𝖺𝗂𝗇⁡\(h,k\)∨𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\neg\\mathsf\{Gain\}\(h,k\)\\lor\\mathsf\{Smarter\}\(h\), which contains the literals¬𝖦𝖺𝗂𝗇⁡\(h,k\)\\neg\\mathsf\{Gain\}\(h,k\)and𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\mathsf\{Smarter\}\(h\)\. Algorithm[2](https://arxiv.org/html/2610.40751#alg2)then considers a subsetℐ\\mathcal\{I\}of all type\-compatible instantiations and selects a support set𝕊lit⊆⋃𝔦∈ℐLit​\(𝔦\)\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}\\subseteq\\bigcup\_\{\\mathfrak\{i\}\\in\\mathcal\{I\}\}\\textsc\{Lit\}\(\\mathfrak\{i\}\), whose literals may come from multiple premises and may jointly support the current obligationϕ\\phi\. For computational tractability,𝕊lit\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}is restricted to at most two literals\. The literals in𝕊lit\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}are conjoined to form a candidate*semantic support*Σ=⋀ℓ∈𝕊litℓ\\Sigma=\\bigwedge\_\{\{\\ell\}\\in\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}\}\{\\ell\}, yielding a candidate*semantic bridge*Σ→ϕ\\Sigma\\rightarrow\\phi\. For example, whenϕ=𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\\phi=\\mathsf\{SmarterThanBefore\}\(h\), selecting𝕊lit=\{𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\}\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}=\\\{\\mathsf\{Smarter\}\(h\)\\\}yieldsΣ=𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\Sigma=\\mathsf\{Smarter\}\(h\)and the corresponding bridge𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)→𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\\mathsf\{Smarter\}\(h\)\\rightarrow\\mathsf\{SmarterThanBefore\}\(h\)\. Next, candidate semantic bridges are filtered using a lightweight semantic similarity model and a natural language inference \(NLI\) model, both of which takeNL𝒯⁡\(Σ\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\Sigma\)andNL𝒯⁡\(ϕ\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\phi\)as inputs\. Finally, the LLM\-basedGate\\operatorname\{Gate\}evaluates whether each remaining bridge holds\.

Even after a bridge is accepted byGate\\operatorname\{Gate\}, its supportΣ\\Sigmamay remain unresolved\. We therefore use logical abduction\[[17](https://arxiv.org/html/2610.40751#bib.bib18)\]to derive a residual proof obligation𝔬\\mathfrak\{o\}that, together with the instantiations inℐ\\mathcal\{I\}, is sufficient to establishΣ\\Sigma:

𝔬=Abduce​\(ℐ,Σ\),\(⋀𝔦∈ℐ𝔦\)∧𝔬⊧Σ\.\\mathfrak\{o\}=\\textsc\{Abduce\}\(\\mathcal\{I\},\\Sigma\),\\qquad\\left\(\\bigwedge\\nolimits\_\{\\mathfrak\{i\}\\in\\mathcal\{I\}\}\\mathfrak\{i\}\\right\)\\land\\mathfrak\{o\}\\models\\Sigma\.The residual obligation𝔬\\mathfrak\{o\}is then passed to Algorithm[1](https://arxiv.org/html/2610.40751#alg1)for recursive discharge\. Thus, Algorithm[2](https://arxiv.org/html/2610.40751#alg2)decouples semantic understanding from logical reasoning: neural models evaluate only the candidate semantic bridgeΣ→ϕ\\Sigma\\rightarrow\\phi, whereas the residual obligation required to establishΣ\\Sigmais derived symbolically through logical abduction and must still be discharged by the symbolic solver\.

#### 4\.3\.3Termination and Soundness

When the search succeeds, Algorithm[1](https://arxiv.org/html/2610.40751#alg1)returns a bridge set that satisfies both criteria in Equation \([11](https://arxiv.org/html/2610.40751#S4.E11)\): the set enables the solver to complete the proof of goal𝔤\\mathfrak\{g\}, and every bridge in the set is accepted byGate\\operatorname\{Gate\}\. Theoretical proof of this soundness guarantee is provided in Appendix[A\.2](https://arxiv.org/html/2610.40751#A1.SS2)\. A search branch fails if the current obligation already appears on its ancestor path, if all candidate bridges are rejected, or if a search limit is reached\. The ancestor check aims to prevent circular reasoning\[[3](https://arxiv.org/html/2610.40751#bib.bib16)\]: if an attempt to proveϕ\\phigeneratesψ\\psiand a subsequent attempt to proveψ\\psiregeneratesϕ\\phi, the repeated obligation is rejected because it cannot serve as its own justification\.

## 5Experimental Results

### 5\.1Experimental Setup

Models\.We compareSafin\-1\.5with Safin\-1 \(35B\-A3B\)\[[56](https://arxiv.org/html/2610.40751#bib.bib24)\], the base model\.Safin\-1\.5incorporates REX\[[16](https://arxiv.org/html/2610.40751#bib.bib46)\]andReSIinto this base model\. Post\-training andReSIupdates are performed on the full model, including the removable experts introduced by REX \(Section[2\.2](https://arxiv.org/html/2610.40751#S2.SS2)\)\.

ReSIinstantiation\.We instantiate the extensible pools, training settings, and validation sets ofReSIwith representative resources\. The safety data pool is initialized with the WildJailbreak training split\[[15](https://arxiv.org/html/2610.40751#bib.bib47)\]\. The red\-teaming pool contains DARWIN and JailbreakSkill\[[32](https://arxiv.org/html/2610.40751#bib.bib54),[48](https://arxiv.org/html/2610.40751#bib.bib55)\]\. The alignment\-method pool contains A3, SInternal, and AlphaAlign \(Section[3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2)\)\. General\-task examples are drawn from Dolci\-Instruct\-SFT111[https://huggingface\.co/datasets/allenai/Dolci\-Instruct\-SFT](https://huggingface.co/datasets/allenai/Dolci-Instruct-SFT)\. All updates use LoRA with rank 32 andα=64\\alpha=64\. Recipe development and checkpoint selection use a development panel drawn from WildJailbreak, H\-CoT, XSTest, and IFEval, which provides the validation sets for the safety gain and the Pareto gate \(Sections[3\.2\.3](https://arxiv.org/html/2610.40751#S3.SS2.SSS3)and[3\.2\.4](https://arxiv.org/html/2610.40751#S3.SS2.SSS4)\)\.

Evaluation\.FollowingReSI\[[62](https://arxiv.org/html/2610.40751#bib.bib37)\], we evaluate resistance, resilience, benign compliance, and retention of general capabilities, and additionally measure hazardous knowledge\. Resistance is measured by attack success rate \(ASR, lower is better\) on WildJailbreak, which shares its distribution with the safety data pool, and on HarmBench\[[25](https://arxiv.org/html/2610.40751#bib.bib48)\], which measures retention of existing defenses\. Resilience is assessed on two attack mechanisms outside the red\-teaming pool: H\-CoT\[[18](https://arxiv.org/html/2610.40751#bib.bib49)\], which hijacks the model’s safety reasoning with injected chain\-of\-thought content, and X\-Teaming\[[36](https://arxiv.org/html/2610.40751#bib.bib50)\], an adaptive multi\-turn attack\. Benign compliance is measured by the full\-compliance rate on benign XSTest requests\[[38](https://arxiv.org/html/2610.40751#bib.bib51)\]\. General capabilities are measured by MMLU\-Pro\[[47](https://arxiv.org/html/2610.40751#bib.bib52)\]and IFEval\[[64](https://arxiv.org/html/2610.40751#bib.bib53)\]\. Hazardous knowledge is measured by multiple\-choice accuracy on WMDP\-Bio and WMDP\-Cyber\[[20](https://arxiv.org/html/2610.40751#bib.bib6)\]\.Safin\-1\.5and the REX\-based variants in the ablation study are evaluated after excision\.

Formalization\.We integrate POGB intoSafin\-1\.5as an inference\-time component enabled only for logical reasoning tasks\. We evaluateSafin\-1\.5on four logical reasoning benchmarks: FOLIO\[[10](https://arxiv.org/html/2610.40751#bib.bib20)\], ProofWriter\[[44](https://arxiv.org/html/2610.40751#bib.bib21)\], PrOntoQA\[[39](https://arxiv.org/html/2610.40751#bib.bib22)\], and ProverQA\-Hard\[[31](https://arxiv.org/html/2610.40751#bib.bib23)\]\. These benchmarks cover linguistically diverse, human\-written problems and template\-constrained synthetic tasks with varying reasoning complexity\. We compareSafin\-1\.5with Gemini3\-Flash\[[9](https://arxiv.org/html/2610.40751#bib.bib25)\], DeepSeek\-V3\.2\[[22](https://arxiv.org/html/2610.40751#bib.bib26)\], Qwen3\.8\-Flash\[[35](https://arxiv.org/html/2610.40751#bib.bib27)\], and GPT\-5\.5\[[28](https://arxiv.org/html/2610.40751#bib.bib28)\], GPT\-5\.6\-Luna\[[29](https://arxiv.org/html/2610.40751#bib.bib3)\],Claude Opus 5\[[2](https://arxiv.org/html/2610.40751#bib.bib62)\],GLM\-5\.3\[[53](https://arxiv.org/html/2610.40751#bib.bib64)\],Kimi K3\[[27](https://arxiv.org/html/2610.40751#bib.bib63)\]\. each evaluated using Direct Prediction \(Direct\) and Chain\-of\-Thought \(CoT\) prompting\. For each problem,Safin\-1\.5samples up to three formalizations, stopping once a valid formal proof is found and falling back to CoT if all attempts fail\. For semantic bridge identification,Safin\-1\.5usesall\-MiniLM\-L6\-v2\[[37](https://arxiv.org/html/2610.40751#bib.bib29)\]to compute semantic similarity androberta\-large\-mnli\[[23](https://arxiv.org/html/2610.40751#bib.bib30)\]for natural language inference\. The NLI entailment thresholdτNLI\\tau\_\{\\mathrm\{NLI\}\}is set to 0\.80 across all datasets\. We report accuracy on each benchmark and an overall average weighted by the evaluation set size of each dataset\.

### 5\.2Main Results

We compareSafin\-1\.5with Safin\-1 \(Table[1](https://arxiv.org/html/2610.40751#S5.T1)\), place it among frontier models \(Table[2](https://arxiv.org/html/2610.40751#S5.T2)\), and integrate it with formalization \(Table[3](https://arxiv.org/html/2610.40751#S5.T3)\)\.

Results on H\-CoT and X\-Teaming show thatSafin\-1\.5substantially strengthens resilience to attack mechanisms outside the red\-teaming pool compared with Safin\-1\. As shown in Table[1](https://arxiv.org/html/2610.40751#S5.T1), H\-CoT ASR decreases from 82\.00% to 14\.00%, and X\-Teaming ASR from 64\.78% to 32\.08%\.

Moreover,Safin\-1\.5improves resistance on WildJailbreak, and its HarmBench ASR remains low\. WildJailbreak ASR decreases from 2\.10% for Safin\-1 to 1\.20%, and HarmBench ASR is 1\.25%, compared with 0\.25% for Safin\-1\.

Compared with Safin\-1,Safin\-1\.5retains instruction following and knowledge, with a small decrease in benign compliance\. Specifically, IFEval accuracy changes from 85\.58% to 87\.06% and MMLU\-Pro accuracy from 77\.10% to 76\.80%, while benign compliance on XSTest decreases from 88\.40% to 86\.80%\.

Table 1:Comparison between Safin\-1 andSafin\-1\.5\(%\)\.WildJailbreak, HarmBench, H\-CoT, and X\-Teaming report ASR; XSTest reports benign compliance; IFEval reports loose prompt\-level accuracy; WMDP reports multiple\-choice accuracy\.MetricSafin\-1Safin\-1\.5WildJailbreak↓\\downarrow2\.101\.20HarmBench↓\\downarrow0\.251\.25H\-CoT↓\\downarrow82\.0014\.00X\-Teaming↓\\downarrow64\.7832\.08XSTest↑\\uparrow88\.4086\.80MMLU\-Pro↑\\uparrow77\.1076\.80IFEval↑\\uparrow85\.5887\.06WMDP\-Bio↓\\downarrow82\.5643\.68WMDP\-Cyber↓\\downarrow58\.3333\.17Compared with frontier models,Safin\-1\.5achieves the lowest X\-Teaming and WildJailbreak ASRs and a competitive H\-CoT ASR, while its benign compliance is the lowest in the table \(Table[2](https://arxiv.org/html/2610.40751#S5.T2)\)\. The X\-Teaming ASR ofSafin\-1\.5is 32\.08%, compared with 56\.69–84\.85% for the frontier models\. Moreover, its WildJailbreak ASR of 1\.20% is lower than those of all frontier models, which range from 1\.90% to 9\.25%\. On H\-CoT,Safin\-1\.5reaches 14\.00%, lower than Claude Opus 5, GLM\-5\.3, and Kimi K3 and higher than GPT\-5\.6\-Luna\. However, its benign compliance of 86\.80% is lower than those of all other models in the table\.

Table 2:Comparison with frontier models \(%\)\.WJB and HB denote WildJailbreak and HarmBench\. Safety columns report ASR; XSTest reports benign compliance\.ModelWJB↓\\downarrowHB↓\\downarrowH\-CoT↓\\downarrowX\-Teaming↓\\downarrowXSTest↑\\uparrowGPT\-5\.6\-Luna\[[29](https://arxiv.org/html/2610.40751#bib.bib3)\]1\.900\.008\.0056\.69100\.00Claude Opus 5\[[2](https://arxiv.org/html/2610.40751#bib.bib62)\]9\.253\.5038\.0084\.8598\.80GLM\-5\.3\[[53](https://arxiv.org/html/2610.40751#bib.bib64)\]5\.353\.2524\.0076\.7399\.20Kimi K3\[[27](https://arxiv.org/html/2610.40751#bib.bib63)\]4\.503\.7518\.0077\.8099\.60Safin\-12\.100\.2582\.0064\.7888\.40Safin\-1\.51\.201\.2514\.0032\.0886\.80As shown in Table[3](https://arxiv.org/html/2610.40751#S5.T3),Safin\-1\.5combines strong predictive accuracy with verifiable reasoning\. On FOLIO, it achieves the highest accuracy of 88\.73%, surpassing the strongest baseline, Claude Opus 5 with Direct prompting, by 0\.98 percentage points\. It also attains 100\.00% on PrOntoQA, matching the best\-performing baselines, and near\-perfect accuracy of 99\.50% on ProofWriter, only 0\.33 percentage points below the best result\. On ProverQA\-Hard,Safin\-1\.5achieves 75\.60% accuracy\. Across all 1,804 evaluation examples, its overall accuracy reaches 91\.80%, exceeding every evaluated baseline configuration except those using Claude Opus 5\. Beyond answer accuracy,Safin\-1\.5provides machine\-checkable proofs whenever formal proof search succeeds\. These proofs allow the corresponding conclusions to be independently verified from the formalized premises and accepted semantic bridges, providing an explicit verification mechanism alongside competitive end\-to\-end performance\.

Table 3:End\-to\-end reasoning accuracy \(%\)\.The evaluation set size \(NN\) for each dataset is shown below its column header\.LLMMethodFOLIO↑\\uparrowN=204N=204ProofWriter↑\\uparrowN=600N=600PrOntoQA↑\\uparrowN=500N=500ProverQA↑\\uparrowN=500N=500Average↑\\uparrowGemini3\-FlashDirect69\.6177\.5095\.8065\.0078\.22CoT83\.8295\.33100\.0074\.8089\.63DeepSeek\-V3\.2Direct65\.6957\.6768\.2058\.8061\.81CoT84\.8091\.67100\.0069\.4087\.03Qwen3\.8\-FlashDirect68\.1472\.8390\.8064\.0074\.83CoT82\.3594\.33100\.0073\.4088\.75GPT\-5\.5Direct77\.4598\.67100\.0067\.8088\.08CoT79\.4198\.50100\.0066\.4087\.86GPT\-5\.6\-LunaDirect62\.7595\.8399\.8048\.6080\.10CoT74\.0299\.83100\.0051\.8083\.65Claude Opus 5Direct87\.7598\.50100\.0084\.0093\.68CoT82\.3598\.1799\.8081\.8092\.29GLM\-5\.3Direct81\.3798\.50100\.0062\.0086\.86CoT82\.8498\.83100\.0069\.8089\.30Kimi K3Direct83\.3398\.50100\.0076\.2091\.02CoT83\.8298\.17100\.0076\.0090\.91Safin\-1\.5N/A88\.7399\.50100\.0075\.6091\.80
### 5\.3Analysis

#### 5\.3\.1Safety\-Native Architecture

We first evaluate REX itself on Safin\-1\-35B\-A3B, against the same RMU recipe applied directly to the original model\.RRapplies the RMU operator, hyperparameters, and forget budget of the residual cleanup directly toBB, so thatRRandA2A\_\{2\}differ only in their starting point and retain reference\. For post\-training, three routes use the identical 250M\-token standard full\-parameter SFT with the same data order and random seed, and differ only in their starting points\.A3A\_\{3\}, which is Safin\-1\+REX, is trained on the recombined full model asF3F\_\{3\}and excised at deployment;A3A\_\{3\}\-direct is trained directly on the excisedA2A\_\{2\}; andRR\-SFT is trained onRR\. Hazardous knowledge is measured by WMDP\-Bio and WMDP\-Cyber, both four\-way multiple choice with a chance level of 25%, and general knowledge by MMLU\. Results are listed in Table[4](https://arxiv.org/html/2610.40751#S5.T4)\.

Table 4:REX versus the same RMU recipe on Safin\-1\-35B\-A3B \(%\)\.Kept share is\(WB−W250​M\)/\(WB−W0\)\(W\_\{B\}\-W\_\{250\\mathrm\{M\}\}\)/\(W\_\{B\}\-W\_\{0\}\), the fraction of the removal at the start of post\-training that remains after 250M tokens, whereWWdenotes WMDP accuracy\.StageModelWMDP\-Bio↓\\downarrowWMDP\-Cyber↓\\downarrowMMLU↑\\uparrowKept share↑\\uparrow\(Bio / Cyber\)OriginalBB\(Safin\-1\)82\.658\.382\.3–BaseRR56\.932\.782\.0–A2A\_\{2\}\(REX\)36\.229\.578\.9–250Mpost\-trainingRR\-SFT81\.747\.282\.43\.4 / 43\.6A3A\_\{3\}\-direct64\.041\.880\.740\.0 / 57\.5A3A\_\{3\}\(REX\)40\.832\.580\.290\.0 / 89\.9F3F\_\{3\}\(full model\)82\.857\.482\.6–Excising the removable experts takes the target knowledge of both domains away, while the full model retains it\. After 250M tokens of post\-training, the full modelF3F\_\{3\}reaches 82\.8% on WMDP\-Bio and 57\.4% on WMDP\-Cyber, on par with 82\.6% and 58\.3% forBB\. Its excised counterpartA3A\_\{3\}falls to 40\.8% and 32\.5%, with Cyber close to chance level, while MMLU differs by only 2\.4 points\. The same post\-training therefore produces two deliverables at once: a full model for authorized users that retains the hazardous capability, and a public model that contains no parameters of the removable experts\. A single set of removable experts serves both domains, and one excision removes the target knowledge of both, so the removable experts act as a common removal unit for multiple hazardous domains\.

Before post\-training, the public base modelA2A\_\{2\}of REX is already lower thanRRin both domains under the same RMU recipe\.A2A\_\{2\}reaches 36\.2% on WMDP\-Bio, 20\.7 points below the 56\.9% ofRR, and 29\.5% on WMDP\-Cyber, closer to chance level than the 32\.7% ofRR\. The two models share an identical RMU, so the difference comes from REX first relocating the target knowledge into the removable experts and excising it, which lets the cleanup start from a lower point\.A2A\_\{2\}retains over 96% of the MMLU accuracy ofBB\.

Under the same 250M tokens of standard post\-training, the removal by the same RMU recipe almost entirely disappears, whereas the public model of REX stays low, which is the most direct value of REX for Safety RSI\.RR\-SFT returns to 81\.7% on WMDP\-Bio, nearly the 82\.6% ofBB, whileA3A\_\{3\}stays at 40\.8%, 40\.9 points lower\. On WMDP\-Cyber,RR\-SFT returns to 47\.2% andA3A\_\{3\}stays at 32\.5%\. The kept share measures how much of the removal at the start of post\-training survives it, independent of where each route starts\. On Bio,A3A\_\{3\}keeps 90\.0% of the removal present at the start, whereasRR\-SFT keeps only 3\.4%; on Cyber, the two keep 89\.9% and 43\.6%\.A3A\_\{3\}\-direct starts from the sameA2A\_\{2\}but is trained on the public form without recombination, and its WMDP\-Bio rises to 64\.0%, a kept share of 40\.0%\. Since the three trajectories share data, budget, and order, the gap betweenRR\-SFT andA3A\_\{3\}\-direct comes from relocation and excision, and the gap betweenA3A\_\{3\}\-direct andA3A\_\{3\}comes from training on the full structure and excising at deployment\. The latter gap also directly supports the choice inReSIto train the full model rather than its excised counterpart \(Section[3\.3](https://arxiv.org/html/2610.40751#S3.SS3)\)\. Together, the two effects keep the public model close to its pre\-post\-training removal level, while general knowledge continues to grow, with MMLU rising from 78\.9% forA2A\_\{2\}to 80\.2% forA3A\_\{3\}\.

The same delivery scheme carries over to the safety updates ofReSI\. Starting fromF3F\_\{3\},ReSItrains the full model with all experts and red\-teams, validates, and gates its excised counterpart \(Section[3\.3](https://arxiv.org/html/2610.40751#S3.SS3)\)\. After this round, the excised model stays at 43\.68% on WMDP\-Bio and 33\.17% on WMDP\-Cyber, compared with 82\.56% and 58\.33% for Safin\-1 \(Table[1](https://arxiv.org/html/2610.40751#S5.T1)\)\. AlthoughReSIdiffers from standard post\-training in both its objective and its data, the removal brought by REX carries through this round as well\. Updating on the full structure and excising at deployment can thus serve as a fixed interface for every round of Safety RSI, so that neither safety repairs nor capability gains come at the cost of hazardous knowledge returning to the public model\.

#### 5\.3\.2ReSI: Recursive Safety Improvement

FollowingReSI\[[62](https://arxiv.org/html/2610.40751#bib.bib37)\], we analyze the results from Safin\-1 and Safin\-1\+REX in terms of resistance, resilience, and retention of general capabilities and benign compliance \(Table[5](https://arxiv.org/html/2610.40751#S5.T5)\); Table[1](https://arxiv.org/html/2610.40751#S5.T1)presents the overall comparison between Safin\-1 andSafin\-1\.5\.

Resistance: in\-distribution safety improvements and retention of existing defenses\.Results on WildJailbreak and HarmBench illustrate improved in\-distribution safety and retention of existing safety defenses, respectively, from both starting models afterReSIalignment\. Safin\-1 improves from 2\.10% to 0\.35% on WildJailbreak and retains its already low HarmBench ASR of 0\.25%\. Safin\-1\+REX improves from 2\.10% to 1\.20% on WildJailbreak, and its HarmBench ASR remains low, changing from 1\.00% to 1\.25%\.

Resilience: generalization to unseen attack mechanisms\.Beyond in\-distribution improvements,ReSIsubstantially strengthens safety against attack mechanisms outside the red\-teaming pool\. H\-CoT ASRs decrease from 82\.00% and 64\.00% before alignment to 6\.00% and 14\.00% afterward for Safin\-1 and Safin\-1\+REX, respectively\. In the overall comparison, X\-Teaming ASR decreases from 64\.78% for Safin\-1 to 32\.08% forSafin\-1\.5\(Table[1](https://arxiv.org/html/2610.40751#S5.T1)\)\.

Retention of general capabilities and benign compliance\.The safety gains fromReSIaccompany broadly retained general capabilities and benign compliance, with variation across starting models\. After alignment, benign\-compliance rates on XSTest decrease by 2\.80 percentage points for Safin\-1 and by 8\.40 points for Safin\-1\+REX\. MMLU\-Pro accuracy changes by\+2\.30\+2\.30and−2\.40\-2\.40percentage points, and IFEval loose prompt\-level accuracy by−1\.29\-1\.29and−5\.55\-5\.55points, for Safin\-1 and Safin\-1\+REX, respectively\.

Comparison with the A3 baseline\.Table[5](https://arxiv.org/html/2610.40751#S5.T5)compares A3\[[55](https://arxiv.org/html/2610.40751#bib.bib56)\], a fixed alignment method with its own data construction and refinement, withReSIon both starting models\. On Safin\-1,ReSIachieves lower ASRs and better benign compliance and capability retention than A3 across the reported metrics\. On Safin\-1\+REX,ReSIyieldsSafin\-1\.5, which matches A3 on HarmBench and H\-CoT and improves WildJailbreak, XSTest, and IFEval, although MMLU\-Pro accuracy is lower\. The comparison highlights the model\-dependent tradeoff between safety, benign compliance, and general capabilities\.

Table 5:Comparison with A3 on both starting models \(%\)\.WJB and HB denote WildJailbreak and HarmBench; XSTest reports benign compliance, and IFEval reports loose prompt\-level accuracy\. The final\+\+ReSIrow corresponds toSafin\-1\.5\.ModelWJB↓\\downarrowHB↓\\downarrowH\-CoT↓\\downarrowXSTest↑\\uparrowMMLU\-Pro↑\\uparrowIFEval↑\\uparrowSafin\-12\.100\.2582\.0088\.4077\.1085\.58\+ A30\.701\.0024\.0084\.8077\.4080\.59\+ReSI0\.350\.256\.0085\.6079\.4084\.29Safin\-1\+REX2\.101\.0064\.0095\.2079\.2092\.61\+ A31\.401\.2514\.0084\.8079\.8072\.46\+ReSI1\.201\.2514\.0086\.8076\.8087\.06

## 6Conclusions

In this work, we presentedSafin\-1\.5, a model built on a safety architecture, trained through recursive safety improvement, and equipped with an inference\-time formal reasoning harness\. Persistent safety memory and hazardous\-knowledge disentanglement support the retention of safety knowledge and the control of hazardous capabilities, while recursive safety improvement turns newly discovered vulnerabilities into evaluated repairs\. Experiments show substantial reductions in attack success rates while largely preserving general capabilities and benign compliance\. The formal reasoning harness further improves reasoning accuracy by combining the model’s language understanding with symbolic inference and verification, producing checkable proofs under formalized premises and accepted semantic bridges\. These results demonstrate progress toward the AI\-45° Law’s goal of coordinated safety and capability development\. In the future, we plan to examine safety retention over longer improvement trajectories and explore formal reasoning for safety decisions governed by explicit rules\.

## Authorship Statement

This work was led by the Shanghai Artificial Intelligence Laboratory with contributions from the authors listed below\.

Jingnan Zheng\*Cheng Jin\*Ming Zhang\*Huan Sun\*Zhongtian MaKaisen YangZiyuan ZhouTong WuDongcheng ZhangYi ZhangXiao WangHan QiShu YuErmo HuaZongji YuChaozhuo LiXiaoyu WenZhekai ChenJiawei ZhouSirui ChenNing DingAn ZhangTat\-Seng ChuaXiangnan HeXia HuBowen ZhouQiaosheng Zhang‡Youbang Sun‡Xiang Wang‡Zhongyu Huang‡Chaochao Lu†
∗Equal Contribution‡Technical Lead†Project Lead

## References

- \[1\]Anthropic\(2025\)Claude 4 system card\.External Links:[Link](https://www-cdn.anthropic.com/6d8a8055020700718b0c49369f60816ba2a7c285.pdf)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[2\]Anthropic\(2026\)System Card: Claude Opus 5\.Note:System cardAccessed 20 September 2026External Links:[Link](https://www.anthropic.com/claude-opus-5-system-card)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1),[Table 2](https://arxiv.org/html/2610.40751#S5.T2.7.3.1.1)\.
- \[3\]R\. N\. Bol, K\. R\. Apt, and J\. W\. Klop\(1991\)An analysis of loop checking mechanisms for logic programs\.Theoretical Computer Science86\(1\),pp\. 35–79\.Cited by:[§4\.3\.3](https://arxiv.org/html/2610.40751#S4.SS3.SSS3.p1.1)\.
- \[4\]L\. Cardelli\(1996\)Type systems\.ACM Computing Surveys28\(1\),pp\. 263–264\.Cited by:[§4\.2](https://arxiv.org/html/2610.40751#S4.SS2.p2.1)\.
- \[5\]M\. Chen, L\. Wang, and B\. Qu\(2026\)Recursive self\-improvement in ai: from bounded self\-refinement to autonomous research loops\.arXiv preprint arXiv:2607\.07663\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[6\]J\. Doshi and A\. C\. Stickland\(2024\)Does unlearning truly unlearn? a black box evaluation of llm unlearning methods\.arXiv preprint arXiv:2411\.12103\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.40751#S2.SS2.p1.1)\.
- \[7\]Y\. Duan, Y\. Liu, Z\. Tang, H\. Chen, J\. Zhou, Y\. Liu, B\. Xu, Y\. Wu, S\. Chen, Y\. Zhou,et al\.\(2026\)The last ai built by humans: toward genuine recursive self\-improvement\.arXiv preprint arXiv:2609\.11873\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[8\]C\. Gong, J\. Bi, D\. Yao, X\. Liang, C\. Xiang, and R\. Guo\(2026\)Evolutionary safety of recursive self\-improving ai: taxonomy, risk discovery, and evaluation\.arXiv preprint arXiv:2609\.31186\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[9\]Google DeepMind\(2025\)Gemini 3 Flash \- Model card\.External Links:[Link](https://deepmind.google/models/model-cards/gemini-3-flash/)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[10\]S\. Han, H\. Schoelkopf, Y\. Zhao, Z\. Qi, M\. Riddell, W\. Zhou, J\. Coady, D\. Peng, Y\. Qiao, L\. Benson,et al\.\(2024\)FOLIO: natural language reasoning with first\-order logic\.InProceedings of the 2024 Conference on Empirical Methods in Natural Language Processing,pp\. 22017–22031\.Cited by:[§A\.1](https://arxiv.org/html/2610.40751#A1.SS1.p1.2),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[11\]E\. J\. Hu, Y\. Shen, P\. Wallis, Z\. Allen\-Zhu, Y\. Li, S\. Wang, L\. Wang, and W\. Chen\(2021\)LoRA: Low\-Rank Adaptation of Large Language Models\.External Links:2106\.09685,[Link](https://arxiv.org/abs/2106.09685)Cited by:[§3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2.p5.1)\.
- \[12\]N\. İbrahimoğlu, M\. U\. Demirezen, and F\. Yıldız\(2026\)Autonomous ai agents and recursive self\-improvement: a comprehensive survey of contemporary architectures, capabilities, and safety frameworks\.Cluster Computing29\(13\),pp\. 766\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[13\]A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, T\. Lacroix, J\. Liu, W\. Li, M\. Jamnik, G\. Lample, and Y\. Wu\(2023\)Draft, sketch, and prove: guiding formal theorem provers with informal proofs\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=SMa9EAovKMC)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p3.1)\.
- \[14\]J\. Jiang, F\. Wang, J\. Shen, S\. Kim, and S\. Kim\(2026\)A survey on large language models for code generation\.ACM Transactions on Software Engineering and Methodology35\(2\),pp\. 1–72\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[15\]L\. Jiang, K\. Rao, S\. Han, A\. Ettinger, F\. Brahman, S\. Kumar, N\. Mireshghallah, X\. Lu, M\. Sap, Y\. Choi, and N\. Dziri\(2024\)WildTeaming at Scale: From In\-the\-Wild Jailbreaks to \(Adversarially\) Safer Language Models\.External Links:2406\.18510,[Link](https://arxiv.org/abs/2406.18510)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p2.1)\.
- \[16\]C\. Jin, Z\. Ma, X\. Wang, H\. Qi, X\. Wen, X\. Wang, Y\. Sun, X\. Hu, B\. Zhou, C\. Lu, and Q\. Zhang\(2026\)Towards architectural\-level safety control: relocating hazardous knowledge into removable experts in mixture\-of\-experts models\.External Links:2610\.25791,[Link](https://arxiv.org/abs/2610.25791)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p4.1),[§2\.2](https://arxiv.org/html/2610.40751#S2.SS2.p1.1),[§3\.3](https://arxiv.org/html/2610.40751#S3.SS3.p2.1),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p1.1)\.
- \[17\]J\. R\. Josephson and S\. G\. Josephson\(1996\)Abductive inference: computation, philosophy, technology\.Cambridge University Press\.Cited by:[§4\.3\.2](https://arxiv.org/html/2610.40751#S4.SS3.SSS2.p3.1)\.
- \[18\]M\. Kuo, J\. Zhang, A\. Ding, Q\. Wang, L\. DiValentin, Y\. Bao, W\. Wei, H\. Li, and Y\. Chen\(2025\)H\-CoT: Hijacking the Chain\-of\-Thought Safety Reasoning Mechanism to Jailbreak Large Reasoning Models, Including OpenAI o1/o3, DeepSeek\-R1, and Gemini 2\.0 Flash Thinking\.External Links:2502\.12893,[Link](https://arxiv.org/abs/2502.12893)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[19\]S\. A\. Lab, :, Y\. Bao, G\. Chen, M\. Chen, Y\. Chen, C\. Chen, L\. Chen, S\. Chen, X\. Chen, J\. Cheng, Y\. Cheng, D\. Deng, Y\. Ding, D\. Ding, X\. Ding, Y\. Ding, Z\. Dong, L\. Du, Y\. Fan, X\. Feng, Y\. Fu, Y\. Gao, R\. Ge, T\. Gu, L\. Gui, J\. Guo, Q\. He, Y\. Hou, X\. Hu, H\. Huang, K\. Huang, S\. Huang, Y\. Jiang, S\. Lei, J\. Li, L\. Li, H\. Li, J\. Li, X\. Li, Y\. Li, L\. Li, X\. Li, H\. Liang, D\. Liu, Q\. Liu, Z\. Liu, B\. Liu, H\. Liu, Y\. Liu, Z\. Liu, C\. Lu, Y\. Lu, X\. Lu, Z\. Lu, Q\. Lv, C\. Ma, J\. Ma, X\. Ma, Z\. Ma, L\. Meng, Z\. Miao, Y\. Niu, Y\. Peng, Y\. Pu, H\. Qi, C\. Qian, X\. Qiao, J\. Qu, J\. Qu, W\. Qu, W\. Qu, X\. Qu, Q\. Ren, Q\. Ren, Q\. Ren, J\. Shao, W\. Shao, S\. Shao, D\. Shi, X\. Song, X\. Song, Y\. Teng, X\. Tong, Y\. Wang, X\. Wang, S\. Wang, X\. Wang, Y\. Wang, Y\. Wang, Y\. Wang, F\. Wang, R\. Wang, W\. Wang, Y\. Wang, M\. Wei, X\. Wen, F\. Weng, Y\. Wu, Y\. Xiong, X\. Xu, C\. Yang, Y\. Yang, Y\. Yao, Y\. Ye, Z\. Yin, Y\. Yu, B\. Zhang, Q\. Zhang, J\. Zhang, Y\. Zhang, Y\. Zheng, H\. Zhou, Z\. Zhou, P\. Zhu, Q\. Zhu, Y\. Zhu, and B\. Zhou\(2025\)SafeWork\-r1: coevolving safety and intelligence under the ai\-45∘\{\}^\{\\circ\}law\.External Links:2507\.18576,[Link](https://arxiv.org/abs/2507.18576)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[20\]N\. Li, A\. Pan, A\. Gopal, S\. Yue, D\. Berrios, A\. Gatti, J\. D\. Li, A\. Dombrowski, S\. Goel, G\. Mukobi, N\. Helm\-Burger, R\. Lababidi, L\. Justen, A\. B\. Liu, M\. Chen, I\. Barrass, O\. Zhang, X\. Zhu, R\. Tamirisa, B\. Bharathi, A\. Herbert\-Voss, C\. B\. Breuer, A\. Zou, M\. Mazeika, Z\. Wang, P\. Oswal, W\. Lin, A\. A\. Hunt, J\. Tienken\-Harder, K\. Y\. Shih, K\. Talley, J\. Guan, I\. Steneker, D\. Campbell, B\. Jokubaitis, S\. Basart, S\. Fitz, P\. Kumaraguru, K\. K\. Karmakar, U\. Tupakula, V\. Varadharajan, Y\. Shoshitaishvili, J\. Ba, K\. M\. Esvelt, A\. Wang, and D\. Hendrycks\(2024\)The WMDP benchmark: measuring and reducing malicious use with unlearning\.InProceedings of the 41st International Conference on Machine Learning,R\. Salakhutdinov, Z\. Kolter, K\. Heller, A\. Weller, N\. Oliver, J\. Scarlett, and F\. Berkenkamp \(Eds\.\),Proceedings of Machine Learning Research, Vol\.235,pp\. 28525–28550\.External Links:[Link](https://proceedings.mlr.press/v235/li24bc.html)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.40751#S2.SS2.p1.1),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[21\]P\. Lincoln and N\. Shankar\(1994\)Proof search in first\-order linear logic and other cut\-free sequent calculi\.InProceedings of the 9th Annual Symposium on Logic in Computer Science,pp\. 282–291\.Cited by:[§4\.3\.1](https://arxiv.org/html/2610.40751#S4.SS3.SSS1.p2.2)\.
- \[22\]A\. Liu, A\. Mei, B\. Lin, B\. Xue, B\. Wang, B\. Xu, B\. Wu, B\. Zhang, C\. Lin, C\. Dong,et al\.\(2025\)DeepSeek\-V3\.2: pushing the frontier of open large language models\.arXiv preprint arXiv:2512\.02556\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[23\]Y\. Liu, M\. Ott, N\. Goyal, J\. Du, M\. Joshi, D\. Chen, O\. Levy, M\. Lewis, L\. Zettlemoyer, and V\. Stoyanov\(2019\)RoBERTa: a robustly optimized BERT pretraining approach\.arXiv preprint arXiv:1907\.11692\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[24\]C\. Lu, C\. Lu, R\. T\. Lange, J\. Foerster, J\. Clune, and D\. Ha\(2024\)The ai scientist: towards fully automated open\-ended scientific discovery\.External Links:2408\.06292,[Link](https://arxiv.org/abs/2408.06292)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[25\]M\. Mazeika, L\. Phan, X\. Yin, A\. Zou, Z\. Wang, N\. Mu, E\. Sakhaee, N\. Li, S\. Basart, B\. Li, D\. Forsyth, and D\. Hendrycks\(2024\)HarmBench: A Standardized Evaluation Framework for Automated Red Teaming and Robust Refusal\.External Links:2402\.04249,[Link](https://arxiv.org/abs/2402.04249)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[26\]S\. Minaee, T\. Mikolov, N\. Nikzad, M\. Chenaghlu, R\. Socher, X\. Amatriain, and J\. Gao\(2024\)Large language models: a survey\.arXiv preprint arXiv:2402\.06196\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[27\]Moonshot AI\(2026\)Kimi K3: Open Frontier Intelligence\.Note:Technical reportExternal Links:[Link](https://github.com/MoonshotAI/Kimi-K3/blob/main/k3_tech_report.pdf)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1),[Table 2](https://arxiv.org/html/2610.40751#S5.T2.7.5.1.1)\.
- \[28\]OpenAI\(2026\)GPT\-5\.5 system card\.External Links:[Link](https://deploymentsafety.openai.com/gpt-5-5)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[29\]OpenAI\(2026\)GPT\-5\.6 system card\.Note:OpenAI Deployment Safety HubAccessed 20 September 2026External Links:[Link](https://deploymentsafety.openai.com/gpt-5-6)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1),[§1](https://arxiv.org/html/2610.40751#S1.p2.1),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1),[Table 2](https://arxiv.org/html/2610.40751#S5.T2.7.2.1.1)\.
- \[30\]L\. Pan, A\. Albalak, X\. Wang, and W\. Wang\(2023\)Logic\-LM: empowering large language models with symbolic solvers for faithful logical reasoning\.InFindings of the Association for Computational Linguistics: EMNLP 2023,H\. Bouamor, J\. Pino, and K\. Bali \(Eds\.\),Singapore,pp\. 3806–3824\.External Links:[Link](https://aclanthology.org/2023.findings-emnlp.248/),[Document](https://dx.doi.org/10.18653/v1/2023.findings-emnlp.248)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p3.1)\.
- \[31\]C\. Qi, R\. Ma, B\. Li, B\. Hui, J\. Wu, Y\. Laili, C\. He,et al\.\(2025\)Large language models meet symbolic provers for logical reasoning evaluation\.InProceedings of the 13th International Conference on Learning Representations,pp\. 54186–54205\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[32\]W\. Qi, Z\. Wu, Z\. Guo, T\. Zheng, C\. Lu, L\. He, Z\. Qin, and K\. Ren\(2026\)DARWIN: Evolving Jailbreak Adversary and Guardrail for LLM Safety Evaluation and Protection\.External Links:2607\.19829,[Link](https://arxiv.org/abs/2607.19829)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p2.1)\.
- \[33\]X\. Qi, A\. Panda, K\. Lyu, X\. Ma, S\. Roy, A\. Beirami, P\. Mittal, and P\. Henderson\(2025\)Safety alignment should be made more than just a few tokens deep\.InThe Thirteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=6Mxhg9PtDE)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1),[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.
- \[34\]X\. Qi, Y\. Zeng, T\. Xie, P\. Chen, R\. Jia, P\. Mittal, and P\. Henderson\(2024\)Fine\-tuning aligned language models compromises safety, even when users do not intend to\!\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 30988–31043\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1),[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.
- \[35\]Z\. Qiu, Z\. Wang, X\. Li, Y\. Li, Y\. Xu, Y\. Wang, H\. Zhang, R\. Men, B\. Mao, C\. Zhang,et al\.\(2026\)On the design of Qwen3\.8\-Next architecture: evaluation, efficiency, and training stability\.arXiv preprint arXiv:2608\.30320\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[36\]S\. Rahman, L\. Jiang, J\. Shiffer, G\. Liu, S\. Issaka, M\. R\. Parvez, H\. Palangi, K\. Chang, Y\. Choi, and S\. Gabriel\(2025\)X\-Teaming: Multi\-Turn Jailbreaks and Defenses with Adaptive Multi\-Agents\.External Links:2504\.13203,[Link](https://arxiv.org/abs/2504.13203)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[37\]N\. Reimers and I\. Gurevych\(2019\)Sentence\-BERT: sentence embeddings using siamese BERT\-networks\.InProceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing,pp\. 3982–3992\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[38\]P\. Röttger, H\. R\. Kirk, B\. Vidgen, G\. Attanasio, F\. Bianchi, and D\. Hovy\(2023\)XSTest: A Test Suite for Identifying Exaggerated Safety Behaviours in Large Language Models\.External Links:2308\.01263,[Link](https://arxiv.org/abs/2308.01263)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[39\]A\. Saparov and H\. He\(2023\)Language models are greedy reasoners: a systematic formal analysis of chain\-of\-thought\.InProceedings of the 11th International Conference on Learning Representations,Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[40\]Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. K\. Li, Y\. Wu, and D\. Guo\(2024\)DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models\.External Links:2402\.03300,[Link](https://arxiv.org/abs/2402.03300)Cited by:[4th item](https://arxiv.org/html/2610.40751#S3.I1.i4.p1.1)\.
- \[41\]H\. Sun, Z\. Huang, C\. Li, Z\. Chen, Y\. Sun, C\. Lu, and X\. Hu\(2026\)Let solvers reason and models understand: proof\-obligation\-guided bridging\.Zenodo\.Note:PreprintExternal Links:[Document](https://dx.doi.org/10.5281/zenodo.23527696),[Link](https://doi.org/10.5281/zenodo.23527696)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p4.1)\.
- \[42\]Y\. Sun, X\. Wang, J\. Fu, C\. Lu, and B\. Zhou\(2025\)R2\{\}^\{2\}AI: Towards Resistant and Resilient AI in an Evolving World\.External Links:2509\.06786,[Link](https://arxiv.org/abs/2509.06786)Cited by:[§3](https://arxiv.org/html/2610.40751#S3.p1.1)\.
- \[43\]Y\. Sun, X\. Wang, J\. Fu, C\. Lu, and B\. Zhou\(2026\)Position: safe AI should be resistant and resilient in an evolving world\.InForty\-third International Conference on Machine Learning Position Paper Track,External Links:[Link](https://openreview.net/forum?id=ApUb0ToKMN),2509\.06786Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1),[§3](https://arxiv.org/html/2610.40751#S3.p1.1)\.
- \[44\]O\. Tafjord, B\. Dalvi, and P\. Clark\(2021\)ProofWriter: generating implications, proofs, and abductive statements over natural language\.InFindings of the Association for Computational Linguistics: ACL\-IJCNLP 2021,pp\. 3621–3634\.Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1)\.
- \[45\]E\. Wallace, C\. A\. Choquette\-Choo, N\. Kandpal, S\. Toyer, D\. Hunn, S\. Lin, Y\. Wen, X\. Qi, C\. Wolff, Z\. Wang, M\. Nasr, S\. Zhu, C\. Guo, J\. F\. C\. Uribe, K\. Wang, A\. Low, K\. Xiao, and K\. Chen\(2026\)GPT\-red: automated red teaming via self\-play at scale\.External Links:2607\.26115,[Link](https://arxiv.org/abs/2607.26115)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.
- \[46\]H\. Wang, Y\. Zhao, Z\. Qin, C\. Du, M\. Lin, X\. Wang, and T\. Pang\(2026\)Lifelong safety alignment for language models\.Advances in Neural Information Processing Systems38,pp\. 19908–19938\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.
- \[47\]Y\. Wang, X\. Ma, G\. Zhang, Y\. Ni, A\. Chandra, S\. Guo, W\. Ren, A\. Arulraj, X\. He, Z\. Jiang, T\. Li, M\. Ku, K\. Wang, A\. Zhuang, R\. Fan, X\. Yue, and W\. Chen\(2024\)MMLU\-Pro: A More Robust and Challenging Multi\-Task Language Understanding Benchmark\.External Links:2406\.01574,[Link](https://arxiv.org/abs/2406.01574)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[48\]X\. Wen, J\. Li, Z\. He, P\. Yu, C\. Wang, H\. Qi, Z\. Zhou, C\. Jin, Y\. Wen, X\. Xu, S\. Hu, T\. Zheng, C\. Lu, and Q\. Zhang\(2026\)JailbreakSkill: Scaling Automated Red\-Teaming with Reusable and Ever\-Evolving Skills\.External Links:2608\.16465,[Link](https://arxiv.org/abs/2608.16465)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p2.1)\.
- \[49\]J\. Woodcock, P\. G\. Larsen, J\. Bicarregui, and J\. Fitzgerald\(2009\)Formal methods: practice and experience\.ACM Comput\. Surv\.41\(4\)\.External Links:ISSN 0360\-0300,[Link](https://doi.org/10.1145/1592434.1592436),[Document](https://dx.doi.org/10.1145/1592434.1592436)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p3.1)\.
- \[50\]T\. Wu, F\. Lin, G\. Wang, T\. Liu, Z\. Wang, W\. Meng, A\. Liu, and K\. Ren\(2025\)CoGA: a collaborative gray\-box adversarial attack for multimodal language models\.IEEE Transactions on Information Forensics and Security21,pp\. 870–885\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.
- \[51\]Y\. Yao, J\. Duan, K\. Xu, Y\. Cai, Z\. Sun, and Y\. Zhang\(2024\)A survey on large language model \(llm\) security and privacy: the good, the bad, and the ugly\.High\-Confidence Computing4\(2\),pp\. 100211\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[52\]Q\. Yu, Z\. Zhang, R\. Zhu, Y\. Yuan, X\. Zuo, Y\. Yue, W\. Dai, T\. Fan, G\. Liu, L\. Liu, X\. Liu, H\. Lin, Z\. Lin, B\. Ma, G\. Sheng, Y\. Tong, C\. Zhang, M\. Zhang, W\. Zhang, H\. Zhu, J\. Zhu, J\. Chen, J\. Chen, C\. Wang, H\. Yu, Y\. Song, X\. Wei, H\. Zhou, J\. Liu, W\. Ma, Y\. Zhang, L\. Yan, M\. Qiao, Y\. Wu, and M\. Wang\(2025\)DAPO: an open\-source LLM reinforcement learning system at scale\.arXiv preprint arXiv:2503\.14476\.External Links:[Document](https://dx.doi.org/10.48550/arXiv.2503.14476),[Link](https://arxiv.org/abs/2503.14476)Cited by:[4th item](https://arxiv.org/html/2610.40751#S3.I1.i4.p1.1)\.
- \[53\]Z\.ai\(2026\)GLM\-5\.3\.Note:Official model cardAccessed 20 September 2026External Links:[Link](https://huggingface.co/zai-org/GLM-5.3)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p4.1),[Table 2](https://arxiv.org/html/2610.40751#S5.T2.7.4.1.1)\.
- \[54\]J\. Zhang, S\. Hu, C\. Lu, R\. T\. Lange, and J\. Clune\(2026\)Darwin gödel machine: open\-ended evolution of self\-improving agents\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=pUpzQZTvGY)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[55\]J\. Zhang, H\. Sleight, and J\. Benton\(2026\)A3: An Automated Alignment Agent for Safety Finetuning\.Note:Alignment Science BlogAccessed 15 September 2026External Links:[Link](https://alignment.anthropic.com/2026/automated-alignment-agent/)Cited by:[§3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2.p3.1),[§5\.3\.2](https://arxiv.org/html/2610.40751#S5.SS3.SSS2.p5.1)\.
- \[56\]M\. Zhang, K\. Yang, S\. Yu, E\. Hua, Z\. Chen, C\. Jin, J\. Zheng, Y\. Zhang, Z\. Ma, J\. Zhou, S\. Chen, Q\. Zhang, X\. Wang, N\. Ding, X\. Hu, B\. Zhou, Y\. Sun, and C\. Lu\(2026\)Safin\-1: safety from within through memory\-native state evolution\.External Links:2609\.00092,[Link](https://arxiv.org/abs/2609.00092)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p4.1),[§2\.1](https://arxiv.org/html/2610.40751#S2.SS1.SSS0.Px2.p1.1),[§2\.1](https://arxiv.org/html/2610.40751#S2.SS1.p1.1),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p1.1)\.
- \[57\]M\. Zhang, K\. Yang, S\. Yu, E\. Hua, N\. Ding, X\. Hu, B\. Zhou, C\. Lu, and Y\. Sun\(2026\)MARCH: scaling recurrent memory with content\-routed state anchors\.arXiv preprint arXiv:2608\.12435\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p4.1),[§2\.1](https://arxiv.org/html/2610.40751#S2.SS1.p1.1),[§3\.3](https://arxiv.org/html/2610.40751#S3.SS3.p3.1)\.
- \[58\]R\. Zhang, L\. Lin, Y\. Bai, and S\. Mei\(2024\)Negative preference optimization: from catastrophic collapse to effective unlearning\.InFirst Conference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=MXLBXjQkmb)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.40751#S2.SS2.p1.1)\.
- \[59\]Y\. Zhang, Y\. Chen, L\. Sheng, D\. Zhang, C\. Lu, X\. Wang, and A\. Zhang\(2026\)Internalizing Safety Understanding in Large Reasoning Models via Verification\.External Links:2605\.08930,[Link](https://arxiv.org/abs/2605.08930)Cited by:[§3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2.p3.1)\.
- \[60\]Y\. Zhang, A\. Zhang, X\. Zhang, L\. Sheng, Y\. Chen, Z\. Liang, and X\. Wang\(2025\)AlphaAlign: incentivizing safety alignment with extremely simplified reinforcement learning\.External Links:2507\.14987,[Link](https://arxiv.org/abs/2507.14987)Cited by:[§3\.2\.2](https://arxiv.org/html/2610.40751#S3.SS2.SSS2.p3.1)\.
- \[61\]Y\. Zhang, J\. Wang, S\. Lyu, Y\. Ge, K\. Liang, Z\. Jin, C\. K\. Reddy, and J\. Hamm\(2026\)Safety must survive self\-improvement: why failures persist and how agents recover\.arXiv preprint arXiv:2610\.01073\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[62\]J\. Zheng, D\. Zhang, Y\. Zhang, M\. Zhang, Q\. Zhang, Y\. Sun, A\. Zhang, X\. He, T\. Chua, X\. Hu, B\. Zhou, C\. Lu, and X\. Wang\(2026\)ReSI: recursive safety improvement toward resistant and resilient ai\.External Links:2610\.12233,[Link](https://arxiv.org/abs/2610.12233)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p4.1),[§3](https://arxiv.org/html/2610.40751#S3.p1.1),[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1),[§5\.3\.2](https://arxiv.org/html/2610.40751#S5.SS3.SSS2.p1.1)\.
- \[63\]T\. Zheng, X\. Wu, Z\. Zhang, Z\. He, C\. Zhang, B\. Coleman, R\. Wei, D\. Bai, H\. Liu, R\. Liu,et al\.\(2026\)Dream\-rsi: recursive self\-improvement through evolving worlds\.arXiv preprint arXiv:2609\.14858\.Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p1.1)\.
- \[64\]J\. Zhou, T\. Lu, S\. Mishra, S\. Brahma, S\. Basu, Y\. Luan, D\. Zhou, and L\. Hou\(2023\)Instruction\-Following Evaluation for Large Language Models\.External Links:2311\.07911,[Link](https://arxiv.org/abs/2311.07911)Cited by:[§5\.1](https://arxiv.org/html/2610.40751#S5.SS1.p3.1)\.
- \[65\]Z\. Zhou, G\. Liu, M\. Zhou, and W\. Guo\(2025\)Robust multi\-agent reinforcement learning with stochastic adversary\.InForty\-second International Conference on Machine Learning,External Links:[Link](https://openreview.net/forum?id=bnhFueOeav)Cited by:[§1](https://arxiv.org/html/2610.40751#S1.p2.1)\.

## Appendix AAppendix

### A\.1Running Example

In this section, we illustrate our proposed method through a simplified example from the FOLIO dataset\[[10](https://arxiv.org/html/2610.40751#bib.bib20)\]\. The NL premise setℙ=\{p1;p2;p3\}\\mathbb\{P\}=\\\{p\_\{1\};p\_\{2\};p\_\{3\}\\\}states: “Reading a book gives a person knowledge; gaining knowledge makes that person smarter; and Harry read*Walden*\.” The NL queryqqasks whether the statement “Harry is smarter than before” can be concluded from these premises\. Let the constantshh,ww, andkkdenote Harry,*Walden*, and knowledge, respectively\. We first perform a grounding autoformalizationA​F\{AF\}to mapX=\(ℙ,q\)X=\(\\mathbb\{P\},q\)to

𝒫=\{\\displaystyle\\mathcal\{P\}=\\\{𝔭1:∀x1​∀y\.\(𝖡𝗈𝗈𝗄⁡\(y\)∧𝖱𝖾𝖺𝖽⁡\(x1,y\)\)→𝖦𝖺𝗂𝗇⁡\(x1,k\),\\displaystyle\\mathfrak\{p\}\_\{1\}:\\ \\forall x\_\{1\}\\forall y\.\\ \\bigl\(\\mathsf\{Book\}\(y\)\\land\\mathsf\{Read\}\(x\_\{1\},y\)\\bigr\)\\rightarrow\\mathsf\{Gain\}\(x\_\{1\},k\),𝔭2:∀x2\.𝖦𝖺𝗂𝗇⁡\(x2,k\)→𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(x2\),\\displaystyle\\mathfrak\{p\}\_\{2\}:\\ \\forall x\_\{2\}\.\\ \\mathsf\{Gain\}\(x\_\{2\},k\)\\rightarrow\\mathsf\{Smarter\}\(x\_\{2\}\),𝔭3:𝖡𝗈𝗈𝗄\(w\)∧𝖱𝖾𝖺𝖽\(h,w\)\},𝔮=𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾\(h\),\\displaystyle\\mathfrak\{p\}\_\{3\}:\\ \\mathsf\{Book\}\(w\)\\land\\mathsf\{Read\}\(h,w\)\\;\\\},\\qquad\\mathfrak\{q\}=\\mathsf\{SmarterThanBefore\}\(h\),and the grounding table𝒯\\mathcal\{T\}shown in Table[6](https://arxiv.org/html/2610.40751#A1.T6)\. During proof\-time inference, the solver can therefore access all entries in𝒯\\mathcal\{T\}\. In particular, type informationtype𝒯⁡\(𝔢\)\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)constrains which instantiations are admissible, whereas NL informationNL𝒯⁡\(𝔢\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)guides the search for semantic bridges when exact symbolic matching fails\.

Table 6:The grounding table𝒯\\mathcal\{T\}of the running example\.Formal element𝔢\\mathfrak\{e\}Type informationtype𝒯⁡\(𝔢\)\\operatorname\{type\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)Natural\-language informationNL𝒯⁡\(𝔢\)\\operatorname\{NL\}\_\{\\mathcal\{T\}\}\(\\mathfrak\{e\}\)hh𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“Harry”ww𝖡𝗈𝗈𝗄\\mathsf\{Book\}“*Walden*”kk𝖮𝖻𝗃𝖾𝖼𝗍\\mathsf\{Object\}“knowledge”x1x\_\{1\}𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“a person”x2x\_\{2\}𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“a person”yy𝖡𝗈𝗈𝗄\\mathsf\{Book\}“a book”𝖡𝗈𝗈𝗄⁡\(\{a1\}\)\\mathsf\{Book\}\(\\\{a\_\{1\}\\\}\)𝖡𝗈𝗈𝗄\\mathsf\{Book\}“\{a1\}\\\{a\_\{1\}\\\}is a book”𝖱𝖾𝖺𝖽⁡\(\{a1\},\{a2\}\)\\mathsf\{Read\}\(\\\{a\_\{1\}\\\},\\\{a\_\{2\}\\\}\)𝖯𝖾𝗋𝗌𝗈𝗇,𝖡𝗈𝗈𝗄\\mathsf\{Person\},\\mathsf\{Book\}“\{a1\}\\\{a\_\{1\}\\\}reads\{a2\}\\\{a\_\{2\}\\\}”𝖦𝖺𝗂𝗇⁡\(\{a1\},k\)\\mathsf\{Gain\}\(\\\{a\_\{1\}\\\},k\)𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“\{a1\}\\\{a\_\{1\}\\\}gains knowledge”𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(\{a1\}\)\\mathsf\{Smarter\}\(\\\{a\_\{1\}\\\}\)𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“\{a1\}\\\{a\_\{1\}\\\}is smarter”𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(\{a1\}\)\\mathsf\{SmarterThanBefore\}\(\\\{a\_\{1\}\\\}\)𝖯𝖾𝗋𝗌𝗈𝗇\\mathsf\{Person\}“\{a1\}\\\{a\_\{1\}\\\}is smarter than before”After completing the grounding autoformalization process described above, we perform the proof\-obligation\-guided search\. Initialize the proof obligation asϕ=𝔮=𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\\phi=\\mathfrak\{q\}=\\mathsf\{SmarterThanBefore\}\(h\)\. Algorithm[2](https://arxiv.org/html/2610.40751#alg2)instantiates𝔭1\\mathfrak\{p\}\_\{1\}and𝔭2\\mathfrak\{p\}\_\{2\}using the substitutionsx1↦hx\_\{1\}\\mapsto h,x2↦hx\_\{2\}\\mapsto h, andy↦wy\\mapsto w, yielding𝔦1\\mathfrak\{i\}\_\{1\}and𝔦2\\mathfrak\{i\}\_\{2\}\. Type compatibility permits these substitutions while ruling out alternatives such asx1↦wx\_\{1\}\\mapsto w,x1↦kx\_\{1\}\\mapsto k,x2↦wx\_\{2\}\\mapsto w,x2↦kx\_\{2\}\\mapsto k,y↦hy\\mapsto h, andy↦ky\\mapsto k\. Algorithm[2](https://arxiv.org/html/2610.40751#alg2)considersℐ=\{𝔦2\}\{\\mathcal\{I\}\}=\\\{\\mathfrak\{i\}\_\{2\}\\\}and obtains

Lit​\(𝔦2\)=\{¬𝖦𝖺𝗂𝗇⁡\(h,k\),𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\},\\textsc\{Lit\}\(\\mathfrak\{i\}\_\{2\}\)=\\\{\\neg\\mathsf\{Gain\}\(h,k\),\\mathsf\{Smarter\}\(h\)\\\},It then selects𝕊lit=\{𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\}⊆Lit​\(𝔦2\)\{\\mathbb\{S\}\_\{\\mathrm\{lit\}\}\}=\\\{\\mathsf\{Smarter\}\(h\)\\\}\\subseteq\\textsc\{Lit\}\(\\mathfrak\{i\}\_\{2\}\), and constructs the candidate semantic supportΣ=𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)\\Sigma=\\mathsf\{Smarter\}\(h\)and the candidate semantic bridge

𝔟\\displaystyle\\mathfrak\{b\}=Σ→ϕ\\displaystyle=\\Sigma\\rightarrow\\phi=𝖲𝗆𝖺𝗋𝗍𝖾𝗋⁡\(h\)→𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\.\\displaystyle=\\mathsf\{Smarter\}\(h\)\\rightarrow\\mathsf\{SmarterThanBefore\}\(h\)\.Logical abduction then derives the residual obligation𝔬=𝖦𝖺𝗂𝗇⁡\(h,k\)\\mathfrak\{o\}=\\mathsf\{Gain\}\(h,k\)\. Once the LLM\-basedGate\\operatorname\{Gate\}accepts𝔟\\mathfrak\{b\}based on its NL interpretation that “Harry is smarter” entails “Harry is smarter than before,” Algorithm[1](https://arxiv.org/html/2610.40751#alg1)proceeds to discharge the residual obligations:

𝖲𝗆𝖺𝗋𝗍𝖾𝗋𝖳𝗁𝖺𝗇𝖡𝖾𝖿𝗈𝗋𝖾⁡\(h\)\\displaystyle\\mathsf\{SmarterThanBefore\}\(h\)→𝔟𝔭2\[x2↦h\]\{𝖦𝖺𝗂𝗇⁡\(h,k\)\}\\displaystyle\\xrightarrow\[\\mathfrak\{b\}\]\{\\mathfrak\{p\}\_\{2\}\[x\_\{2\}\\mapsto h\]\}\\\{\\mathsf\{Gain\}\(h,k\)\\\}→𝔭1\[x1↦h,y↦w\]\{𝖡𝗈𝗈𝗄⁡\(w\),𝖱𝖾𝖺𝖽⁡\(h,w\)\}\\displaystyle\\xrightarrow\{\\mathfrak\{p\}\_\{1\}\[x\_\{1\}\\mapsto h,y\\mapsto w\]\}\\\{\\mathsf\{Book\}\(w\),\\mathsf\{Read\}\(h,w\)\\\}→𝔭3✓\.\\displaystyle\\xrightarrow\{\\mathfrak\{p\}\_\{3\}\}\\checkmark\.Here, each arrow represents the residual obligations produced in a single round of derivation, with bridging applied as needed\. Finally, premise𝔭3\\mathfrak\{p\}\_\{3\}discharges the two remaining obligations\. In this example, only the displayed bridge𝔟\\mathfrak\{b\}requires LLM evaluation throughout the derivation\.

### A\.2Proof of Soundness

###### Lemma 1\(Existential decomposition\)\.

Forϕ=∃x\.ψ\\phi=\\exists x\.\\,\\psi, letℬ\\mathcal\{B\}be the bridge set returned by a recursive call for an admissible instanceψ​\[θ\]∈Inst​\(ψ,𝒯\)\\psi\[\\theta\]\\in\\textnormal\{\{Inst\}\}\(\\psi,\\mathcal\{T\}\)\. If𝒮⁡\(𝒫∪ℬ,ψ⁡\[θ\]\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\psi\[\\theta\]\)=\\textnormal\{\{Proved\}\}\}, then𝒮⁡\(𝒫∪ℬ,ϕ\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\phi\)=\\textnormal\{\{Proved\}\}\}\.

###### Proof\.

Apply existential introduction with the witnessθ\\theta’s bridge set\. ∎

###### Lemma 2\(Universal decomposition\)\.

Forϕ=∀x\.ψ\\phi=\\forall x\.\\,\\psi, introduce a fresh eigenvariablecfresh\{c\_\{\\mathrm\{fresh\}\}\}and letℬ\\mathcal\{B\}be the bridge set returned forψ\[x↦cfresh\]\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\]\. Each bridge involvingcfresh\{c\_\{\\mathrm\{fresh\}\}\}is universally quantified over the corresponding variable and accepted by Gate with that universal scope\. If𝒮\(𝒫∪ℬ,ψ\[x↦cfresh\]\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\]\)=\\textnormal\{\{Proved\}\}\}, then𝒮⁡\(𝒫∪ℬ,ϕ\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\phi\)=\\textnormal\{\{Proved\}\}\}\.

###### Proof\.

The relevant bridges are asserted for every admissible assignment to the variable represented bycfresh\{c\_\{\\mathrm\{fresh\}\}\}\. Freshness and universal closure ensure that the assumptions do not depend on a particular value ofcfresh\{c\_\{\\mathrm\{fresh\}\}\}\. Universal introduction therefore extends the subproof ofψ\[x↦cfresh\]\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\]to a proof of∀x\.ψ\\forall x\.\\,\\psi, using the same bridge set\. ∎

###### Lemma 3\(Conjunctive decomposition\)\.

Forϕ=ϕ1∧ϕ2\\phi=\\phi\_\{1\}\\land\\phi\_\{2\}, letℬ1\\mathcal\{B\}\_\{1\}andℬ2\\mathcal\{B\}\_\{2\}be the bridge sets returned by the two recursive calls\. If𝒮⁡\(𝒫∪ℬi,ϕi\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\}\_\{i\},\\phi\_\{i\}\)=\\textnormal\{\{Proved\}\}\}fori=1,2i=1,2, then their merged setℬ=ℬ1∪ℬ2\\mathcal\{B\}=\\mathcal\{B\}\_\{1\}\\cup\\mathcal\{B\}\_\{2\}satisfies𝒮⁡\(𝒫∪ℬ,ϕ\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\phi\)=\\textnormal\{\{Proved\}\}\}\.

###### Proof\.

Combine the two subproofs by conjunction introduction\. ∎

###### Lemma 4\(Disjunctive decomposition\)\.

Forϕ=ϕ1∨ϕ2\\phi=\\phi\_\{1\}\\lor\\phi\_\{2\}, select any successful branchi∈\{1,2\}i\\in\\\{1,2\\\}with returned bridge setℬi\\mathcal\{B\}\_\{i\}\. If𝒮⁡\(𝒫∪ℬi,ϕi\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\}\_\{i\},\\phi\_\{i\}\)=\\textnormal\{\{Proved\}\}\}, then the selected setℬ=ℬi\\mathcal\{B\}=\\mathcal\{B\}\_\{i\}satisfies𝒮⁡\(𝒫∪ℬ,ϕ\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\phi\)=\\textnormal\{\{Proved\}\}\}\.

###### Proof\.

Apply disjunction introduction to the selected subproof, retaining only its bridge set\. ∎

###### Lemma 5\(Bridge identification\)\.

If Algorithm[2](https://arxiv.org/html/2610.40751#alg2)yields\(ℬ,𝔬\)\(\\mathcal\{B\},\\mathfrak\{o\}\)forϕ\\phi,𝒮⁡\(𝒫∪ℬ𝔬,𝔬\)=Proved\{\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\}\_\{\\mathfrak\{o\}\},\\mathfrak\{o\}\)=\\textnormal\{\{Proved\}\}\}with a Gate\-accepted bridge setℬ𝔬\\mathcal\{B\}\_\{\\mathfrak\{o\}\}, then

𝒮⁡\(𝒫∪ℬ∪ℬ𝔬,ϕ\)=Proved∧Gate⁡\(ℬ∪ℬ𝔬,𝒯\)=Accepted\.\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\}\\cup\\mathcal\{B\}\_\{\\mathfrak\{o\}\},\\phi\)=\\textnormal\{\{Proved\}\}\\quad\\land\\quad\\operatorname\{Gate\}\(\\mathcal\{B\}\\cup\\mathcal\{B\}\_\{\\mathfrak\{o\}\},\\mathcal\{T\}\)=\\textnormal\{\{Accepted\}\}\.

###### Proof\.

The yield statement requires Gate acceptance\. The instantiated premise setℐ\\mathcal\{I\}follows from𝒫\\mathcal\{P\}\. By the abduction condition in Section[4\.3](https://arxiv.org/html/2610.40751#S4.SS3), the instantiated premises and the residual subproof jointly establish the selected supportΣ\\Sigma\. ∎

###### Theorem 1\(Soundness of successful search\)\.

If Algorithm[1](https://arxiv.org/html/2610.40751#alg1)returns a bridge setℬ\\mathcal\{B\}for a goal𝔤\\mathfrak\{g\}, thenℬ\\mathcal\{B\}satisfies both criteria in Equation \([11](https://arxiv.org/html/2610.40751#S4.E11)\):

𝒮⁡\(𝒫∪ℬ,𝔤\)=Proved∧Gate⁡\(ℬ,𝒯\)=Accepted\.\\mathcal\{S\}\(\\mathcal\{P\}\\cup\\mathcal\{B\},\\mathfrak\{g\}\)=\\textsc\{Proved\}\\quad\\land\\quad\\operatorname\{Gate\}\(\\mathcal\{B\},\\mathcal\{T\}\)=\\textsc\{Accepted\}\.

###### Proof\.

We prove by induction on the successful recursive derivation that each successful callProve​\(ϕ,𝒜,𝒯\)\\textsc\{Prove\}\(\\phi,\\mathcal\{A\},\\mathcal\{T\}\)returns a Gate\-accepted bridge set under which the solver can dischargeϕ\\phi\.

*Base case\.*The solver directly provesϕ\\phifrom𝒫\\mathcal\{P\}\. The returned bridge set is empty, so Gate acceptance is vacuous\.

*Inductive step\.*Assume the claim for the successful recursive subcalls\. Normalization preserves equivalence, so it suffices to discharge the normalized obligation\. Its four logical decomposition cases are as follows\.

1. \(i\)ϕ=∃x\.ψ\\phi=\\exists x\.\\,\\psi\. A recursive call succeeds for an admissible instanceψ⁡\[θ\]\\psi\[\\theta\]\. The induction hypothesis establishes that instance with accepted bridges, and Lemma[1](https://arxiv.org/html/2610.40751#Thmsearchlemma1)dischargesϕ\\phi\.
2. \(ii\)ϕ=∀x\.ψ\\phi=\\forall x\.\\,\\psi\. The recursive call succeeds forψ\[x↦cfresh\]\\psi\[x\\mapsto\{c\_\{\\mathrm\{fresh\}\}\}\], withcfresh\{c\_\{\\mathrm\{fresh\}\}\}recorded as arbitrary in the extended grounding table\. The induction hypothesis establishes the body with accepted bridges; those involvingcfresh\{c\_\{\\mathrm\{fresh\}\}\}retain their universal scope\. Lemma[2](https://arxiv.org/html/2610.40751#Thmsearchlemma2)dischargesϕ\\phi\.
3. \(iii\)ϕ=ϕ1∧ϕ2\\phi=\\phi\_\{1\}\\land\\phi\_\{2\}\. Both recursive calls must succeed\. By the induction hypothesis, their returned setsℬ1\\mathcal\{B\}\_\{1\}andℬ2\\mathcal\{B\}\_\{2\}contain accepted bridges and establishϕ1\\phi\_\{1\}andϕ2\\phi\_\{2\}, respectively\. Lemma[3](https://arxiv.org/html/2610.40751#Thmsearchlemma3)dischargesϕ\\phiunder the merged set\.
4. \(iv\)ϕ=ϕ1∨ϕ2\\phi=\\phi\_\{1\}\\lor\\phi\_\{2\}\. At least one recursive call succeeds\. The induction hypothesis establishes the disjunct of any selected successful branch with its accepted bridge setℬi\\mathcal\{B\}\_\{i\}\. Lemma[4](https://arxiv.org/html/2610.40751#Thmsearchlemma4)dischargesϕ\\phiwithℬ=ℬi\\mathcal\{B\}=\\mathcal\{B\}\_\{i\}\.

If no logical decomposition applies, Algorithm[2](https://arxiv.org/html/2610.40751#alg2)yields\(ℬ,𝔬\)\(\\mathcal\{B\},\\mathfrak\{o\}\), and Algorithm[1](https://arxiv.org/html/2610.40751#alg1)recursively proves𝔬\\mathfrak\{o\}\. The induction hypothesis supplies its proof and accepted bridge setℬ𝔬\\mathcal\{B\}\_\{\\mathfrak\{o\}\}\. Lemma[5](https://arxiv.org/html/2610.40751#Thmsearchlemma5)then dischargesϕ\\phiunderℬ∪ℬ𝔬\\mathcal\{B\}\\cup\\mathcal\{B\}\_\{\\mathfrak\{o\}\}, whose bridges are accepted by that lemma and the induction hypothesis\. Thus every successful return supplies a symbolic proof and accepted bridges\. Takingϕ=𝔤\\phi=\\mathfrak\{g\}gives Equation \([11](https://arxiv.org/html/2610.40751#S4.E11)\)\. ∎