SMART: State-based Multi Agent Reasoning Traces for Verification-oriented Problem-Solving

Sai Vallurupalli; Francis Ferraro

cs.AINov 5, 2026

SMART: State-based Multi Agent Reasoning Traces for Verification-oriented Problem-Solving

Authors: Sai Vallurupalli, Francis Ferraro

Organizations: Department of Computer Science and Electrical Engineering, University of Maryland Baltimore County, Baltimore, MD 21250 USA

Abstract

Complex problems with limited context, such as claims, require a means to obtain additional knowledge necessary for solution reasoning. We propose a multi-agent framework, SMART, to obtain knowledge through capturing the implicit state of participating entities in a problem context. SMART curates the state knowledge as diverse, complementary and solution-salient premises using a variety of LLMs and a structured role-based prompt strategy. Using knowledge from these real-world verified curated premises, SMART's knowledge guided solution reasoning improves validation performance up to 20% on complex scientific claims spanning 3 datasets. We show that grounding premises in real-world knowledge is necessary and improves performance up to 5%.

Figures & tables

Figure 1: A complex problem’s implicit state-based reasoning using a scientific claim from SciFact Wadden et al. (2020) . We identify experts knowledgeable about participating entities and explore their state and obtain contrastive premises. We curate true premises of supporting or opposing stance and reason with these to infer the solution.

Prompt Type	Claim Prompt
General, Refute Filter	s 10.6.1 , s 10.6.14
Direct & Baselines	s 10.6.2 , s 10.6.3
Identify Salient Entities	s 10.6.4
Explore for Premise Pairs	s 10.6.5
Verify Premise	s 10.6.6 , s 10.6.7
Premise’s Stance	s 10.6.8

Table 1: The prompts we developed; see the Appendix.

Panel of Figure 2 — Figure 2: Comparison of SMART-PK performance with CoT and RAG on SciFact & SFBench datasets, after applying the Refute Filter (rationales are required to adequately support refute labels; see s 5.2 ). SMART-PK improves over baselines; on avg. 10% on SFBench and 5% on Scifact over CoT (details in Appendix Table 4 ).

Panel of Figure 3 — Figure 3: Improving SMART performance using external premise validation with websearch (SMART-WS) and cross model generation and reasoning (X-SMART-PK). For SciFact, X-SMART-PK uses Qwen3 8b generated premises & improves performance by 6.2%; for SFBench, GPT-5.4-mini generated premises lead to 4% improvement.

Figure 4: Comparing SMART-PK performance generating a single premise Vs. contrastive premises on SFBench claims. See Fig. 13 for SciFact claims. Contrastive premises improve performance by 3% across datasets and models. See results in Table 5

Figure 5: We compare the 5 meta-reasonsers for SciFact claims: M-Majority Voting, R-Reasoning Judge, A-Aggregating Judge, C-Critical Judge and S-Supporting Judge. Reasoning Judge consistently improves performance across models and datasets: by 8% on SFBench and 5% on SciFact on average (See Fig. 9 for SFBench claims and results in Appendix Table 7 ).

Figure 6: Comparing SMART-NV where no verification is performed) with verification using self (SMART-PK), external knowledge with websearch (SMART-WS), and cross-model (X-SMART-PK) on SciFact claims. Verification improves performance an average by 2-7% across methods for both datasets, with a few exceptions (see SFBench in Fig. 10 ). See results in appendix Table 8 .

Figure 7: Distribution of GPT-5.4-mini curated stances, their alignment with the claim and their confidence ratings for the SciFact-Open dataset. Supporting and opposing premises are required for supporting claims that of the support and refute type respectively.

Figure 8: We compare the validation performance of SMART-PK with 3 sizes of Qwen and GPT-5.4-mini on SciFact-Open claims using premises generated and curated by one model and solution reasoning with another model. These comparisons show that both Qwen3 8b and GPT-5.4-mini generate good quality premises that other models can curate and use for solution-reasoning.

Model	CoT	SMART-PK	SMART-WS
Gemma 3 1b	.563 $\pm$ .003	.562 $\pm$ .005	.562 $\pm$ .005
Gemma 3 4b	.622 $\pm$ .001	.594 $\pm$ .007	.609 $\pm$ .011
Gemma 3 12b	.680 $\pm$ .002	.654 $\pm$ .003	.651 $\pm$ .005

Table 2: Gemma Models do not make for good SMART agents for two reasons: a) CoT performance is boosted by refuting claims for which there is no supporting evidence. b) Models are good at generating supporting premises but poor at generating contrastive premises that can lead to refuting evidence. This results in SMART meta-reasoning being overly positive with not having opposing reasons for a claim. As a result, we do not use these models in examining other data besides SciFact. This behavior is also seen to a lesser extent with Llama3.1 70b model.

Figure 9: We compare the 5 meta-reasonsers for SFBench claims: M-Majority Voting, R-Reasoning Judge, A-Aggregating Judge, C-Critical Judge and S-Supporting Judge. Reasoning Judge metareasoner is more consistent across models and datasets and improves performance, by 8% on SFBench and 5% on SciFact (See Fig. 5 for SciFact and results in Appendix Table 8 ).

Figure 10: Comparing SMART-PK, where premises are verified with parametric knowledge, with SMART-NV where no verification is performed on SFBench claims, we show that verification improves performance an average of 2% with a few exceptions (also true for SciFact claims in Fig. 6 ). Results are in appendix Table 7 .

Figure 11: Comparing SMART-PK performance using a stronger premise Vs. both premises. Logically using a stronger premise was a good decision (performance of both both GPT-5.4-mini and Claude-Haiku-4.5 reduces due to direct conflicts), however, model reasoning is able to use the additional nuanced information provided by both premises. Larger models are better at leveraging the nuanced information in both premises (Llama70b improves by 1.3% & Qwen3 32b by 6.7%); smaller models benefit from additional premises as they do not curate as many premises (Qwen3 1b improves by 1.5%).

Figure 12: We compare various premise generation methods using the SciFact collection. We obtain premises with a single expert in one-shot (Non-Iter) Vs an iterative generation strategy (Iter). We also compare SMART’s multiple context-derived experts with the iterative strategy. Claude-Haiku-4.5 does not allow obtaining more than one generation per API call; due to this we do not have any result for the single expert in one-shot (Non-Iter) strategy.

Figure 13: Comparing SMART-PK performance generating a single premise Vs. contrastive premises on SciFact claims. See Fig. 4 for SFBench claims. Contrastive premises improve performance by 3% across datasets and models. See results in Table 5

Dataset——— $>$	SFBench			SciFact
Model	CoT	SMART-PK	SMART-S	CoT	SMART-PK	SMART-S
Qwen3 1.7b	56	43	58	78	46	48
Qwen3 8b	28	20	53	63	31	24
Qwen3 32b	12	09	26	67	32	11
Llama 8b	48	27	51	87	99	29
Llama 70b	13	12	47	61	27	18

Table 3: Comparing the percentage of rationales that lack support for a refute claim that are filtered by the Refute Filter for CoT reasoning, SMART-PK reasoning with contrastive premises and the single premise generation method (SMART-S). These lead to incorrect logical reasoning on 50% of SFBench claims and 40% of SciFact claims (claims with a gold refute ). CoT leads to almost double the errors than SMART on smaller models. Single premise generation leads to more errors on SFBench (double the number than on SciFact) where as the reverse is true for contrastive premises. We discuss these results in s 6 .

		Chain-of-Thought			RAG with Web Search			SMART-PK			%SMART
Data	Model	Before RF	After RF	%Drop $\downarrow$	Before RF	After RF	%Drop $\downarrow$	Before RF	After RF	%Drop $\downarrow$	Improv.
	Qwen3 1.7b	.534 $\pm$ .000	.165 $\pm$ .006	36.9	.503 $\pm$ .008	.100 $\pm$ .008	40.3	.535 $\pm$ .023	.274 $\pm$ .025	26.1	10.9
	Qwen3 8b	.610 $\pm$ .006	.369 $\pm$ .005	34.1	.500 $\pm$ .000	.000 $\pm$ .000	50.0	.568 $\pm$ .009	.435 $\pm$ .016	13.3	6.6
	Qwen3 32b	.642 $\pm$ .000	.362 $\pm$ .005	28.0	.507 $\pm$ .068	.096 $\pm$ .022	43.9	.620 $\pm$ .019	.569 $\pm$ .032	5.1	20.7
SFBench	Llama 8b	.523 $\pm$ .000	.243 $\pm$ .099	28.0	.514 $\pm$ .009	.038 $\pm$ .006	47.6	.579 $\pm$ .004	.447 $\pm$ .010	13.2	20.4
	Llama 70b	.643 $\pm$ .000	.514 $\pm$ .000	12.9	.519 $\pm$ .003	.040 $\pm$ .008	47.9	.542 $\pm$ .023	.536 $\pm$ .030	0.6	2.2

Table 4: Comparing the balanced accuracy of CoT, RAG and SMART-PK before and after applying the Refute Filter ( refute labels that are not adequately supported are changed to ’unknown’, essentially dropping them from contributing to balanced accuracy). Smaller models either lack or are unable to leverage claim knowledge and select more refute labels, both with CoT and SMART reasoning (the %drop is higher for the smaller models). However, this incorrect performance boost is worse with CoT than SMART (the %drop is higher for CoT than SMART). It is also worse for SFBench’s Material Science knowledge than SciFact’s Biological Science knowledge (the %drop is higher SFBench than SciFact, Llama3 8b model on SciFact is an exception where the model does not generate most rationales). Web search based on a claim is noisy; up to half the RAG refute labels are based on not finding the appropriate evidence. Since RAG performance is lower than CoT, we provide % SMART improvement over CoT in the last column ( SMART-PK improves performance up to 20%. ) We discuss these results in s 6 .

		Single Premise SMART			Contrastive Premises (SMART-PK)			%Contrast. Improv.
Data	Model	Before RF	After RF	%Drop $\downarrow$	Before RF	After RF	%Drop $\downarrow$	Before RF	After RF
	Qwen3 1.7b	.550 $\pm$ .005	.330 $\pm$ .005	22.0	.535 $\pm$ .023	.274 $\pm$ .025	26.1	-1.5	-5.6
	Qwen3 8b	.566 $\pm$ .005	.392 $\pm$ .005	17.4	.568 $\pm$ .009	.435 $\pm$ .016	13.3	0.2	4.3
	Qwen3 32b	.567 $\pm$ .012	.508 $\pm$ .005	5.9	.620 $\pm$ .019	.569 $\pm$ .032	5.1	5.3	6.1
SFBench	Llama 8b	.611 $\pm$ .016	.442 $\pm$ .005	16.9	.579 $\pm$ .004	.447 $\pm$ .010	13.2	-3.2	0.5
	Llama 70b	.640 $\pm$ .006	.492 $\pm$ .005	14.8	.542 $\pm$ .023	.536 $\pm$ .030	0.6	-9.8	4.4

Table 5: Comparing the balanced accuracy of using Single Vs. Contrastive premises with the SMART framework. We examine performance before and after applying the Refute Filter ( refute labels that are not adequately supported are changed to ’unknown’, essentially dropping them from contributing to balanced accuracy). Single premises often lack necessary claim knowledge that models select refute labels without adequately supporting them. Correcting for this with the Refute Filter shows that contrastive knowledge improves on average across models and datasets by 3%. The smallest model Qwen3 1.7b is worse at obtaining contrastive knowledge, but leads to better performance with single premises. We discuss these results in s 6 .

Data	Model	SMART-PK	SMART-WS	%Imp. $\uparrow$	X-SMART-PK	%Imp. $\uparrow$
	Qwen3 1.7b	.535 $\pm$ .023	.544 $\pm$ .020	0.9	.620 $\pm$ .015	8.5
	Qwen3 8b	.568 $\pm$ .009	.598 $\pm$ .014	3.0	.621 $\pm$ .013	5.3
	Qwen3 32b	.620 $\pm$ .019	.611 $\pm$ .019	-0.9	.645 $\pm$ .021	2.5
SFBench	Llama3.1 8b	.579 $\pm$ .004	.545 $\pm$ .029	-3.4	.578 $\pm$ .019	0.0
	Llama3.1 70b	.542 $\pm$ .023	.610 $\pm$ .007	6.8	.598 $\pm$ .019	5.6
	GPT-5.4-mini	.750 $\pm$ .026	.736 $\pm$ .015	-2.4	.750 $\pm$ .031	-

Table 6: Comparing performance (BAccuracy) of SMART-WS and X-SMART-PK with SMART-PK. X-SMART-PK where models use premises from a better generating model: Qwen3 8b for SciFact and GPT-5.4-mini for SFBench. Since SMART-PK does not lead to as much of an artificial performance boost, we compare results without applying the Refute Filter . Performance on SciFact collection of claims improves by a 6.5-14.1%; and up to 8.5% for SFBench claims. We discuss these results and choice of curation model in s 6 .

Data	Model	SMART-PK	MajVot	AggJ	CriJ	SuppJ	%Improv. $\uparrow$
	Qwen3 1.7b	.535 $\pm$ .023	.536 $\pm$ .022	.540 $\pm$ .009	.520 $\pm$ .005	.528 $\pm$ .010	-0.1
	Qwen3 8b	.568 $\pm$ .009	.522 $\pm$ .014	.558 $\pm$ .007	.543 $\pm$ .016	.586 $\pm$ .021	4.6
	Qwen3 32b	.620 $\pm$ .019	.530 $\pm$ .008	.606 $\pm$ .019	.575 $\pm$ .025	.594 $\pm$ .019	9.0
SFBench	Llama3.1 8b	.579 $\pm$ .004	.464 $\pm$ .014	.534 $\pm$ .027	.529 $\pm$ .014	.568 $\pm$ .022	11.5
	Llama3.1 70b	.542 $\pm$ .023	.506 $\pm$ .042	.552 $\pm$ .015	.553 $\pm$ .007	.523 $\pm$ .005	3.6
	GPT-5.4-mini	.750 $\pm$ .026	.528 $\pm$ .011	.739 $\pm$ .012	.646 $\pm$ .023	.728 $\pm$ .030	22.2

Table 7: Comparing the balanced accuracy of SMART-PK (with Reasoning Judge as meta-reasoner) with 4 other meta-reasoners. We show the advantage of using the Reasoning Judge over Majority Voting in the %Improv. column.

Data	Model	SMART-NV	SMART-PK	%Improv $\uparrow$	SMART-WS	%Improv $\uparrow$	X-SMART-PK	%Improv $\uparrow$
	Qwen3 1.7b	.520 $\pm$ .005	.535 $\pm$ .023	1.5	.544 $\pm$ .020	2.4	.620 $\pm$ .015	10.0
	Qwen3 8b	.542 $\pm$ .014	.568 $\pm$ .009	2.6	.598 $\pm$ .014	5.6	.621 $\pm$ .013	7.9
	Qwen3 32b	.564 $\pm$ .014	.620 $\pm$ .019	4.9	.611 $\pm$ .019	4.7	.645 $\pm$ .021	8.1
SFBench	Llama3.1 8b	.572 $\pm$ .016	.579 $\pm$ .004	0.7	.545 $\pm$ .029	-2.7	.578 $\pm$ .019	0.6
	Llama3.1 70b	.518 $\pm$ .004	.542 $\pm$ .023	2.4	.610 $\pm$ .007	9.2	.598 $\pm$ .019	8.0
	GPT-5.4-mini	.753 $\pm$ .008	.750 $\pm$ .026	-0.3	.736 $\pm$ .015	-1.7	.750 $\pm$ .031	-0.3

Table 8: Comparing the balanced accuracy of SMART without verification (SMART-NV) with self-verification (SMART-PK), external verification with websearch (SMART-WS) and cross-verification (X-SMART-PK). Improvement with each method is shown in %Improve (the difference in performance between SMART-NV and the method). Verification improves performance on average across models and datasets by by 2-7%. Grounding premises with real-world knowledge provided by websearch improves on average by 4-5% with some exceptions.

		Model	SMART-PK Inference				SMART-WS Inference				Premise
Data	Model	Calls	KTok	%Fback	Sup.	Opp.	KTok	%Fback	Sup.	Opp.	Quality
	Qwen3 1.7b	5	11	42	1	0	11	70	.5	0	NA
	Qwen3 8b	11	12	25	1.5	1.2	11	83	.3	.1	NA
	Qwen3 32b	19	13	3	4.1	1.9	12	23	2.0	.73	NA
SFBench	Llama 8b	15	20	4	2.7	1.6	16	40	1.2	.7	NA
	Llama 70b	18	14	0	5	1.9	11	63	.6	.2	NA

Table 9: Comparing inference cost for SMART-PK and SMART-WS in model calls and number of input

+

output tokens measured in K tokens (KTok). We report % fallbacks (Fback) to the direct reasoning prompt when there are no curated premises, the quality of curated premises (Qual) and their average numbers per stance (Sup. & Opp.). Both methods require the same # calls since we verify before obtaining stance; these do not include 10 calls that iteratively obtain premises as a single call could potentially be used to obtain all premises for GPT-5.4-mini and Claude-Haiku-4.5. All values are per claim averages. We report NA-Not applicable as the premise quality (Qual) for SFbench claims due to not having textual evidence. Average premise quality by coincidence is the same for both methods, so we report in a single column.

Panel of Figure 14 — Figure 14: Distribution of curated premise stances, their alignment with the claim and their confidence ratings for Qwen3 models. Correct identification of refuted claims requires opposing premises and supported claims require supporting premises. Qwen3 1.7b curation leads to few and noisy premises compared to Qwen8b. Qwen3 32 generates too many supporting premises increasing meta-reasoning difficulty. Supporting and opposing premises are required for supporting claims of support and refute labels respectively.

Figure 15: We compare various configurations we used for generating premises. The performance of these different configurations is compared in Fig. 12 .

Models	Contrastive premise pairs (separated by an &; … replaces repeating text from premise #1)
Fig. 1 Example Claim: Genetic deletion of JAM-A decreases gut permeability.
Qwen3 1b	Premises are few and superficial.
	Genetic deletion of JAM-A occurs in a specific cellular context. & Genetic deletion of JAM-A does not occur in a specific cellular context.
	Genetic deletion of JAM-A is associated with a specific cellular location. & Genetic deletion of JAM-A is not associated with a specific cellular location.
Qwen3 8b	Premises are atomic and easy to validate.
	JAM-A is involved in maintaining gut barrier integrity. & JAM-A is not … integrity.

Table 10: Example premises with different Qwen3 and GPT-5.4-mini models. See Table 11 for other models.

Models	Contrastive premise pairs (separated by an &; … replaces repeating text from premise #1)
Fig. 1 Example Claim: Genetic deletion of JAM-A decreases gut permeability.
Llama3.1 8b	Premises are limited to the context and do not explore new entities and concepts.
	JAM-A is expressed in the epithelial cells of the gut & JAM-A is not expressed …
	Gut permeability is not affected by JAM-A deletion & Gut permeability is increased by …
	The mechanism of JAM-A’s effect on gut permeability is well understood & The mechanism of JAM-A’s effect on gut permeability is not well understood
	Gut permeability decreases when JAM-A is not present. & Gut permeability does not …

Table 11: Example premises with Llama3 and Claude models. See Table 10 for other models.

Error	Issue Description
	Claim: Fluorine-containing additives in a liquid electrolyte enable Li-ion battery chemistries to cycle up to 10 V.
Type 2b	CoT with Qwen3 8b: refuted label is correct . Rationale: While fluorine-containing additives in electrolytes can improve the performance and stability of Li-ion batteries, there is no widely accepted evidence that they enable cycling up to 10 V. The typical voltage range for Li-ion batteries is around 3.0–4.3 V, and achieving 10 V would require significant technological advancements beyond current understanding and practice.
	SMART with Qwen3 8b : supported label is incorrect . Rationale: The claim is supported by the evidence that fluorine-containing additives increase voltage capacity and enhance electrochemical stability at high voltages. While there are opposing conditions suggesting potential degradation, the supporting conditions are more specific and credible, indicating that fluorine additives can enable Li-ion batteries to cycle up to 10 V.
	Claim: A battery with a lithium titanate anode, a lithium manganese oxide cathode, and an electrolyte consisting of 1M lithium hexafluorophosphate in dimethyl carbonate can pass cold crank at -10’C
Type 1	CoT with Qwen3 8b: Lithium titanate (Li4Ti5O12) anodes and lithium manganese oxide (LiMn2O4) cathodes are known for their good low-temperature performance. The electrolyte described, 1M lithium hexafluorophosphate in dimethyl carbonate, is commonly used in lithium-ion batteries and can function effectively at low temperatures, including -10°C. Therefore, the claim is supported by current scientific knowledge.
	SMART with Qwen3 8b : The claim is not supported because the opposing conditions indicate that the electrolyte loses ionic conductivity, has high viscosity, and the anode has low electrical conductivity at low temperatures, all of which hinder cold crank performance at -10°C.

Table 12: Errors seen in SFBench Data. With Qwen3 8b, 32b and Llama3.1 70b, there are more Type 2a & 2b situations than Type 1 leading to SMART-PK’s lower performance; SMART-WS improves upon some of the Type 2a & 2b errors through external premise validation. See error descriptions in s 10.10 and Table 13 for SciFact errors.

Error	Issue Description
	Claim: Chenodeosycholic acid treatment reduces whole-body energy expenditure.
Type 1	CoT with Qwen3 32b: feasible label is incorrect . Chenodeoxycholic acid (CDCA) is a bile acid and FXR agonist, and FXR activation has been shown in experimental studies to suppress thermogenic pathways and lower whole-body energy expenditure. The evidence is mainly preclinical and context-dependent, so the support is good but not absolute.
	SMART with Qwen3 32b : infeasible label is correct . Chenodeoxycholic acid is a bile acid that can activate pathways such as TGR5, which promotes type 2 deiodinase activity in thermogenic tissue and tends to increase thermogenesis and whole-body energy expenditure. Given these opposing conditions, the claim that it reduces energy expenditure is not supported and is likely opposite to the expected biological effect.
	Claim: Macrolides have no protective effect against myocardial infarction.
Type 2a	CoT with Qwen3 32b: infeasible label is correct . Current scientific evidence does not strongly support the claim that macrolides protect against myocardial infarction. While some studies have suggested potential anti-inflammatory and immunomodulatory effects of macrolides, these effects have not been conclusively linked to a protective role against myocardial infarction in large, well-controlled clinical trials.
	SMART with Qwen3 32b : feasible label is incorrect . The claim that macrolides protect against myocardial infarction is supported by multiple plausible biological mechanisms, including anti-inflammatory, immunomodulatory, antioxidant, and anti-platelet effects, all of which are relevant to cardiovascular disease and myocardial infarction prevention. While there are no opposing conditions presented, the evidence is largely mechanistic and not based on strong clinical trial data showing direct protection against myocardial infarction, which limits the confidence to a high but not maximum level.

Table 13: Errors seen in SciFact Data. With Llama3.1 70b, GPT-5.4-mini and Claude-Haiku-4.5, there are a more Type 2a situations than Type 1 leading to SMART-PK’s lower performance. X-SMART-PK reduces some of the Type 3 and Type 2a errors leading to improved performance. See error descriptions in s 10.10 and Table 13 for SFBench errors.

Multi-Agent LLM Systems

Multi-agent large language model systems coordinate multiple AI agents to solve tasks through communication, specialization, shared tools, and memory.

See all 1,070 papers

Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
Oct 11, 2026Debargha Ganguly, Weicong Chen, Mohsen Hariri +13LLM Agent Training LLM Agent Reliability
Case Western Reserve University · UT Austin · Microsoft Research
Eigen-Agent: Adaptive Multi-Agent Scientific Reasoning with Monitor-Based RAG
Sep 25, 2025Xiangru Tang, Wanghan Xu, Yujie Wang +13Scientific Reasoning in Language Models Multi-Agent Reasoning
Yale University · Shanghai Jiao Tong University · Fudan University +4
Does Recursive Knowledge Construction Help Agents Verify Consensus Claims in Science?
Oct 29, 2026Lun Ai, Yu-Heng Wu, Jonathan Schaul +6Scientific Claim Verification Scientific Agent Benchmarks
European Bioinformatics Institute (EMBL-EBI), European Molecular Biology Laboratory, Hinxton, UK. · Institute for Computational Biomedicine, Heidelberg University, Faculty of Medicine, and Heidelberg University Hospital, Heidelberg, Germany. · EMBL Rome, European Molecular Biology Laboratory, Monterotondo, Italy.

Oct 11, 2026J/K move · Enter open · S save

Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning

Debargha Ganguly, Weicong Chen, Mohsen Hariri, Vikash Singh+12

Case Western Reserve University · UT Austin · Microsoft Research

LLM Agent Training LLM Agent Reliability Efficient Language Model Reasoning

Open paper AskPDF arXiv

We introduce Sequent-Prover, a family of verifier-using language-model agents, and the post-training framework that produces them. Agents reason in an executable SMT-LIB scratchpad: they write complete SMT-LIB programs, query Z3 across turns, inspect solver feedback, repair formalizations, and terminate with an explicit answer. Our recipe, verifier-conditioned trajectory distillation, bootstraps from a noisy teacher proposal policy by sampling multi-turn trajectories, retaining the successful tail that is correct, non-trivial, grounded, and executable, then applying supervised fine-tuning and trajectory-level preference optimization. Because solver success alone does not guarantee semantic faithfulness, we evaluate task accuracy, k-sample reliability, and SMT program quality. Across 37 benchmarks and 7,254 problems per model family, post-training raises the 4B model's per-attempt accuracy from 85.6% to 97.0% and four-sample all-correct reliability (pass^4}) from 64.1% to 91.7%. It also reduces average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k. Sequent-Prover agents give answers backed by executable formal artifacts.

Abstract

Multi-Agent LLM Systems

Explore similar work

Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning

Eigen-Agent: Adaptive Multi-Agent Scientific Reasoning with Monitor-Based RAG

Does Recursive Knowledge Construction Help Agents Verify Consensus Claims in Science?