BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Koundinya Vajjha

Koundinya Vajjha contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Machine LearningLogic in Computer ScienceArtificial Intelligencemath.MGmath.OCmath.PRProgramming Languages

Trust snapshot

Quick read

Trust 17 - UnverifiedVerification L1Unclaimed author
4works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

4 published item(s)

preprint2022arXiv

Formalization of a Stochastic Approximation Theorem

Stochastic approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown and direct observations are corrupted by noise. These algorithms are useful, for instance, for root-finding and function minimization when the target function or model is not directly known. Originally introduced in a 1951 paper by Robbins and Monro, the field of Stochastic approximation has grown enormously and has come to influence application domains from adaptive signal processing to artificial intelligence. As an example, the Stochastic Gradient Descent algorithm which is ubiquitous in various subdomains of Machine Learning is based on stochastic approximation theory. In this paper, we give a formal proof (in the Coq proof assistant) of a general convergence theorem due to Aryeh Dvoretzky, which implies the convergence of important classical methods such as the Robbins-Monro and the Kiefer-Wolfowitz algorithms. In the process, we build a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On the Reinhardt Conjecture and Formal Foundations of Optimal Control

We describe a reformulation (following Hales (2017)) of a 1934 conjecture of Reinhardt on pessimal packings of convex domains in the plane as a problem in optimal control theory. Several structural results of this problem including its Hamiltonian structure and Lax pair formalism are presented. General solutions of this problem for constant control are presented and are used to prove that the Pontryagin extremals of the control problem are constrained to lie in a compact domain of the state space. We further describe the structure of the control problem near its singular locus, and prove that we recover the Pontryagin system of the multi-dimensional Fuller optimal control problem (with two dimensional control) in this case. We show how this system admits logarithmic spiral trajectories when the control set is the circumscribing disk of the 2-simplex with the associated control performing an infinite number of rotations on the boundary of the disk in finite time. We also describe formalization projects in foundational optimal control viz., model-based and model-free Reinforcement Learning theory. Key ingredients which make these formalization novel viz., the Giry monad and contraction coinduction are considered and some applications are discussed.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

A Formal Proof of PAC Learnability for Decision Stumps

We present a formal proof in Lean of probably approximately correct (PAC) learnability of the concept class of decision stumps. This classic result in machine learning theory derives a bound on error probabilities for a simple type of classifier. Though such a proof appears simple on paper, analytic and measure-theoretic subtleties arise when carrying it out fully formally. Our proof is structured so as to separate reasoning about deterministic properties of a learning function from proofs of measurability and analysis of probabilities.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Verification of ML Systems via Reparameterization

As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machine learning algorithms with formal guarantees about performance, robustness, or fairness. Yet, the analysis of these algorithms is often complex, and implementing such systems in practice introduces room for error. Proof assistants can be used to formally verify machine learning systems by constructing machine checked proofs of correctness that rule out such bugs. However, reasoning about probabilistic claims inside of a proof assistant remains challenging. We show how a probabilistic program can be automatically represented in a theorem prover using the concept of \emph{reparameterization}, and how some of the tedious proofs of measurability can be generated automatically from the probabilistic program. To demonstrate that this approach is broad enough to handle rather different types of machine learning systems, we verify both a classic result from statistical learning theory (PAC-learnability of decision stumps) and prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.

0 citations0 reviewsNo code linkedOpen access