Timos Antonopoulos

Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos et al.

Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely on probabilistic model checking to compute the ability of the agent to influence reaching a certain event. We call this the scope of agency. We say that there is evidence of intentional behavior if the scope of agency is high and the decisions of the agent are close to being optimal for reaching the event. Our method applies counterfactual reasoning to automatically generate relevant scenarios that can be analyzed to increase the confidence of our assessment. In a case study, we show how our method can distinguish between 'intentional' and 'accidental' traffic collisions.

Ferhat Erata, Sam Kouteili, Thanos Typaldos et al.

Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn effective cubing heuristics. We introduce a neuro-symbolic post-training framework for this task. We design an MCTS-based data curation pipeline that uses symbolic heuristics to explore splitting decisions over SAT competition formulas, producing preference data grounded in solver statistics and augmented with reasoning traces from a teacher model. Our two-stage post-training, supervised fine-tuning (SFT) followed by direct preference optimization (DPO), enables a 4B-parameter model to achieve a pass@5 score of 53 on 100 SAT competition benchmarks, surpassing frontier LLMs such as Claude-Sonnet-4 (50) and matching the best symbolic heuristic (53). Ablations show that SFT alone improves pass@5 from 46 to 51, with DPO adding 2 additional benchmarks; an entropy/agreement ablation on realized first-cube decisions further shows that SFT, not DPO, accounts for the root-level decision diversity that produces complementary per-run coverage over deterministic symbolic methods. This demonstrates that transformers can be trained to make effective cubing decisions in a domain traditionally dominated by symbolic methods.

Ferhat Erata, Orr Paradise, Thanos Typaldos et al. · amazon-science

A self-corrector for a function $f$ takes a black-box oracle computing $f$ that is correct on most inputs and turns it into one that is correct on every input with high probability. Self-correctors exist for any function that is randomly self-reducible (RSR), where the value $f$ at a given point $x$ can be recovered by computing $f$ on random correlated points. While RSRs enable powerful self-correction capabilities and have applications in complexity theory and cryptography, their discovery has traditionally required manual derivation by experts. We present Bitween, a method and tool for automated learning of randomized self-reductions for mathematical functions. We make two key contributions: First, we demonstrate that our learning framework based on linear regression outperforms sophisticated methods including genetic algorithms, symbolic regression, and mixed-integer linear programming for discovering RSRs from correlated samples. Second, we introduce Agentic Bitween, a neuro-symbolic approach where large language models dynamically discover novel query functions for RSR property discovery, leveraging vanilla Bitween as a tool for inference and verification, moving beyond the fixed query functions ($x+r$, $x-r$, $x \cdot r$, $x$, $r$) previously used in the literature. On RSR-Bench, our benchmark suite of 80 scientific and machine learning functions, vanilla Bitween surpasses existing symbolic methods, while Agentic Bitween discovers new RSR properties using frontier models to uncover query functions.

Ning Luo, Qiao Xiang, Timos Antonopoulos et al.

In an interdomain network, autonomous systems (ASes) often establish peering agreements, so that one AS (agreement consumer) can influence the routing policies of the other AS (agreement provider). Peering agreements are implemented in the BGP configuration of the agreement provider. It is crucial to verify their implementation because one error can lead to disastrous consequences. However, the fundamental challenge for peering agreement verification is how to preserve the privacy of both ASes involved in the agreement. To this end, this paper presents IVeri, the first privacy-preserving interdomain agreement verification system. IVeri models the interdomain agreement verification problem as a SAT formula, and develops a novel, efficient, privacy-serving SAT solver, which uses oblivious shuffling and garbled circuits as the key building blocks to let the agreement consumer and provider collaboratively verify the implementation of interdomain peering agreements without exposing their private information. A prototype of IVeri is implemented and evaluated extensively. Results show that IVeri achieves accurate, privacy-preserving interdomain agreement verification with reasonable overhead.