Mason Journals (George Mason Univ.)
Not a member yet
3256 research outputs found
Sort by
Diagnosing and Repairing LLM Proof Failures: An Error Taxonomy and APOLLO-Guided Corrections on MiniF2F
No full textAn important challenge in artificial intelligence is enabling models to perform rigorous mathematical reasoning, which Automated Theorem Proving (ATP) addresses by constructing machine-verifiable proofs. Recent systems use Large Language Models (LLMs) with proof assistants such as Lean4 to automate formal reasoning. Despite strong performances on benchmarks like MiniF2F, current theorem-proving LLMs often rely on best-of-n sampling, which is computationally expensive. Error reflection systems like Lyra, DREAM, MA-LoT, and APOLLO use formal verifier error messages to guide subsequent proof attempts, APOLLO introducing a modular pipeline that reprompts an LLM on failed sub-problems. APOLLO achieves state-of-the-art accuracy on MiniF2F-test with a significantly reduced sampling budget. This work analyzes DeepSeek-Prover-V2-7B’s Pass@1 performance on MiniF2F-test, classifying its errors and determining which APOLLO mitigates. Using Chain-of-Thought prompting, the model attempted all 244 problems once. The resulting proofs were verified by the Lean4 compiler, and failures were categorized through a semantic analysis of the proofs and error messages. DeepSeek-Prover-V2-7B achieved a 49.2% success rate. Among failures, 47.6% were due to natural language reasoning errors (M-type), 37.1% of which were a repetitive generation breakdown subtype (L-type); 25.8% to logic translation errors (IP-type); 20.2% to tactic failures (U-type); 4.8% to inefficient strategies (T-type); and 1.6% to syntax errors (S-type). APOLLO, given a single pass per LLM call and limited recursion, corrected a subset of M/L, IP, and U errors, raising the success rate by 9.4%. A variant using o3-mini for initial reasoning to mitigate M/L-errors (APOLLO-SP) was created and tested, achieving a 6.6% gain, though it was limited by o3-mini’s failures to produce syntactically valid Lean4 proof sketches. The high rate of M/L-errors suggests that reasoning gaps are the primary barrier to improving Pass@1 performance. Future work should evaluate Pass@k performance, test other LLMs and repair frameworks, and develop targeted error correction strategies for the identified error types. Addressing higher-level reasoning and translation failures may require methods such as prompt engineering, fine-tuning NL-to-Lean translation, or agentic repair strategies beyond low-level tactic correction. This error classification and frequency data provides a clearer picture of current ATP limitations, enabling the further improvement of LLM performance in ATP through error reflection
A Retrieval-Augmented Generation-Powered Chatbot for Air Force Policy and Logistics Compliance
No full textAccelerated innovation from foreign adversaries and recent personnel cuts mandated by the U.S. government have intensified time pressure on U.S. Department of the Air Force (DAF) personnel, highlighting the need to reduce administrative overload. A specific pain point involves the over 11,400 regulatory publications that the DAF must interpret and comply with. Previous works have shown potential in using Retrieval-Augmented Generation (RAG) chatbots for complex regulatory documents, and the Air Force Research Laboratory has attempted to implement a chatbot for the U.S. Armed Forces, NIPRGPT. However, this solution is slow, computationally intensive, and prone to hallucinations. As a result, this work aims to provide a faster alternative that can answer complex questions about the aforementioned regulatory publications with specific citations.
Because of its large scope and recent updates, DAF Manual 36-2664 was selected for testing with 17 questions spanning various difficulty levels, plain text, tables, and images. Due to the bullet structure of the document, semantic chunking was employed to divide the document with an average chunk length of 63 words. Several bi-encoding Sentence Transformer models were evaluated, with the all-mpnet-base-v2 model achieving the highest mean reciprocal rank (MRR) of 0.418, outperforming the next best model by 0.072. Cross-encoding with the ms-marco-MiniLM-L6-v2 model further improved MRR to 0.528. Then, due to its strong benchmark performance, the Llama-3.1-8B-Instruct small language model (SLM) was integrated into the system, enabling concise human-like answers to queries. Ten additional questions regarding DAF Manual 36-2664 were formulated, and the system achieved 87.80% of NIPRGPT’s accuracy while responding 18.18x faster, a 15.96x increase in overall utility. Further testing on a different DAF document, DAF Instruction 36-2903, showed similar results. On 12 questions, the system achieved 255.56% of NIPRGPT’s accuracy and responded 9.43x faster, resulting in a 24.10x overall improvement. These findings suggest that small-scale RAG systems can meet the DAF’s growing need to reduce administrative overload. Future research would explore agentic RAG, where another SLM selects the best RAG techniques based on document characteristics and system demands
A Universal Equation for Predicted Fold Improvement of Bivalent Inhibitor Binding Affinities
No full textMonovalent small molecules traditionally inhibit proteins, but other proteins that have multiple shallow sites fail to do so. Several researchers have tethered two monovalents (called bivalents) targeting different shallow sites to increase the overall inhibitory potency. Bivalent molecules provide this potency gain through the tether which effectively concentrates the second ligand around the first. However, predicting the fold improvement in binding has proven challenging, specifically when the tethered monovalents feature differing dissociation constants (KDs). This work uses the reacted-site probability model to predict theoretical best fold improvements possible for heterodimeric bivalents. The model shows a correlation between the increase in tether lengths and the decrease in fold improvement from bivalents. Additionally, we found the fold improvement varies universally as the inverse root of both the KD and the cube of the full tether length. Maximum tether lengths to obtain at least a 10-fold improvement fall naturally out of this equation. Surprisingly long tethers are predicted to increase effective potencies significantly. Researchers can now determine the viability of their bivalent designs against shallow binding pockets
Stock Market Reactions to Corporate Silence: A Data-Driven Study of Sociopolitical Controversies
No full textIncreased pressure on corporations to address divisive social issues has raised questions about the financial risks of speaking out versus staying silent. While prior research (e.g., Hersch et al., 2008) finds short-term stock gains from political expression, the market impact of corporate silence remains unclear. This research compares the stock returns of 10 silent companies and 10 vocal companies. In this context, a company is silent if it made no public statements about the bill, and vocal if it publicly opposed the bill—through official statements, social media, or CEO commentary—in a way that aligned with prevailing public sentiment or civil rights concerns. The analysis focuses on three social issues: Trump Travel Ban (2017), Georgia Election Reforms (2021), and Florida Parental Rights in Education Act (2022). Using the event study methodology and a trading-day window of (−2, +6), we calculated the cumulative abnormal returns (CAR) to assess the market's response. Although return differentials between vocal and silent firms are modest, vocal firms more frequently outperformed the S&P 500 during the event window, while silent firms underperformed. These findings suggest that speaking out may shape market perception, albeit in ways moderated by industry context, concurrent news, and broader macroeconomic factors
Empirical Validation of Account Abstraction: A Quantitative Analysis of Transaction Performance and Adoption Patterns in the Ethereum Blockchain
No full textAccount abstraction (AA) is a novel blockchain innovation which offers programmable account logic and enhanced transactions capabilities beyond traditional Externally Owned Accounts (EOAs) on Ethereum. Theoretical advantages of the technology include gasless transactions, strengthened privacy, batched transactions, and an elevated user experience; however, an empirical validation of AA’s proposed benefits remains limited. With over $81 billion dollars of digital assets secured across 110 million unique accounts in the Ethereum infrastructure, a robust evaluation of the technology’s proposed benefits is crucial. This study conducts a comprehensive quantitative analysis of AA adoption and performance across major blockchain platforms beyond solely Ethereum. Our methodology leveraged automated data collection from Etherscan and BundleBear APIs to gather transaction volumes, gas consumption patterns, failure rates, and other relevant transaction metrics for AA implementations holding more than a 1% DeFi market share. Afterwards, we completed a statistical analysis to compare the efficiency of AA transactions with traditional EOAs. The analysis revealed that an overwhelming majority of AA transactions were sponsored: about 99.2% of UserOperations had their gas paid by a paymaster. Moreover, we found that the ERC-4337 AA failure rate of 3.2% was substantially lower than the Optimism EOA failure rate of 5.0%. Finally, we noticed that a significant portion of AA transactions were batched as large bundlers–such as Alchemy and Coinbase–see around 2-3 UOs per transaction. Ultimately, this work provides a needed validation of AA’s many proposed benefits and lays the groundwork for future innovation atop the promising technology
The Determinants of Trading Activity in Tokenized Equity Markets: Legal Design and On-Chain Performance
No full textTokenized equities, on‑chain representations of conventional stocks and ETFs, are marketed for 24/7 access,fractionalization, and DeFi composability. Yet whether these instruments actually behave like their off‑chain counterpartsremains unclear. Prior work catalogs legal wrappers and notes thin liquidity but does not quantitatively link structuraldesign to observed trading outcomes. We address this gap by assembling and analyzing 106 tokenized equity productslisted on RWA.xyz, integrating legal, technical, and on‑chain data into a single panel. Prospectuses and SEC/EDGAR filingswere parsed and cross‑referenced with blockchain data (Etherscan, Arbiscan, Solscan) to classify each token’s legalwrapper, jurisdiction, peg mechanism, redemption terms, and transaction activity. We computed concentration andtransfer-frequency statistics, NAV-alignment indicators, and ownership dispersion, then used panel regression methodswith issuer fixed effects to analyze relationships between structural features and trading patterns. From this analysis, aclear pattern emerges: a single issue (Exodus) accounts for ≥60% of aggregate value, skewing concentration measures,while Dinari lists 347 products but contributes <1%, evidencing breadth without depth. Most tokens exhibit ≤10 transfersper month, confirming a buy‑and‑hold profile rather than continuous secondary trading. Jurisdictional choices are uneven(≈38% Swiss SPVs, 24% U.S. Trust/Reg S, 13% Liechtenstein SPVs), illustrating regulatory arbitrage. Although ≈87% assertfully backed, 1:1 pegs, independent audits are rare and redemption rights differ sharply across issuers; these frictionsalign with the absence of meaningful price discovery. Overall, enforceable redemption rights and transparent custody, nottokenization alone, are prerequisites for genuine, continuous price discovery and liquid secondary markets in tokenizedequities
Understanding the Behavior of Institutional Funds
No full textThe real-world asset market (RWA) is an expanding industry in which traditional assets such as real estate, commodities, and financial instruments are tokenized and utilized on the blockchain. Recent developments within the RWA market indicate an increasing volume of institutional funds, including hedge funds, venture capital, private credit, and other alternative investments. The understanding of this sector remains limited, resulting in a lack of useful information for regulators, market participants, and other academic researchers. Utilizing rwa.xyz, company newsletters, and blockchain transactions, we are able to conduct a comprehensive examination of the institutional funds industry. Specifically, by examining regulatory filings and prospectuses, crucial details such as legal considerations, peg mechanisms, economic rationale, and market implications were revealed. A thorough analysis of the market shows typically around 46% of the market relies on a master-feeder fund structure, exclusively opened to accredited investors. These funds appeal to investors because of their yield-bearing potential, decreased minimum investments (20,000), and accessibility to the global market. Their influence on the credit market is significant. By utilizing the blockchain, they open the market to a broader investment base and allow for greater transparency, therefore enabling increased efficiency within the credit market. However, the volatility of the fund is extreme, with certain time periods having high activity and other times having idle activity. This phenomenon is due to roughly 50% of the funds being feeder funds, meaning they usually can only mint and burn at specific times, causing large shifts in the market. These results provide a deeper insight into the institutional funds market and allow investors greater information on which to base their financial decisions
How do regulatory frameworks and governance structures of cryptocurrency exchanges influence their product offerings, geographic reach, and exposure to enforcement actions?
No full textAs market power is growing in centralized cryptocurrency exchanges (CEXs), they are increasingly exposed to more advanced global regulation and scrutiny. The exchanges vary widely in control arrangements–ranging from regulated, publicly traded markets to opaque offshore entities. This project analyzes how regulatory environment and governance arrangements shape the operational profiles of cryptocurrency exchanges, with emphasis on product offerings, geographic access to markets, and exposure to enforcement action. We constructed a formal database of over 200 CEXs from public announcements, licensing registries, exchange transparency reports, and regulatory filings. For each exchange, we identified its ownership structure, legal domicile, product types (e.g., spot, futures, staking), known licenses, regulatory frameworks followed, and documented cases of enforcement or judicial sanctions. We labeled exchanges by governance transparency (i.e., recognized executives, investor backing) and jurisdictional risk according to regulatory stringency. Preliminary results indicate that exchanges with strong internal governance and militant licensing are well placed to maintain wider product offerings across more jurisdictions with less legal upheaval. On the other hand, light-touch jurisdiction-based exchanges (i.e., Seychelles, British Virgin Islands) restrict product offerings in central markets and face more recurring enforcement. This study offers a comparative framework for analyzing the institutional maturity and legal exposure of CEXs. It provides insights for regulators, institutional investors, and researchers seeking to know how organizational and regulatory structures determine risk and reach in digital asset markets
Benchmarking Food Transformation in Africa Through the Use of Machine Learning Modelling
No full textDeveloping nations across the African continent face persistent challenges with food insecurity. In response to this, the CAADP framework has been adopted with the goal of transforming the agrifood sector in order to alleviate hunger. The objective of this study is to assess the extent to which various African nations have made progress towards reaching the targets of the CAADP framework and to identify indicators that can be used to inform food transformation policy. The GPT-4o Large Language Model (LLM) is employed to extract country profile data from the latest CAADP biennial report. While relevant macroeconomic indicators were obtained from publicly available World Bank and IMF databases. Several machine learning models are then employed to model and analyze the relationship between indicators and the C-value, a numeric value that represents a country’s progress towards a specific performance category. Initial results using a Random Forest Regressor model, developed to predict public expenditures to agriculture based on indicators such as government debt (% of GDP), government revenue (% of GDP), and government expenditure (% of GDP), show an r-squared value of 0.67 and a mean absolute error (MAE) of 0.875. Further models will be developed and evaluated using the most recent macroeconomic indicators from 2025 to provide a more nuanced assessment of the current status of food transformation in Africa
Proteomic Analysis of Rhizoplane Microbiomes as Treatments for Hydroponic Phytopathogens
No full textPlant pathogens such as the oomycetes Phytophthora and Pythium spp. commonly cause root rot in hydroponic systems and represent major threats to food security. The current study aims to examine how plant-growth-promoting microbes prevent root rot in hydroponic systems by examining the rhizosphere proteome. Microbiomes are typically studied using genomics for taxonomic identification, but proteomics has potential to provide more insight, such as understanding the mechanisms of infection, measuring the effectiveness of biocontrol treatments and for diagnostics. Amaranthus tricolor seeds were planted on burlap in a series of hydroponic systems and treated with rhizobacteria and mycorrhizae, then infected with an unknown oomycete isolate cultured in a vegetable-based broth. Root rot spread rapidly in the trials, and the treatment failed to prevent symptoms. Roots were harvested and sonicated in water then filtered through cheesecloth to collect the rhizosphere microbes. Proteins were extracted using phenol and sodium dodecyl sulfate. Protein extracts were then analyzed using MALDI-TOF mass spectrometry. Data yielded over 22,874 proteins across 12 samples, showing that the sonication and extraction methods worked well. Among the proteins identified using BLAST analysis were specific to Phytophthora, Pythium, and Fusarium. Given that there were multiple proteins specific to Phytophthora, there is a strong possibility that the unknown isolate utilized in the study is Phytophthora. However, the isolated pathogen could include more than one genus. More analysis is needed to determine if proteomics can be used for agricultural biocontrol analyses