SearcharxivSearch

arXiv subjects

Simon DeDeo

Publications and source records attributed to Simon DeDeo.

At least 19 recordsLinked to original sources

Ablation and the Meno: Tools for Empirical Metamathematics

We present the results from Meno, a simple autoformalizer that proves theorems in Lean by systematically exploring the space of both formal and informal proofs, and tactic ablation, a new method for exploring mathematical creativity under constraint. We show these tools in action on simple theorems found in Terrence Tao's Analysis I, selectively ablating solution paths associated with non-constructive proofs, and analyze the properties of the resulting population using Goedel Prover embeddings. Among other things, our analysis of this novel population reveals that they lie on low (one or two) dimensional submanifolds of the much higher-dimensional representation space, and far away from their corresponding human constructions.

cs.LO

A correspondence problem for mathematical proof

Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for a particular derivation to ''correspond'' to a particular proof. Mere existence of a formalization is not enough, and a substantive account of the required correspondence resolves into two criteria -- adequate representation (of the original theorem) and tracking (of the steps in the original proof). An examination of the actually-existing formalization systems we have today shows the variety of quasi-empirical ways we establish these criteria, and points towards new burdens that may be placed on the future evolution of mathematics itself.

math.HO

Explaining Necessary Truths

Knowing the truth is rarely enough -- we also seek out reasons why the fact is true. While much is known about how we explain contingent truths, we understand less about how we explain facts, such as those in mathematics, that are true as a matter of logical necessity. We present a framework, based in computational complexity, where explanations for deductive truths co-emerge with discoveries of simplifying steps during the search process. When such structures are missing, we revert, in turn, to error-based reasons, where a (corrected) mistake can serve as fictitious, but explanatory, contingency-cause: not making the mistake serves as a reason why the truth takes the form it does. We simulate human subjects, using GPT-4o, presented with SAT puzzles of varying complexity and reasonableness, validating our theory and showing how its predictions can be tested in future human studies.

cs.AI

Hard Proofs and Good Reasons

Practicing mathematicians often assume that mathematical claims, when they are true, have good reasons to be true. Such a state of affairs is "unreasonable", in Wigner's sense, because basic results in computational complexity suggest that there are a large number of theorems that have only exponentially-long proofs, and such proofs can not serve as good reasons for the truths of what they establish. Either mathematicians are adept at encountering only the reasonable truths, or what mathematicians take to be good reasons do not always lead to equivalently good proofs. Both resolutions raise new problems: either, how it is that we come to care about the reasonable truths before we have any inkling of how they might be proved, or why there should be good reasons, beyond those of deductive proof, for the truth of mathematical statements. Taking this dilemma seriously provides a new way to make sense of the unstable ontologies found in contemporary mathematics, and new ways to understand how non-human, but intelligent, systems might found new mathematics on inhuman "alien" lemmas.

math.HO

Undermining Mental Proof: How AI Can Make Cooperation Harder by Making Thinking Easier

Large language models and other highly capable AI systems ease the burdens of deciding what to say or do, but this very ease can undermine the effectiveness of our actions in social contexts. We explain this apparent tension by introducing the integrative theoretical concept of "mental proof," which occurs when observable actions are used to certify unobservable mental facts. From hiring to dating, mental proofs enable people to credibly communicate values, intentions, states of knowledge, and other private features of their minds to one another in low-trust environments where honesty cannot be easily enforced. Drawing on results from economics, theoretical biology, and computer science, we describe the core theoretical mechanisms that enable people to effect mental proofs. An analysis of these mechanisms clarifies when and how artificial intelligence can make low-trust cooperation harder despite making thinking easier.

cs.CY

From "um" to "yeah": Producing, predicting, and regulating information flow in human conversation

Conversation demands attention. Speakers must call words to mind, listeners must make sense of them, and both together must negotiate this flow of information, all in fractions of a second. We used large language models to study how this works in a large-scale dataset of English-language conversation, the CANDOR corpus. We provide a new estimate of the information density of unstructured conversation, of approximately 13 bits/second, and find significant effects associated with the cognitive load of both retrieving, and presenting, that information. We also reveal a role for backchannels -- the brief yeahs, uh-huhs, and mhmms that listeners provide -- in regulating the production of novelty: the lead-up to a backchannel is associated with declining information rate, while speech downstream rebounds to previous rates. Our results provide new insights into long-standing theories of how we respond to fluctuating demands on cognitive resources, and how we negotiate those demands in partnership with others.

cs.CL

Sameness Entices, but Novelty Enchants in Fanfiction Online

Cultural evolution is driven by how we choose what to consume and share with others. A common belief is that the cultural artifacts that succeed are ones that balance novelty and conventionality. This balance theory suggests that people prefer works that are familiar, but not so familiar as to be boring; novel, but not so novel as to violate the expectations of their genre. We test this idea using a large dataset of fanfiction. We apply a multiple regression model and a generalized additive model to examine how the recognition a work receives varies with its novelty, estimated through a Latent Dirichlet Allocation topic model, in the context of existing works. We find the opposite pattern of what the balance theory predicts$\unicode{x2014}$overall success decline almost monotonically with novelty and exhibits a U-shaped, instead of an inverse U-shaped, curve. This puzzle is resolved by teasing out two competing forces: sameness attracts the mass whereas novelty provides enjoyment. Taken together, even though the balance theory holds in terms of expressed enjoyment, the overall success can show the opposite pattern due to the dominant role of sameness to attract the audience. Under these two forces, cultural evolution may have to work against inertia$\unicode{x2014}$the appetite for consuming the familiar$\unicode{x2014}$and may resemble a punctuated equilibrium, marked by occasional leaps.

cs.CL

AlephZero and Mathematical Experience

This essay explores the impact of automated proof construction on three key areas of mathematical cognition: on how we judge the role one piece of mathematics plays in another, on how we make mistakes in reasoning about mathematical objects, and on how we understand what our theorems are truly about. It concludes by speculating on a new form of mathematical experience that these methods could make possible: ``glitching'', a game-like search for uncanny consequences of our definitions.

math.HO

Inferring Cultural Landscapes with the Inverse Ising Model

The space of possible human cultures is vast, but some cultural configurations are more consistent with cognitive and social constraints than others. This leads to a ``landscape'' of possibilities that our species has explored over millennia of cultural evolution. But what does this fitness landscape, which constrains and guides cultural evolution, look like? The machine-learning algorithms that can answer these questions are typically developed for large-scale datasets. Applications to the sparse, inconsistent, and incomplete data found in the historical record have received less attention, and standard recommendations can lead to bias against marginalized, under-studied, or minority cultures. We show how to adapt the Minimum Probability Flow algorithm and the Inverse Ising model, a physics-inspired workhorse of machine learning, to the challenge. A series of natural extensions -- including dynamical estimation of missing data, and cross-validation with regularization -- enables reliable reconstruction of the underlying constraints. We demonstrate our methods on a curated subset of the Database of Religious History: records from 407 religious groups throughout human history, ranging from the Bronze Age to the present day. This reveals a complex, rugged, landscape, with both sharp, well-defined peaks where state-endorsed religions tend to concentrate, and diffuse cultural floodplains where evangelical religions, non-state spiritual practices, and mystery religions can be found.

physics.soc-ph

The Diversity of Argument-Making in the Wild: from Assumptions and Definitions to Causation and Anecdote in Reddit's "Change My View"

What kinds of arguments do people make, and what effect do they have on others? Normative constraints on argument-making are as old as philosophy itself, but little is known about the diversity of arguments made in practice. We use NLP tools to extract patterns of argument-making from the Reddit site "Change My View" (r/CMV). This reveals six distinct argument patterns: not just the familiar deductive and inductive forms, but also arguments about definitions, relevance, possibility and cause, and personal experience. Data from r/CMV also reveal differences in efficacy: personal experience and, to a lesser extent, arguments about causation and examples, are most likely to shift a person's view, while arguments about relevance are the least. Finally, our methods reveal a gradient of argument-making preferences among users: a two-axis model, of "personal--impersonal" and "concrete--abstract", can account for nearly 80% of the strategy variance between individuals.

cs.CL

Epistemic Phase Transitions in Mathematical Proofs

Mathematical proofs are both paradigms of certainty and some of the most explicitly-justified arguments that we have in the cultural record. Their very explicitness, however, leads to a paradox, because the probability of error grows exponentially as the argument expands. When a mathematician encounters a proof, how does she come to believe it? Here we show that, under a cognitively-plausible belief formation mechanism combining deductive and abductive reasoning, belief in mathematical arguments can undergo what we call an epistemic phase transition: a dramatic and rapidly-propagating jump from uncertainty to near-complete confidence at reasonable levels of claim-to-claim error rates. To show this, we analyze an unusual dataset of forty-eight machine-aided proofs from the formalized reasoning system Coq, including major theorems ranging from ancient to 21st Century mathematics, along with five hand-constructed cases including Euclid, Apollonius, Hernstein's Topics in Algebra, and Andrew Wiles's proof of Fermat's Last Theorem. Our results bear both on recent work in the history and philosophy of mathematics on how we understand proofs, and on a question, basic to cognitive science, of how we justify complex beliefs.

cs.SC

The Cultural Transmission of Tacit Knowledge

A wide variety of cultural practices take the form of "tacit" knowledge, where the rules and principles are neither obvious to an observer nor known explicitly by the practitioners. This poses a problem for cultural evolution: if beginners cannot simply imitate experts, and experts cannot simply say or demonstrate what they are doing, how can tacit knowledge pass from generation to generation? We present a domain-general model of "tacit teaching", that shows how high-fidelity transmission of tacit knowledge is possible. It applies in cases where the underlying features of the practice are subject to interacting and competing constraints, as is expected both in embodied and in social practices. Our model makes predictions for key features of the teaching process. It predicts a tell-tale distribution of teaching outcomes: some students will be nearly perfect performers while others receiving the same instruction will be disastrously bad. This differs from most mainstream cultural evolution models centered on high-fidelity transmission with minimal copying errors, which lead to a much narrower distribution where students are mostly equally mediocre. The model also predicts generic features of the cultural evolution of tacit knowledge. The evolution of tacit knowledge is expected to be bursty, with long periods of stability interspersed with brief periods of dramatic change, and where tacit knowledge, once lost, becomes essentially impossible to recover.

physics.soc-ph

The Cognitive Science of Extremist Ideologies Online

Extremist ideologies are finding new homes in online forums. These serve as both places for true believers, and recruiting-grounds for curious newcomers. To understand how newcomers learn ideology online, we study the Reddit archives of a novel sexist ideology known as the "the Red Pill''. Matching a longstanding hypothesis in the social sciences, our methods resolve the ideology into two components: a "behavioral'' dimension, concerned with correcting behavior towards the self and others, and an "explanatory'' dimension, of unifying explanations for the worldview. We then build a model of how newcomers to the group navigate the underlying conceptual structure. This reveals a large population of "tourists'', who leave quickly, and a smaller group of "residents'' who join the group and remain for orders of magnitude longer. Newcomers are attracted by the behavioral component, in the form of self-help topics such as diet, exercise, and addiction. Explanations, however, keep them there, turning tourists into residents. They have powerful effects: explanation adoption can more than double the duration of median engagement, and can explain the emergence of a long-tail of high-power engagers. The most sticky explanations, that predict the longest engagement, are about status hierarchies.

cs.SI

When Science is a Game

What happens when scientists are, at certain points in a field's development, playing a game? I present a framework for such an analysis that draws on the theory of games provided by the historian Johan Huizinga. Huizinga gives five conditions for a social practice to become a game: free engagement, disconnection, boundedness in time and arena, the order-creation of rules, and the presence of tension. Application of this theory to scientific practice predicts patterns of behavior that can be tested by quantitative analysis: the emergence of hard boundaries between disciplines, the closure of loopholes in theory creation, resistance to certain innovations in journal publication, and the ways in which scientists fail to prosecute colleagues who engage in questionable research practices.

physics.hist-ph

From Probability to Consilience: How Explanatory Values Implement Bayesian Reasoning

Recent work in cognitive science has uncovered a diversity of explanatory values, or dimensions along which we judge explanations as better or worse. We propose a Bayesian account of how these values fit together to guide explanation. The resulting taxonomy provides a set of predictors for which explanations people prefer and shows how core values from psychology, statistics, and the philosophy of science emerge from a common mathematical framework. In addition to operationalizing the explanatory virtues associated with, for example, scientific argument-making, this framework also enables us to reinterpret the explanatory vices that drive conspiracy theories, delusions, and extremist ideologies.

q-bio.NC

How we do things with words: Analyzing text as social and cultural data

In this article we describe our experiences with computational text analysis. We hope to achieve three primary goals. First, we aim to shed light on thorny issues not always at the forefront of discussions about computational text analysis methods. Second, we hope to provide a set of best practices for working with thick social and cultural concepts. Our guidance is based on our own experiences and is therefore inherently imperfect. Still, given our diversity of disciplinary backgrounds and research practices, we hope to capture a range of ideas and identify commonalities that will resonate for many. And this leads to our final goal: to help promote interdisciplinary collaborations. Interdisciplinary insights and partnerships are essential for realizing the full potential of any computational text analysis that involves social and cultural concepts, and the more we are able to bridge these divides, the more fruitful we believe our work will be.

cs.CL

Lévy Flights of the Collective Imagination

We present a structured random-walk model that captures key aspects of how people communicate in groups. Our model takes the form of a correlated Lévy flight that quantifies the balance between focused discussion of an idea and long-distance leaps in semantic space. We apply our model to three cases of increasing structural complexity: philosophical texts by Aristotle, Hume, and Kant; four days of parliamentary debate during the French Revolution; and branching comment trees on the discussion website Reddit. In the philosophical and parliamentary cases, the model parameters that describe this balance converge under coarse-graining to limit regions that demonstrate the emergence of large-scale structure, a result which is robust to translation between languages. Meanwhile, we find that the political forum we consider on Reddit exhibits a debate-like pattern, while communities dedicated to the discussion of science and news show much less temporal order, and may make use of the emergent, tree-like topology of comment replies to structure their epistemic explorations. Our model allows us to quantify the ways in which social technologies such as parliamentary procedures and online commenting systems shape the joint exploration of ideas.

cs.SI

Aggression heuristics underlie animal dominance hierarchies and provide evidence of group-level social information

Members of a social species need to make appropriate decisions about who, how, and when to interact with others in their group. However, it has been difficult for researchers to detect the inputs to these decisions and, in particular, how much information individuals actually have about their social context. We present a new method that can serve as a social assay to quantify how patterns of aggression depend upon information about the ranks of individuals within social dominance hierarchies. Applied to existing data on aggression in 172 social groups across 85 species in 23 orders, it reveals three main patterns of rank-dependent social dominance: the downward heuristic (aggress uniformly against lower-ranked opponents), close competitors (aggress against opponents ranked slightly below self), and bullying (aggress against opponents ranked much lower than self). The majority of the groups (133 groups, 77%) follow a downward heuristic, but a significant minority (38 groups, 22%) show more complex social dominance patterns (close competitors or bullying) consistent with higher levels of social information use. These patterns are not phylogenetically constrained and different groups within the same species can use different patterns, suggesting that heuristics use may depend on context and the structuring of aggression by social information should not be considered a fixed characteristic of a species. Our approach provides new opportunities to study the use of social information within and across species and the evolution of social complexity and cognition.

q-bio.PE